Primitive across pairings and the word condition in paper (5.11)(c)

An across pairing κ : A ≃ Aᶜ determines a fixed-point-free involution of all positions: use κ on A and κ.symm on its complement. This file connects that representation to PartialPairing, transfers primitivity to the word-level leaf-block condition in (5.11)(c), and records the corresponding filtered form of the factorial estimate (5.10).

def Anderson4D.PartialPairing.Crosses {m : ℕ} (κ : PartialPairing (Fin m)) (A : Finset (Fin m)) : Prop

A pairing crosses the cut A | Aᶜ when every position is sent to the opposite side.

Equations

• κ.Crosses A = ∀ (i : Fin m), κ i ∈ A ↔ i ∉ A

@[implicit_reducible]

instance Anderson4D.PartialPairing.instDecidableCrosses {m : ℕ} (κ : PartialPairing (Fin m)) (A : Finset (Fin m)) : Decidable (κ.Crosses A)

Equations

• κ.instDecidableCrosses A = Anderson4D.PartialPairing.instDecidableCrosses._aux_1 κ A

def Anderson4D.PartialPairing.RespectsWord {α : Type u_1} {m : ℕ} (κ : PartialPairing (Fin m)) (w : Fin m → α) : Prop

A partial pairing respects a word when paired positions carry the same letter.

Equations

• κ.RespectsWord w = ∀ (i : Fin m), w i = w (κ i)

@[implicit_reducible]

instance Anderson4D.PartialPairing.instDecidableRespectsWord {α : Type u_1} [DecidableEq α] {m : ℕ} (κ : PartialPairing (Fin m)) (w : Fin m → α) : Decidable (κ.RespectsWord w)

Equations

• κ.instDecidableRespectsWord w = Anderson4D.PartialPairing.instDecidableRespectsWord._aux_1 κ w

theorem Anderson4D.PartialPairing.Crosses.isFull {m : ℕ} {κ : PartialPairing (Fin m)} {A : Finset (Fin m)} (hκ : κ.Crosses A) : κ.IsFull

Crossing a cut rules out fixed points.

def Anderson4D.acrossMap {m : ℕ} (A : Finset (Fin m)) (κ : AcrossPairing A) (i : Fin m) : Fin m

The underlying map of the full involution associated with an across pairing.

Equations

• Anderson4D.acrossMap A κ i = if hi : i ∈ A then ↑(κ ⟨i, hi⟩) else ↑((Equiv.symm κ) ⟨i, ⋯⟩)

theorem Anderson4D.acrossMap_involutive {m : ℕ} (A : Finset (Fin m)) (κ : AcrossPairing A) : Function.Involutive (acrossMap A κ)

def Anderson4D.acrossToPartialPairing {m : ℕ} (A : Finset (Fin m)) (κ : AcrossPairing A) : PartialPairing (Fin m)

Extend an across pairing to the full involution that uses κ on A and κ.symm on Aᶜ.

Equations

• Anderson4D.acrossToPartialPairing A κ = { toFun := Anderson4D.acrossMap A κ, involutive := ⋯ }

@[simp]

theorem Anderson4D.acrossToPartialPairing_apply_mem {m : ℕ} (A : Finset (Fin m)) (κ : AcrossPairing A) {i : Fin m} (hi : i ∈ A) : (acrossToPartialPairing A κ) i = ↑(κ ⟨i, hi⟩)

@[simp]

theorem Anderson4D.acrossToPartialPairing_apply_notMem {m : ℕ} (A : Finset (Fin m)) (κ : AcrossPairing A) {i : Fin m} (hi : i ∉ A) : (acrossToPartialPairing A κ) i = ↑((Equiv.symm κ) ⟨i, ⋯⟩)

theorem Anderson4D.acrossToPartialPairing_crosses {m : ℕ} (A : Finset (Fin m)) (κ : AcrossPairing A) : (acrossToPartialPairing A κ).Crosses A

The extended involution crosses the prescribed cut.

theorem Anderson4D.acrossToPartialPairing_isFull {m : ℕ} (A : Finset (Fin m)) (κ : AcrossPairing A) : (acrossToPartialPairing A κ).IsFull

In particular, the extended involution is a full pairing.

theorem Anderson4D.acrossToPartialPairing_respectsWord_iff {α : Type u_1} {m : ℕ} (A : Finset (Fin m)) (w : Fin m → α) (κ : AcrossPairing A) : (acrossToPartialPairing A κ).RespectsWord w ↔ RespectsWord A w κ

Compatibility with a word is unchanged by extending an across pairing to the corresponding full involution.

def Anderson4D.IsPrimitiveAcross {m : ℕ} (A : Finset (Fin m)) (κ : AcrossPairing A) : Prop

Primitivity of an across pairing means primitivity of its associated full partial pairing.

Equations

• Anderson4D.IsPrimitiveAcross A κ = Anderson4D.IsPrimitive (Anderson4D.acrossToPartialPairing A κ)

@[implicit_reducible]

instance Anderson4D.instDecidablePredAcrossPairingIsPrimitiveAcross {m : ℕ} (A : Finset (Fin m)) : DecidablePred (IsPrimitiveAcross A)

Equations

• Anderson4D.instDecidablePredAcrossPairingIsPrimitiveAcross A κ = Anderson4D.instDecidablePredAcrossPairingIsPrimitiveAcross._aux_1 A κ

def Anderson4D.letterPositions {α : Type u_1} [DecidableEq α] {m : ℕ} (w : Fin m → α) (S : Finset α) : Finset (Fin m)

