Freiman.lowerEarlyTerminal_width_tie_ratios
ProvedFreiman.lowerEarlyTerminal_width_tie_ratioshall-raynumber-theory
An exact full-width tie has only the two stated continuant-ratio alternatives.
Preamble
import Definitions.Def_Freiman_lowerEarlyTerminalGeometry open Freiman
Formal statement
theorem Freiman.lowerEarlyTerminal_width_tie_ratios (u v : List ℕ+) (h : lowerWidth u = lowerWidth v) : lowerRatio u = lowerRatio v ∨
lowerRatio v = (4-3*lowerRatio u)/(3+4*lowerRatio u) := 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.