continuumEHScaleExplicitFace_eq
plain-language theorem explainer
The continuum Einstein-Hilbert scale face on a real 4×4 matrix equals minus one-eighth times its squared Frobenius norm. Analysts in the 4D Regge continuum preflight cite this for the frozen Option-C EH coefficient in closed form. The proof is a one-line wrapper of the upstream explicit-scale identity from the exact flat Hessian norm gate.
Claim. For every real $4\times 4$ matrix $E$, the continuum Einstein-Hilbert scale face at $E$ equals $-\frac{1}{8}$ times the squared Frobenius norm of $E$.
background
This module freezes the independent continuum Einstein-Hilbert target for the 4D Regge campaign before any continuum recovery is proved. A real $4\times 4$ matrix is the polarization carrier. Its squared Frobenius norm is $\sum_{i,j} E_{ij}^2$. The continuum EH scale face is a naming-compat alias that feeds that Frobenius quantity into the upstream explicit continuum scale functional from the exact flat Hessian norm gate.
Local contracts fix a canonical periodic Freudenthal 4-torus mesh of side $N\ge 3$, Frobenius-normalized Euclidean TT polarizations, and a linearized EH quadratic defined independently of lattice weights. Banked non-ledger identities record algebraic face values such as this one without inhabiting the geometric continuum Tendsto Props. The module doc stresses that the EH quadratic is frozen first; later closers must observe equality, never fit a scale.
proof idea
One-line term wrapper. It applies the upstream theorem continuumEHScaleExplicit_eq from ReggeExactFlatHessianNormGate4D at the squared Frobenius norm of $E$. That is exactly the body of the local face alias, so the equality reduces immediately with no extra algebra.
why it matters
Four parents consume this face. recognitionExactJConvergesEH_closed closes the Recognition mesh midpoint sequence at the scale-explicit Option-C EH face. typedResidual_m2_optionC_faces uses it for typed residual Option-C faces in SRS convergence. srs_limit_value is the same equality under the preflight name, giving the closed-form value the convergence theorem converges to. continuumFace_polarization_eq_neg_quarter_frobenius rewrites both sides to upgrade $-1/8$ Frobenius into the $-1/4$ polarization pairing.
In the preflight tier tags this is a banked non-ledger algebraic face: discrete bookkeeping $2\cdot(-1/8)=-1/4$ recovers frozen EH without inhabiting geometric Tendsto. Continuum recovery Props and $S_{RS}$ converges EH remain OPEN; this only freezes the coefficient those later theorems aim at.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.