discreteExactReggeContinuumFaceCoeff
plain-language theorem explainer
Banked algebraic Einstein-Hilbert continuum face for a 4×4 polarization: the scalar 2·(-1/8)·‖E‖_F². Gravity analysts cite it as the frozen EH target against which Regge mesh symbols are compared. The body is a one-line wrapper applying the discrete EH face functional to the Frobenius squared norm of E.
Claim. For a real $4\times 4$ matrix $E$, the discrete exact Regge continuum face coefficient is the real number $2\cdot(-1/8)\cdot\|E\|_F^2$, obtained by feeding the Frobenius squared norm of $E$ into the banked discrete continuum EH face functional.
background
The module freezes independent continuum targets for the 4D Regge weak-field campaign before any recovery proof. Nothing here claims continuum Tendsto; it only banks algebraic faces and decoys. The Einstein-Hilbert quadratic is frozen independently of lattice weights (via kappa_einstein), so later closers must observe equality rather than fit a scale.
Mat4 is the type of real $4\times 4$ matrices. The local Frobenius squared norm is $|E|F^2=\sum{i,j}E_{ij}^2$. Upstream, the discrete continuum EH face is defined as the product of a bookkeeping factor, the exact unit-Frobenius TT coefficient, and a scalar Frobenius mass; expanded, that product is $2\cdot(-1/8)\cdot|E|_F^2$ (EH audit §2.3). The doc-comment stresses this is a banked algebraic face, not the geometric ContinuumSymbolIs ledger binder.
proof idea
Definitional one-line wrapper. Evaluate the upstream discrete continuum EH face on the local Frobenius squared norm of $E$. No tactics; the algebraic identity $2\cdot(-1/8)\cdot|E|_F^2$ is discharged by the companion equality lemma that unfolds the bookkeeping factors.
why it matters
This name is the preflight's own handle for the frozen EH face. Downstream, the equality lemma restates it as $2\cdot(-1/8)\cdot|E|_F^2$, and SRSConvergesScope4D imports that value as eh_face_value. The scoped convergence verdict uses it twice: the mesh sequence converges to Regge normalization times this face, and (when $|E|_F^2\neq 0$) does not converge to the bare EH face. That separation is the exclusion half of Step 8: the limit exists, is unique, and is the Regge-normalized face, not the raw EH coefficient. It sits in the QG full-theory continuum closure plan as banked non-ledger bookkeeping; the geometric Tendsto props and S_RS_converges_EH_4d remain open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.