schlaefliN_interface_ready
plain-language theorem explainer
Once 10-hinge, 10-edge Schläfli derivative data satisfy the n-dimensional Schläfli identity, the measure-weighted sum of dihedral-angle derivatives vanishes on every edge coordinate. Gravity analysts wiring the 4D Regge flat second-variation elevation cite this as the typed interface that kills the angle term. The proof is a one-line specialization of the generic angle-term eliminator to size (10,10).
Claim. Let $D$ be Schläfli derivative data with 10 hinges and 10 edge-length coordinates, and suppose $D$ obeys the $n$-dimensional Schläfli identity $\sum_h V_{n-2}(h)\,\partial\theta_h/\partial L_e=0$ for every edge $e$. Then for each edge index $e\in\{1,\ldots,10\}$, $\sum_{h=1}^{10} (\mathrm{measure\ of\ hinge\ }h)\cdot(\partial\theta_h/\partial L_e)=0$.
background
In Regge calculus the first variation of deficit-angle action is controlled by the classical Schläfli identity: hinge $(n-2)$-volumes times dihedral-angle derivatives sum to zero along every edge length. The structure SchlaefliDataN nH nE packages finitely many hinges (each carrying a measure) together with the Jacobian matrix $\partial\theta_h/\partial L_e$. The proposition SchlaefliIdentityN is exactly that column-sum identity for every edge.
This module mirrors the 3D contract in which Gate A2 elevates the true nonlinear Regge action to a Schläfli-reduced edge Hessian. In 3D that elevation is closed. In 4D the flat-seed Freudenthal closed form and flat directional Schläfli kill are already theorems pathwise; the residual open obligation is full off-flat pathwise Schläfli, hence elevation of the nonlinear action.
Upstream, schlaefliN_kills_angle_term is the direct eliminator: given any-size data and the identity hypothesis, it returns the vanishing sum for a chosen edge. The present declaration simply pins the interface sizes to the 4D Freudenthal bookkeeping (10 hinges, 10 edges).
proof idea
One-line term proof: apply the generic eliminator schlaefliN_kills_angle_term at the supplied data $D$, identity hypothesis, and edge $e$. No extra algebra; the identity proposition is definitionally the claimed sum.
why it matters
Gate A2 in the 4D Regge flat second-variation program needs a typed hook that, once a concrete Freudenthal Schläfli witness exists, erases the angle column from the second variation and leaves only the candidate reduced Hessian. This theorem is that hook at the (10,10) interface used by the flat Freudenthal pathwise results already proved in Regge4DSchlaefliPathwise.
It does not itself close elevation: the module doc marks full off-flat Freudenthal4SimplexPathwiseSchlaefli and therefore Regge4DSchlafliElevationToCandidate as OPEN. Prior alternative paths (distinct-hinge fold, full two-jet, mean-local Path B, density dictionary) already fail to repair the continuum face mismatch, so the residual really is Schläfli elevation of the nonlinear action. No downstream consumers are wired yet; the declaration is interface readiness only, as the doc-comment states. It does not flip gap_action_recovery and does not inhabit continuum EH convergence in 4D.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.