continuumEHScaleExplicitFace
plain-language theorem explainer
Scale-explicit continuum Einstein-Hilbert face on a 4×4 polarization: multiplies the frozen unit-Frobenius EH TT coefficient by the Frobenius squared norm of E. Continuum-target Props and Recognition-mesh bridges cite it as the Option-C right-hand side. One-line wrapper of the scalar continuum scale map on Frobenius norm squared.
Claim. For a real $4\times 4$ matrix $E$, define the scale-explicit continuum EH face by $C(E) := c_{\mathrm{EH}}\,\|E\|_F^2$, where $c_{\mathrm{EH}}$ is the unit-Frobenius Einstein-Hilbert TT coefficient and $\|E\|_F^2=\sum_{i,j}E_{ij}^2$. Equivalently $C(E)=(-1/8)\|E\|_F^2$.
background
This module freezes the independent continuum EH target, canonical Freudenthal 4-torus mesh, normalized TT data, and honesty decoys before any continuum-recovery proof. Nothing here proves Tendsto recovery; the EH quadratic is fixed via kappa_einstein, not fitted from lattice weights.
Mat4 is a real $4\times 4$ matrix. The local Frobenius squared norm is $\sum_{i,j} E_{ij}^2$. Upstream, the scalar map continuumEHScaleExplicit multiplies a Frobenius-squared input by the unit-Frobenius EH TT coefficient (compat Option-C naming, not the ledger continuum-symbol binder). The sibling equality theorem records that coefficient as $-1/8$.
Option C is the scale-explicit unit-F face used as the frozen continuum RHS on TT polarizations after $|k|^2$ normalization.
proof idea
Definitional one-line wrapper: evaluate the upstream scalar continuum scale map on the Frobenius squared norm of the matrix argument. No tactics; pure composition of frobeniusNormSq with continuumEHScaleExplicit.
why it matters
Names the frozen Option-C continuum face that open targets must hit. Regge4DContinuumEHTarget asserts that the continuum symbol equals this face on every nonzero integer mode and TT polarization (Restatement C). Recognition-mesh bridges use it as the limit value in RecognitionExactJConvergesEH and as the RHS of FactorizedMomentEqualsEH; the closed theorem recognitionExactJConvergesEH_closed and the residual typed faces in SRSConvergesEH4D also reference it.
In the QG campaign this is the independent continuum anchor: later algebraic closers must observe equality to $(-1/8)|E|_F^2$, never reverse-engineer a scale. It sits in the preflight layer that separates MODEL/DEFINITION objects from OPEN Tendsto Props (S_RS_converges_EH_4d still uninhabited).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.