cube_body
plain-language theorem explainer
cube_body fixes the body cell count C of the Q_D lattice at the constant value 1. Researchers assembling the cumulative counts N0 through N3' for the 55-cell partition at D=3 cite this constant when verifying the algebraic closure of the cell numbers. The declaration is a direct constant assignment with no further computation.
Claim. The body cell count $C$ of the three-dimensional cube is defined by $C := 1$.
background
The module SectorDependentTorsion proves algebraic properties of the integers {13, 11, 6, 8} as Q3 cell counts and shows that the relation W = 2V + 1 = N0 holds only for D = 3. This supplies a dimension-forcing condition independent of data. cube_body supplies the constant interior term that appears in every cumulative count N_k = 2 S_k + cube_body and in the total-cell identity V + E + F + C = D^D.
proof idea
The declaration is a one-line definition that directly assigns the natural number 1.
why it matters
cube_body is referenced by the definitions N0, N1, N2 and N3' that realize the partition 2D^D + 1 = 55 at D = 3. It is used in the theorem total_cells_eq_D_pow_D establishing V + E + F + C = 27 and in vertex_face_excess. The constant therefore participates in the D = 3 forcing step of the UnifiedForcingChain and in the subsequent mass-ladder constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.