A rigorously separated inversion block for cross-one-off markings

The ordinary inversions counted here have first coordinate below k by an explicit hypothesis. This is the period-separation condition missing from the printed proof of Corollary 4.31.

noncomputable def Bananas.shiftedEndpointPairEmbedding (lo length : ℕ) : Sym2 (Fin length) → ℤ × ℤ

Translate the standard pair embedding into a natural interval beginning at lo.

Equations

• Bananas.shiftedEndpointPairEmbedding lo length x = ((Bananas.endpointPairEmbedding length x).1 + ↑lo, (Bananas.endpointPairEmbedding length x).2 + ↑lo)

theorem Bananas.shiftedEndpointPairEmbedding_injective (lo length : ℕ) : Function.Injective (shiftedEndpointPairEmbedding lo length)

theorem Bananas.shifted_decreasing_block_inversion_lower_bound {lo length value k : ℕ} {tau : ℤ → ℤ} (hValue : length ≤ value) (hSeparate : lo + length < k) (hBlock : ∀ i ≤ length, tau (↑lo + ↑i) = ↑(value - i)) (hfinite : (kInversions k tau).Finite) : (length + 1).choose 2 ≤ kInversionCount k tau

A shifted decreasing block contributes all of its ordinary inversions to the normalized k-inversion set, provided the block's possible first coordinates lie in [0,k).

theorem Bananas.transmission_crossOneOff_simple_block {g : ℕ} (B : Banana g) (alpha beta : Fin (g + 1)) (tau : ℤ → ℤ) (hg : 3 ≤ g) (hab : alpha ≠ beta) (hAlpha : 1 < B.length alpha) (hBetaLong : g + 1 ≤ B.length beta) (hLong : CrossOneOffLongEnough g (B.length alpha) (B.length beta)) (hTau : IsTransmissionPermutation (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B alpha ⟨1, ⋯⟩) (strandVertex B beta ⟨B.length beta - 1, ⋯⟩)) (g • oneChip (rightEndpoint B)) tau) (i : ℕ) : i ≤ g - 3 → tau ↑(2 + i) = ↑(g - i)

In the long-second-strand regime, corrected Lemma 4.30 restricts to the simple decreasing block tau(2+i)=g-i for 0 ≤ i ≤ g-3.

theorem Bananas.crossOneOff_simple_inversion_lower_bound {g k : ℕ} (B : Banana g) (alpha beta : Fin (g + 1)) (tau : ℤ → ℤ) (hg : 3 ≤ g) (hab : alpha ≠ beta) (hAlpha : 1 < B.length alpha) (hBetaLong : g + 1 ≤ B.length beta) (hLong : CrossOneOffLongEnough g (B.length alpha) (B.length beta)) (hTau : IsTransmissionPermutation (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B alpha ⟨1, ⋯⟩) (strandVertex B beta ⟨B.length beta - 1, ⋯⟩)) (g • oneChip (rightEndpoint B)) tau) (hSeparate : g ≤ k) (hfinite : (kInversions k tau).Finite) : (g - 2).choose 2 ≤ kInversionCount k tau

Corollary 4.29's decreasing-block count, with the period separation made explicit. The hypothesis g ≤ k is sufficient because every first coordinate in the injected family is at most g-2.

This deliberately does not claim the stronger corrected Corollary 4.31 count, whose rows extend to crossOneOffCutoff and require the additional unproved separation crossOneOffCutoff g n ≤ k.