Prove2Me

trunk join bindings 15

Open
Freiman.trunk_join_bindings_15

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

algebracontinued-fractionsformalization

Finite list indexing joins this state’s disjoint record-binding batches.

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

open Freiman
Formal statement
theorem Freiman.trunk_join_bindings_15 (h0 : trunkBindingBatch 15 0 100) (h1 : trunkBindingBatch 15 100 110) :
    ∀ g ∈ (trunkCatalog.states 15).groups, trunkGroupValid trunkCatalog 15 g := 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