flatComplex
plain-language theorem explainer
A degenerate bounded complex at dilate N carrying the measured Freudenthal-cube census counts (vertices, edges, tets) while collapsing every incidence onto a single vertex. Downstream work cites it as the concrete carrier that makes the census-dilate hypothesis class non-empty. Construction is field-by-field: plug in census totals, discharge cap bounds by omega, and hard-wire trivial edge/tet maps.
Claim. For each $N \in \mathbb{N}$, there is a bounded complex whose vertex, edge, and tetrahedron counts equal the four-dimensional Freudenthal cube census at dilate $N$, whose counts lie under the flat capacity at $N$, and whose edge and tetrahedron incidence maps send every index to a single fixed vertex.
background
Gap 2 (A1.7) asks whether the letter-cost failures of the J-Ehrhart and oriented-face constructions are accidents of those two referents or a theorem about the Freudenthal carrier. The module answers: any family of bounded complexes whose three kind counts match the measured 4D Freudenthal cube census at every dilate cannot support a letter cost with fixed kind totals whose history is a cubic surface polynomial, except the zero cost.
A BoundedComplex packages three finite counts (vertices, edges, tetrahedra) under a numeric capacity, plus incidence maps naming the endpoints of each edge and the four vertices of each tet. The census functions supply the measured counts at dilate $N$; the flat capacity is a convenient upper bound large enough to host those counts. The present definition builds the simplest possible complex with those counts: incidence is collapsed, so the object is a pure count witness rather than a geometric triangulation.
proof idea
Definitional construction, not a proof. Vertex/edge/tet fields are set to the census values at $N$. The three capacity inequalities are discharged by unfolding the flat capacity and calling omega. Edge incidence is the constant pair of the zero vertex (justified by census positivity); tet incidence is the constant zero vertex. No geometric lemmas are invoked.
why it matters
Feeds flatFamily, the explicit census-dilate family that witnesses non-vacuity of the hypothesis class used throughout the letter-cost dichotomy. Without a concrete family whose counts match the measured Freudenthal census at every dilate, the dichotomy theorems (surface_and_kindTotals_force_zero, surface_and_fixedKindTotals_force_zero_historyCost) would quantify over an empty class. The flat complex is deliberately incidence-free: the dichotomy is about kind totals and surface growth, not about nontrivial topology, so a collapsed carrier is the right minimal witness. It sits inside the Gravity/SevenGaps chain that closes Gap 2 on the Recognition carrier, sharpening earlier kernel results that needed atom normalizations as hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.