trunk early plan

Open

Freiman.trunk_early_plan

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

algebracontinued-fractionsformalization

H9-notH16 is the precise original eight-row source plan; all cutoff weak/strict directions, suffix classification and anchor labels are explicit.

Preamble

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

open Freiman

Formal statement

theorem Freiman.trunk_early_plan (t : ℝ) (p : LowerPair) (hs : lowerState t p) (hd : lowerEarlyDomain p) (k : Fin 16)
    (hf : lowerHistoryContextFits (lowerNormalize p) (trunkCatalog.states k).context) :
    ∃ pi : ℕ, pi < (trunkSourcePlans (trunkCatalog.states k).context).length ∧
    trunkHolds (trunkPlanAt (trunkCatalog.states k) pi).cuts (lowerRatio (lowerNormalize p).1) (lowerRatio (lowerNormalize p).2) (lowerScale (lowerNormalize p)) ∧
    ([3],[2]) ∈ (trunkPlanAt (trunkCatalog.states k) pi).labels ∧ ([2],[2]) ∈ (trunkPlanAt (trunkCatalog.states k) pi).labels ∧ (trunkPlanAt (trunkCatalog.states k) pi).labels.getLast? = some ([3],[2]) := 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