Freiman.lowerEarlyTerminal_ratio_append
ProvedFreiman.lowerEarlyTerminal_ratio_appendhall-raynumber-theory
Appending a positive-digit suffix updates the denominator ratio by the reversed-suffix continued-fraction map.
Preamble
import Definitions.Def_Freiman_lowerEarlyTerminalGeometry open Freiman
Formal statement
theorem Freiman.lowerEarlyTerminal_ratio_append (u v : List ℕ+) : lowerRatio (u++v) = prefixEval v.reverse (lowerRatio u) := by sorry
Source
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 matrix formula; lowerCD fold recurrence.