continuumEHScaleExplicit_axisTTPlus_face
plain-language theorem explainer
Evaluating the scale-explicit continuum Einstein–Hilbert face at Frobenius square 2 recovers the frozen preflight coefficient −1/4. Gravity auditors cite this when reconciling the unit-Frobenius −1/8 face with the historical axisTTPlus convention. The proof is pure unfolding plus numeric normalization: (−1/8)·2 = −1/4.
Claim. The scale-explicit continuum Einstein–Hilbert coefficient at Frobenius square $2$ equals the frozen preflight EH coefficient: $\mathrm{continuumEHScaleExplicit}(2) = -1/4$.
background
This module is the normalization honesty gate for the 4D continuum Einstein–Hilbert target. A historical preflight freeze set the linearized EH TT coefficient to $-1/4$ (same convention as the closed 3D closer). Exact algebraic $m^2$ on a unit-Frobenius TT polarization instead yields $-1/8$. The mismatch is geometric: the axisTTPlus face has Frobenius-norm squared equal to 2, so $(-1/8)\cdot 2 = -1/4$.
Option C restates the continuum EH face as scale-explicit: unit-Frobenius coefficient times the Frobenius square. The scale-explicit alias multiplies $-1/8$ by a supplied Frobenius square. The frozen preflight coefficient is just the independently frozen definition $-1/4$, not a lattice-derived value. Discrete bookkeeping $\times 2$ is banked only as a non-ledger algebraic identity; it does not inhabit geometric continuum-symbol convergence or the RS ledger action-recovery gap.
proof idea
One-line arithmetic after unfolding. Expand the scale-explicit face to (unit-Frobenius coefficient) times the argument, substitute unit-Frobenius $= -1/8$ and frozen preflight $= -1/4$, then norm_num discharges $(-1/8)\cdot 2 = -1/4$. No external lemmas beyond the four local definitions.
why it matters
Closes the axisTTPlus face of the Option-C restatement in the 4D Regge exact-flat Hessian norm gate. After session 4d-srs-closure failed by demanding frozen $-1/4$ on unit Frobenius, this identity records that the frozen coefficient is exactly the scale-explicit face at $|H|_F^2 = 2$. Downstream ledger claims (S_RS_converges_EH_4d, gap_action_recovery, ContinuumSymbolIs Tendsto) deliberately do not absorb the $\times 2$ bookkeeping; the theorem keeps that factor as a compatibility alias only (EH audit §2.3 / 3D ttSecondDifference parallel). No used-by edges yet; it is a local honesty certificate inside the gravity analysis stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.