trunk parent mode

Open

Freiman.trunk_parent_mode

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

algebracontinued-fractionsformalization

Parent goodness supplies both actual weak cross-contact branches; normalization and positive denominator scale supply HN and Zero, and finite deduplication preserves this conjunction.

Preamble

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

open Freiman

Formal statement

theorem Freiman.trunk_parent_mode (t : ℝ) (p : LowerPair) (hs : lowerState t p) (k : Fin 16)
    (hf : lowerHistoryContextFits (lowerNormalize p) (trunkCatalog.states k).context) :
    ∃ par : ℕ, par < (trunkParents (trunkCatalog.states k).context).length ∧
    trunkHolds ((trunkParents (trunkCatalog.states k).context)[par]?.getD [])
      (lowerRatio (lowerNormalize p).1) (lowerRatio (lowerNormalize p).2) (lowerScale (lowerNormalize p)) := 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