Transmission rows forced by cross-one-off rank differences

This small interface turns an exact value rankDelta = 1 into the corresponding row of a transmission permutation. The geometric calculations are kept in the preceding modules; this file is deliberately purely formal.

theorem Bananas.IsKAffine.row_difference {k : ℕ} {τ : ℤ → ℤ} (hAffine : IsKAffine k τ) {a a' b : ℤ} (hRow : τ b = a) (hRowShift : τ (b + ↑k) = a') : a' = a + ↑k

Comparing two forced rows a period apart. This is the elementary affinity constraint used to rule out candidate short periods.

theorem Bananas.IsKAffine.not_period_of_forced_rows {k : ℕ} {τ : ℤ → ℤ} (hAffine : IsKAffine k τ) {a a' b : ℤ} (hRow : τ b = a) (hRowShift : τ (b + ↑k) = a') (hNe : a' ≠ a + ↑k) : False

A forced pair of rows contradicts a putative affine period whenever their values do not differ by that period.

theorem Bananas.transmission_value_of_rankDelta_eq_one {M : TwiceMarked} {D : CFDiv M.graph} {τ : ℤ → ℤ} (hτ : IsTransmissionPermutation M D τ) {a b : ℤ} (hDelta : rankDelta M (D + a • oneChip M.u - b • oneChip M.v) = 1) : τ b = a

A rank-difference equal to one forces the indicated transmission row.

theorem Bananas.transmission_value_of_linearEquiv_rankDelta_eq_one {M : TwiceMarked} {D E : CFDiv M.graph} {τ : ℤ → ℤ} (hτ : IsTransmissionPermutation M D τ) {a b : ℤ} (hDE : linearEquiv M.graph (D + a • oneChip M.u - b • oneChip M.v) E) (hDelta : rankDelta M E = 1) : τ b = a

Linear equivalence transports a computed second rank difference into a forced transmission row.

theorem Bananas.transmission_crossOneOff_positive_residue {g : ℕ} (B : Banana g) (α β : Fin (g + 1)) (b m r c : ℕ) (τ : ℤ → ℤ) (hg : 2 ≤ g) (hαβ : α ≠ β) (hb : b = m * B.length β + r) (hrLo : 1 ≤ r) (hrHi : r + 1 < B.length β) (hCandidate : b ≤ g + 2 * m + 2) (ha : g + 2 * m + 2 - b ≤ B.length α) (hpLo : 2 ≤ g + 2 * m + 2 - b) (hpHi : g + 2 * m + 2 - b < B.length α) (hc : c ≤ g - 2) (hbm : b ≤ g + m) (hcEq : c = g + m - b) (hτ : IsTransmissionPermutation (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B α ⟨1, ⋯⟩) (strandVertex B β ⟨B.length β - 1, ⋯⟩)) (g • oneChip (rightEndpoint B)) τ) : τ ↑b = ↑(g + 2 * m + 2 - b)

Corrected Lemma 4.30(3), now as a forced transmission row. This is the positive-residue case b = m n_β + r; its candidate is g + 2m - b + 2.

theorem Bananas.transmission_crossOneOff_multiple {g : ℕ} (B : Banana g) (α β : Fin (g + 1)) (b m c : ℕ) (τ : ℤ → ℤ) (hg : 2 ≤ g) (hαβ : α ≠ β) (hb : b = m * B.length β) (hm : 1 ≤ m) (ha : m + 1 < B.length α) (hβLength : 2 ≤ B.length β) (hc : c ≤ g - 1) (hbm : b ≤ g + m) (hcEq : c = g + m - b) (hτ : IsTransmissionPermutation (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B α ⟨1, ⋯⟩) (strandVertex B β ⟨B.length β - 1, ⋯⟩)) (g • oneChip (rightEndpoint B)) τ) : τ ↑b = ↑(m + 1)

Corrected Lemma 4.30(1), as a forced row at a positive multiple of the second marked-strand length.

theorem Bananas.transmission_crossOneOff_complement_residue {g : ℕ} (B : Banana g) (α β : Fin (g + 1)) (b m c : ℕ) (τ : ℤ → ℤ) (hg : 2 ≤ g) (hαβ : α ≠ β) (hm : 1 ≤ m) (hb : b + 1 = m * B.length β) (ha : g + m < B.length α) (hβLength : 2 ≤ B.length β) (hc : c < g - 1) (hcm : m * (B.length β - 1) ≤ g) (hcEq : c = g - m * (B.length β - 1)) (hτ : IsTransmissionPermutation (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B α ⟨1, ⋯⟩) (strandVertex B β ⟨B.length β - 1, ⋯⟩)) (g • oneChip (rightEndpoint B)) τ) : τ ↑b = ↑(g + m)

Corrected Lemma 4.30(2), as a forced row in the complementary-residue case b + 1 = m n_β. The strict normal-form bound excludes exactly the length-two boundary whose rank difference is zero.