Closing one open covariance edge

After a marked covariance is replaced by one Fourier character, its two endpoints no longer have to carry the same spatial cell label. The remaining covariance edges still form a pairing. This file closes that one open edge by adjoining two final positions: the old marked endpoints are paired with copies carrying their respective labels.

The construction is deliberately made before any word or pairing sum is estimated. It is the combinatorial bridge from the genuine one-open-edge R-324 fibre to the existing permutation-sum machine.

def Anderson4D.openEdgeAugmentedSumPairing {m : ℕ} (κ : PartialPairing (Fin m)) (a b : Fin m) (hκab : κ a = b) (hab : a ≠ b) : PartialPairing (Fin m ⊕ Fin 2)

The involution on Fin m ⊕ Fin 2 obtained by cutting the edge a ↔ b and pairing its endpoints with the two new positions.

Equations

• One or more equations did not get rendered due to their size.

def Anderson4D.openEdgeAugmentedPairing {m : ℕ} (κ : PartialPairing (Fin m)) (a b : Fin m) (hκab : κ a = b) (hab : a ≠ b) : PartialPairing (Fin (m + 2))

The same augmented pairing on the ordered carrier Fin (m + 2).

Equations

• Anderson4D.openEdgeAugmentedPairing κ a b hκab hab = (Anderson4D.PartialPairing.congr finSumFinEquiv) (Anderson4D.openEdgeAugmentedSumPairing κ a b hκab hab)

def Anderson4D.openEdgeFirstNew (m : ℕ) : Fin (m + 2)

The first new position, immediately after the old carrier.

Equations

• Anderson4D.openEdgeFirstNew m = Fin.natAdd m 0

def Anderson4D.openEdgeSecondNew (m : ℕ) : Fin (m + 2)

The final new position.

Equations

• Anderson4D.openEdgeSecondNew m = Fin.natAdd m 1

@[simp]

theorem Anderson4D.openEdgeFirstNew_val (m : ℕ) : ↑(openEdgeFirstNew m) = m

@[simp]

theorem Anderson4D.openEdgeSecondNew_val (m : ℕ) : ↑(openEdgeSecondNew m) = m + 1

@[simp]

theorem Anderson4D.openEdgeAugmentedPairing_old_left {m : ℕ} (κ : PartialPairing (Fin m)) (a b : Fin m) (hκab : κ a = b) (hab : a ≠ b) : (openEdgeAugmentedPairing κ a b hκab hab) (Fin.castAdd 2 a) = openEdgeFirstNew m

@[simp]

theorem Anderson4D.openEdgeAugmentedPairing_old_right {m : ℕ} (κ : PartialPairing (Fin m)) (a b : Fin m) (hκab : κ a = b) (hab : a ≠ b) : (openEdgeAugmentedPairing κ a b hκab hab) (Fin.castAdd 2 b) = openEdgeSecondNew m

@[simp]

theorem Anderson4D.openEdgeAugmentedPairing_firstNew {m : ℕ} (κ : PartialPairing (Fin m)) (a b : Fin m) (hκab : κ a = b) (hab : a ≠ b) : (openEdgeAugmentedPairing κ a b hκab hab) (openEdgeFirstNew m) = Fin.castAdd 2 a

@[simp]

theorem Anderson4D.openEdgeAugmentedPairing_secondNew {m : ℕ} (κ : PartialPairing (Fin m)) (a b : Fin m) (hκab : κ a = b) (hab : a ≠ b) : (openEdgeAugmentedPairing κ a b hκab hab) (openEdgeSecondNew m) = Fin.castAdd 2 b

@[simp]

theorem Anderson4D.openEdgeAugmentedPairing_old_other {m : ℕ} (κ : PartialPairing (Fin m)) (a b i : Fin m) (hκab : κ a = b) (hab : a ≠ b) (hia : i ≠ a) (hib : i ≠ b) : (openEdgeAugmentedPairing κ a b hκab hab) (Fin.castAdd 2 i) = Fin.castAdd 2 (κ i)

