sqEdgeRat
plain-language theorem explainer
Rational lookup table for the six squared edge lengths of a Freudenthal tetrahedron in the cube triangulation: the values 1,2,3,1,2,1 on Fin 6. Gravity and discrete-geometry auditors cite it as the exact-arithmetic stand-in for freudenthalTetSqEdges. It is a pure case definition with no proof obligations.
Claim. Define a map from the six edge slots $\{0,\ldots,5\}$ into $\mathbb{Q}$ by $0\mapsto 1$, $1\mapsto 2$, $2\mapsto 3$, $3\mapsto 1$, $4\mapsto 2$, $5\mapsto 1$. These are the squared Euclidean lengths of the six edges of a Freudenthal tetrahedron in the unit-cube triangulation, kept as rationals for exact coefficient arithmetic.
background
The module certifies corrected Freudenthal axis-stencil coefficients for the $N=5$ mixed explicit-fiber residual. It mirrors a Python rational audit and never uses floating point: every coefficient of an unordered monomial $\xi(u)\xi(v)$ is checked exactly.
A Freudenthal triangulation decomposes the unit cube into tetrahedra whose edge set has six combinatorial slots. The squared lengths of those edges are the integers 1, 2, and 3 (with multiplicity). Keeping them as rationals lets later stencil atoms multiply and sum without leaving $\mathbb{Q}$.
Sibling infrastructure supplies the five-vertex periodic lattice (Vertex5, PeriodicEdge5) and the local pair/cell geometry used by the scaled pair coefficient atoms that consume this table.
proof idea
Pure definition by six pattern-match arms on Fin 6. No tactics, no lemmas, no computation beyond the literal rational constants.
why it matters
This table is the rational backbone of the axis-stencil coefficient certificate. Downstream, scaledPairLocalVertexCoeff multiplies by these values when building endpoint-local atoms; the expansion theorems scaledPairLocalVertexCoeffExpansionAtN5 and scaledPairLocalVertexCoeffEndpointSumExpansionAtN5 push those atoms into unordered monomials of the $N=5$ residual; scaledPairEndpointExpansionValueAtN5 evaluates the closed form. The bridge theorem sqEdgeRat_cast_eq_freudenthalTetSqEdges shows that casting each entry to $\mathbb{R}$ recovers the geometric freudenthalTetSqEdges table, so the rational audit matches the continuous Freudenthal geometry used elsewhere in the gravity stack.
In the broader Recognition framework this sits in the discrete gravity / lattice-stencil layer that supports continuum limits on the recognition lattice, not in the T0–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.