trunk endpoint transfer

Open

Freiman.trunk_endpoint_transfer

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

algebracontinued-fractionsformalization

Choose the two actual endpoint branches; their exact source comparison gives the requested physical endpoint inequality, with the common odd sign retained.

Preamble

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

open Freiman

Formal statement

theorem Freiman.trunk_endpoint_transfer (he : TrunkEndpointLaw) (hg : TrunkGreaterLaw)
    (p : LowerPair) (k : Fin 16) (hf : lowerHistoryContextFits (lowerNormalize p) (trunkCatalog.states k).context)
    (sp : Section14Spec)
    (hs : ∀ b ∈ trunkBranches (trunkCatalog.states k).context sp,
      trunkHolds b.1 (lowerRatio (lowerNormalize p).1) (lowerRatio (lowerNormalize p).2) (lowerScale (lowerNormalize p)) →
      lowerHistoryComparisonHolds b.2 (lowerRatio (lowerNormalize p).1) (lowerRatio (lowerNormalize p).2) (lowerScale (lowerNormalize p))) :
    trunkSpecHolds p sp := 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