trunk contacts from specs

Open

Freiman.trunk_contacts_from_specs

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

algebracontinued-fractionsformalization

The two weak crossed endpoint comparisons and the individual nonempty intervals give each explicitly recorded contact; the three source holes are excluded.

Preamble

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

open Freiman

Formal statement

theorem Freiman.trunk_contacts_from_specs (p : LowerPair) (k : Fin 16) (pi par : ℕ) (hm : TrunkMode p k pi par)
    (hs : ∀ sp ∈ trunkSpecs (trunkPlanAt (trunkCatalog.states k) pi), trunkSpecHolds p sp) :
    ∀ lm ∈ (trunkPlanAt (trunkCatalog.states k) pi).labels.zip (trunkPlanAt (trunkCatalog.states k) pi).labels.tail, lm ∉ (trunkPlanAt (trunkCatalog.states k) pi).holes →
    (lowerCover (lowerChild p lm.1) ∩ lowerCover (lowerChild p lm.2)).Nonempty := 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