continuumEHunitFrobeniusFromFirstPrinciples
plain-language theorem explainer
The continuum Einstein–Hilbert coefficient on the unit-Frobenius transverse-traceless face is the real constant −1/8, fixed from first principles. Gravity analysts cite it when separating the geometric continuum face from discrete bookkeeping that doubles the coefficient to −1/4. It is a bare real definition, not a derived identity.
Claim. The continuum Einstein–Hilbert coefficient on the unit-Frobenius TT face, taken from first principles, is the real number $-1/8$.
background
This module is the normalization honesty gate for the 4D continuum Einstein–Hilbert (EH) target in the Regge exact-flat Hessian analysis. A historical preflight demanded a frozen TT coefficient of $-1/4$ on unit Frobenius, but the exact algebraic $m^2$ face yields $-1/8$ per unit Frobenius; $-1/4$ is the axis-TT-plus face where $|H|_F^2 = 2$.
Option (C) restates the continuum EH face as scale-explicit: $(-1/8)\cdot|E|F^2$. The discrete bookkeeping identity $2\cdot(-1/8)=-1/4$ recovers the frozen coefficient on unit-Frobenius TT, but is banked only as a non-ledger algebraic fact (EH audit §2.3 / 3D second-difference). It does not inhabit geometric continuum-symbol convergence, ledger $S{RS}$ convergence to 4D EH, or gap-action recovery.
Sibling constants in the module name the frozen preflight EH coefficient, the exact unit-Frobenius TT coefficient, and the discrete bookkeeping factor (equal to two).
proof idea
Bare definition: the real constant is assigned the value $-(1/8)$ with no proof body and no lemmas. Downstream equality with the exact unit-Frobenius TT coefficient is by rfl once both sides are this same numeral.
why it matters
Pins the continuum EH unit-Frobenius face at $-1/8$ so the honesty gate can distinguish geometry from discrete bookkeeping. The immediate parent is continuumEH_unitF_matches_exact_m2, which states that this constant equals the exact unit-Frobenius TT coefficient (proved by reflexivity) and documents the discrete continuum EH face as $2\cdot(-1/8)\cdot|E|_F^2$.
That landing closes restatement option (C) from the 4D SRS-closure session: scale-explicit aliases stay for compatibility, while the $\times 2$ bookkeeping identity is kept off the geometric and ledger convergence paths. Without this constant, frozen preflight $-1/4$ and exact $m^2$ $-1/8$ remain conflated on the unit-Frobenius face.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.