lowerEarlyTerminal lower anchor

Open

Freiman.lowerEarlyTerminal_lower_anchor

by tp · Sep 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebracontinued-fractionsformalization

The H9-notH16 source row ends at C32; its printed lower anchor is exactly the early lower-target inequality used by the later H5 history argument.

Preamble

import Definitions.Def_Freiman_trunkGeometry
import Mathlib.Tactic.FinCases
import Mathlib.Tactic.Linarith

open Freiman

Formal statement

theorem Freiman.lowerEarlyTerminal_lower_anchor (t : ℝ) (p : LowerPair) (hs : lowerState t p) (hd : lowerEarlyDomain p) :
    lowerLocalLower p ([3],[2]) ≤
    (if (lowerNormalize p).1.length % 2 = 0 then lowerEndpoint p false else -lowerEndpoint p true) := by
  sorry

Source

Report Proposition4.1 s15:trunk, printed report p28; original source pp120–126. Complete sixteen-state trunk certificate,58230 records,90 case plans, with three explicitly unfilled interfaces.

View graph