All positions whose letters lie in S.

Equations

• Anderson4D.letterPositions w S = {i : Fin m | w i ∈ S}

@[simp]

theorem Anderson4D.mem_letterPositions {α : Type u_1} [DecidableEq α] {m : ℕ} {w : Fin m → α} {S : Finset α} {i : Fin m} : i ∈ letterPositions w S ↔ w i ∈ S

def Anderson4D.NoProperLeafBlock {α : Type u_1} [Fintype α] [DecidableEq α] {m : ℕ} (w : Fin m → α) : Prop

Paper (5.11)(c). The positions occupied by any nonempty proper subset of the letters cannot form a proper interval.

Equations

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

@[implicit_reducible]

instance Anderson4D.instDecidableNoProperLeafBlock {α : Type u_1} [Fintype α] [DecidableEq α] {m : ℕ} (w : Fin m → α) : Decidable (NoProperLeafBlock w)

Equations

• Anderson4D.instDecidableNoProperLeafBlock w = Anderson4D.instDecidableNoProperLeafBlock._aux_1 w

theorem Anderson4D.isFullyPairedOn_letterPositions {α : Type u_1} [DecidableEq α] {m : ℕ} {κ : PartialPairing (Fin m)} {w : Fin m → α} (hfull : κ.IsFull) (hword : κ.RespectsWord w) (S : Finset α) : IsFullyPairedOn κ (letterPositions w S)

Every union of word fibers is fully paired when a full pairing respects the word.

theorem Anderson4D.noProperLeafBlock_of_primitive_full_respectsWord {α : Type u_1} [Fintype α] [DecidableEq α] {m : ℕ} {κ : PartialPairing (Fin m)} {w : Fin m → α} (hprimitive : IsPrimitive κ) (hfull : κ.IsFull) (hword : κ.RespectsWord w) : NoProperLeafBlock w

A primitive full pairing respecting a word forces (5.11)(c).

theorem Anderson4D.noProperLeafBlock_of_primitive_across {α : Type u_1} [Fintype α] [DecidableEq α] {m : ℕ} {A : Finset (Fin m)} {w : Fin m → α} {κ : AcrossPairing A} (hprimitive : IsPrimitiveAcross A κ) (hword : RespectsWord A w κ) : NoProperLeafBlock w

Primitive compatible across pairings imply the word restriction in paper (5.11)(c).

def Anderson4D.primitiveCompatibleAcrossPairings {α : Type u_1} [DecidableEq α] {m : ℕ} (A : Finset (Fin m)) (w : Fin m → α) : Finset (AcrossPairing A)

Compatible across pairings whose associated full pairing is primitive.

Equations

• Anderson4D.primitiveCompatibleAcrossPairings A w = Finset.filter (Anderson4D.IsPrimitiveAcross A) (Anderson4D.compatibleAcrossPairings A w)

@[simp]

theorem Anderson4D.mem_primitiveCompatibleAcrossPairings {α : Type u_1} [DecidableEq α] {m : ℕ} {A : Finset (Fin m)} {w : Fin m → α} {κ : AcrossPairing A} : κ ∈ primitiveCompatibleAcrossPairings A w ↔ RespectsWord A w κ ∧ IsPrimitiveAcross A κ

theorem Anderson4D.primitiveCompatibleAcrossPairings_eq_empty_of_not_noProperLeafBlock {α : Type u_1} [Fintype α] [DecidableEq α] {m : ℕ} {A : Finset (Fin m)} {w : Fin m → α} (hw : ¬NoProperLeafBlock w) : primitiveCompatibleAcrossPairings A w = ∅

A word violating (5.11)(c) admits no primitive compatible across pairing.

def Anderson4D.primitivePairedWordSum {α : Type u_1} [Fintype α] [DecidableEq α] {m : ℕ} (mult : α → ℕ) (A : Finset (Fin m)) (F : (Fin m → α) → ℝ) : ℝ

The paired word sum restricted to primitive full pairings.

Equations

• Anderson4D.primitivePairedWordSum mult A F = ∑ w ∈ Anderson4D.validWords mult, ↑(Anderson4D.primitiveCompatibleAcrossPairings A w).card * F w

theorem Anderson4D.primitivePairedWordSum_le_halfFactorial_mul_wordSumFiltered {α : Type u_1} [Fintype α] [DecidableEq α] {m : ℕ} (mult : α → ℕ) (A : Finset (Fin m)) (F : (Fin m → α) → ℝ) (hF : ∀ (w : Fin m → α), 0 ≤ F w) : primitivePairedWordSum mult A F ≤ (∏ a : α, ↑(mult a / 2).factorial) * wordSumFiltered mult NoProperLeafBlock F

Word-level factorial estimate for primitive pairings, with the induced (5.11)(c) word restriction retained on the right.

theorem Anderson4D.primitivePairedWordSum_le_paperSumFiltered {α : Type u_1} [Fintype α] [DecidableEq α] {m : ℕ} (mult : α → ℕ) (A : Finset (Fin m)) (F : (Fin m → α) → ℝ) (hF : ∀ (w : Fin m → α), 0 ≤ F w) : primitivePairedWordSum mult A F ≤ (∏ a : α, ↑(mult a / 2).factorial / ↑(mult a).factorial) * paperSumFiltered mult NoProperLeafBlock F

Filtered (5.10). The exact factorial normalization for primitive pairings, with the word condition (5.11)(c) exposed through paperSumFiltered.