module module high

`IndisputableMonolith.Gravity.FreudenthalLengthChainEndpointCert`

Certifies the fully evaluated rationalized Schläfli summand table on the squared edge lengths of the Freudenthal six-tetrahedron cube. Gravity workers cite it when assembling the physical six-tet cubic Dirichlet model on a periodic torus. The module is a finite table of squared-norm identities, one per summand index, not a deep existence argument.

claimOn the squared edge lengths of the Freudenthal six-tetrahedron decomposition of the unit cube, each rationalized Schläfli summand has an explicitly evaluated squared norm; the module records that finite table of values.

background

The Freudenthal triangulation splits the unit cube into six tetrahedra along the body diagonal from vertex $0$ to vertex $7$, with cube vertices labeled by binary coordinates. That incidence bookkeeping is fixed upstream in the Freudenthal cube triangulation module.

The Schläfli side supplies the local tetrahedral package: Cayley–Menger data and dihedral derivatives are reduced to a single closed-form identity rather than an external field. The present module sits at the join of those two strands. It evaluates the rationalized Schläfli summands at the concrete squared edge lengths of the Freudenthal tets, producing a lookup table of squared norms indexed by summand.

Sibling lemmas name the individual table entries (vanishing and non-vanishing squared norms at each index). The gravity domain uses this table as certified numeric input, not as a geometric existence proof.

proof idea

Definition-and-table module. It fixes the evaluation point at the Freudenthal tet squared edges, then discharges a finite family of squared-norm identities (the snorm_* siblings) by direct computation against the closed-form Schläfli package. No global geometric theorem is proved here; each entry is a concrete rational or zero identity at a fixed multi-index.

why it matters in Recognition Science

Feeds PhysicalSixTetCubicDirichletInstance, which packages the exact theorem obligations needed to instantiate the physical six-tet cubic Dirichlet model on a periodic Freudenthal torus. That downstream module explicitly does not assert the physical Dirichlet equality for free; it needs certified edge and summand data of the kind this table supplies.

In the broader RS gravity stack, the six-tet cube is the discrete cell on which Dirichlet-type length and curvature bookkeeping is stated. Closing the Schläfli summand norms at the Freudenthal edges removes one numeric gap between pure geometry (Freudenthal incidence, Schläfli closed form) and the physical model instance. It does not by itself force $D=3$ or the eight-tick octave; those sit earlier in the forcing chain.

scope and limits

Does not prove the physical six-tet cubic Dirichlet equality.
Does not derive the Freudenthal incidence structure; that is imported.
Does not re-prove the closed-form Schläfli identity; only evaluates summands.
Does not address continuum limits or non-cubic lattices.
Does not certify values off the Freudenthal squared-edge point.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Gravity.PhysicalSixTetCubicDirichletInstance module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Geometry.FreudenthalCubeTriangulation module_import
IndisputableMonolith.Geometry.SchlaefliTetrahedronProof module_import

declarations in this module (39)

def freudenthalSchlaefliPolySummandNormTable L24
theorem snorm_zero_0_0 L64
theorem snorm_zero_0_1 L72
theorem snorm_zero_0_2 L80
theorem snorm_zero_0_3 L88
theorem snorm_0_4 L96
theorem snorm_0_5 L104
theorem snorm_zero_1_0 L112
theorem snorm_1_1 L120
theorem snorm_1_2 L128
theorem snorm_1_3 L136
theorem snorm_1_4 L144
theorem snorm_1_5 L152
theorem snorm_zero_2_0 L160
theorem snorm_2_1 L168
theorem snorm_2_2 L176
theorem snorm_2_3 L184
theorem snorm_2_4 L192
theorem snorm_zero_2_5 L200
theorem snorm_zero_3_0 L208
theorem snorm_3_1 L216
theorem snorm_3_2 L224
theorem snorm_3_3 L232
theorem snorm_3_4 L240
theorem snorm_zero_3_5 L248
theorem snorm_4_0 L256
theorem snorm_4_1 L264
theorem snorm_4_2 L272
theorem snorm_4_3 L280
theorem snorm_4_4 L288
theorem snorm_zero_4_5 L296
theorem snorm_5_0 L304
theorem snorm_5_1 L312
theorem snorm_zero_5_2 L320
theorem snorm_zero_5_3 L328
theorem snorm_zero_5_4 L336
theorem snorm_zero_5_5 L344
theorem freudenthalSchlaefliPolySummandNorm_eq_table L353
theorem freudenthalDihedralClosedDerivLength_snorm L395