trunk bindings 12 100 178
ProvedFreiman.trunk_bindings_12_100_178algebracontinued-fractionsformalization
State ['31', '1'], grouped rows 100–177: exact source branch indices, every parent index, witness-bound membership and rectangle/subrectangle binding.
Preamble
import Definitions.Def_Freiman_trunkGeometry import Mathlib.Tactic.FinCases import Mathlib.Tactic.Linarith open Freiman
Formal statement
theorem Freiman.trunk_bindings_12_100_178 :
trunkBindingBatch 12 100 178 := by
sorrySource
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.