SchlaefliCommonNumeratorTarget
plain-language theorem explainer
Names the residual algebraic target for the closed tetrahedral Schläfli package: after radical normalization, the common numerator of the six rationalized summands must vanish for every squared-edge 6-tuple and every edge index. Geometers working the Cayley–Menger route to a local Schläfli identity would cite it. It is a pure Prop abbreviation, not a proof.
Claim. The residual common-numerator target asserts: for every assignment $a$ of six squared edge lengths of a tetrahedron and every edge index $k\in\{0,\ldots,5\}$, the cleared common numerator of the six rationalized Schläfli summands vanishes, i.e. $\sum_{e} N_{e,k}(a)\prod_{j\neq e} D_j(a)=0$.
background
This module packages the closed-form tetrahedral Schläfli target: explicit Cayley–Menger and dihedral derivative values are wired into a local Schläfli identity so the remaining work is one algebraic identity rather than an external analytic field.
Squared edge data live in SqEdges ($\mathrm{Fin},6\to\mathbb{R}$). Each rationalized summand schlaefliPolySummandNorm is the pure rational expression obtained after removing the arccos radical via the cofactor discriminant; up to the common nonzero factor $1/\sqrt{2,\mathrm{cm}_3(a)}$, it matches the original polynomial-cofactor summand. The common numerator schlaefliCommonNumerator clears all six denominators at once: it sums, over edges $e$, the numerator of summand $(e,k)$ times the product of the other five denominators.
The target Prop simply demands that this common numerator is identically zero in every edge coordinate $k$.
proof idea
No proof: this is a definition of a Prop. The module comment states the intended discharge path: expand each schlaefliPolySummandNorm, clear the cofactor-product denominators, and finish with ring_nf, preferably via six coordinate-specific numerator lemmas rather than one global unfold. Sibling closed-form derivative and equation declarations in the same file supply the surrounding analytic scaffolding.
why it matters
In the Recognition geometry stack, the local tetrahedral Schläfli identity is the hinge that turns Cayley–Menger polynomials and dihedral derivatives into a closed algebraic package usable by discrete gravity and Regge-type analyses. Naming the residual common-numerator vanishing condition isolates the last post-radical algebraic obligation: once it holds, the rationalized six-edge Schläfli identities are finished. No downstream consumers are wired yet (used_by is empty), so this declaration is the explicit open target rather than a lemma already feeding a parent theorem. It does not itself invoke the forcing chain (T0–T8), but it sits in the geometric layer those continuum limits eventually rest on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.