Freiman.lowerEarlyTerminal_opposite_parity_cd
ProvedFreiman.lowerEarlyTerminal_opposite_parity_cdhall-raynumber-theory
Positive words beginning with a digit at least3 and with opposite length parity cannot have the same pair of denominator continuants. Opposite determinant signs would make the sum of their rational convergents an integer strictly between0 and1.
Preamble
import Definitions.Def_Freiman_lowerEarlyTerminalGeometry open Freiman
Formal statement
theorem Freiman.lowerEarlyTerminal_opposite_parity_cd (u v : List ℕ+)
(hu : ∃ a : ℕ+, ∃ w : List ℕ+, u = a::w ∧ 3 ≤ (a:ℕ))
(hv : ∃ a : ℕ+, ∃ w : List ℕ+, v = a::w ∧ 3 ≤ (a:ℕ))
(hp : u.length % 2 ≠ v.length % 2) : lowerCD u ≠ lowerCD v := by
sorrySource
Freiman's Hall ray: Proof report and corrected English text (8 September 2026), pp.120–132, §§ s15:early-residual and s15:terminal-extension; pp.133–139, Proposition l139chain and Appendix app:l139cert. Report continuant determinant identity and the actual lower construction’s first-digit3/4 core restriction.