The corresponding word

def Anderson4D.openEdgeAugmentedSumWord {α : Type u_1} {m : ℕ} (w : Fin m → α) (a b : Fin m) : Fin m ⊕ Fin 2 → α

Copy the labels at the two opened endpoints onto the two new positions.

Equations

• Anderson4D.openEdgeAugmentedSumWord w a b (Sum.inl i) = w i
• Anderson4D.openEdgeAugmentedSumWord w a b (Sum.inr j) = if j = 0 then w a else w b

def Anderson4D.openEdgeAugmentedWord {α : Type u_1} {m : ℕ} (w : Fin m → α) (a b : Fin m) : Fin (m + 2) → α

The augmented word on the ordered carrier Fin (m + 2).

Equations

• Anderson4D.openEdgeAugmentedWord w a b i = Anderson4D.openEdgeAugmentedSumWord w a b (finSumFinEquiv.symm i)

@[simp]

theorem Anderson4D.openEdgeAugmentedWord_old {α : Type u_1} {m : ℕ} (w : Fin m → α) (a b i : Fin m) : openEdgeAugmentedWord w a b (Fin.castAdd 2 i) = w i

@[simp]

theorem Anderson4D.openEdgeAugmentedWord_firstNew {α : Type u_1} {m : ℕ} (w : Fin m → α) (a b : Fin m) : openEdgeAugmentedWord w a b (openEdgeFirstNew m) = w a

@[simp]

theorem Anderson4D.openEdgeAugmentedWord_secondNew {α : Type u_1} {m : ℕ} (w : Fin m → α) (a b : Fin m) : openEdgeAugmentedWord w a b (openEdgeSecondNew m) = w b

theorem Anderson4D.openEdgeAugmentedPairing_respectsWord {α : Type u_1} {m : ℕ} (κ : PartialPairing (Fin m)) (a b : Fin m) (hκab : κ a = b) (hab : a ≠ b) (w : Fin m → α) (hrespect : ∀ (i : Fin m), i ≠ a → i ≠ b → w i = w (κ i)) : (openEdgeAugmentedPairing κ a b hκab hab).RespectsWord (openEdgeAugmentedWord w a b)

If every unmarked old edge respects the original word, the closed augmented pairing respects the augmented word.

theorem Anderson4D.openEdgeAugmentedPairing_isFull {m : ℕ} (κ : PartialPairing (Fin m)) (a b : Fin m) (hκab : κ a = b) (hab : a ≠ b) (hfull : κ.IsFull) : (openEdgeAugmentedPairing κ a b hκab hab).IsFull

Closing the marked edge preserves fullness.

theorem Anderson4D.openEdgeAugmentedPairing_isPrimitive {m : ℕ} (κ : PartialPairing (Fin m)) (a b : Fin m) (hκab : κ a = b) (hab : a < b) (hfull : κ.IsFull) (hprimitive : IsPrimitive κ) : IsPrimitive (openEdgeAugmentedPairing κ a b hκab ⋯)

The dummy closure of a lower marked edge in a primitive full pairing is again primitive. Appending the copies in lower/upper order is essential: a fully paired interval reaching the first copy must also contain the old upper endpoint, hence must reach the final copy.

theorem Anderson4D.noProperLeafBlock_openEdgeAugmentedWord {α : Type u_1} [Fintype α] [DecidableEq α] {m : ℕ} (κ : PartialPairing (Fin m)) (a b : Fin m) (hκab : κ a = b) (hab : a < b) (hfull : κ.IsFull) (hprimitive : IsPrimitive κ) (w : Fin m → α) (hrespect : ∀ (i : Fin m), i ≠ a → i ≠ b → w i = w (κ i)) : NoProperLeafBlock (openEdgeAugmentedWord w a b)

Consequently, a spatial word respected by every unmarked edge becomes a genuine primitive word after the two dummy copies are appended.