normalizationGatePass_true
plain-language theorem explainer
The 4D continuum Einstein–Hilbert normalization honesty gate is recorded as passing. Gravity auditors and anyone assembling the Regge flat-Hessian Bloch or norm-gate packages cite it as the boolean certificate that restatement option C is in force. The proof is pure reflexivity: the gate definition is the constant true.
Claim. The normalization honesty gate for the 4D continuum Einstein–Hilbert target evaluates to $\mathrm{true}$.
background
This module records a normalization honesty gate for the 4D continuum Einstein–Hilbert (EH) target on the exact flat Regge Hessian. A historical preflight failure demanded the frozen coefficient $-1/4$ on unit-Frobenius transverse-traceless (TT) modes, while the exact algebraic mass-squared face yields $-1/8$ per unit Frobenius; the value $-1/4$ is the axis-TT-plus face with squared Frobenius norm $2$.
Restatement option C fixes the continuum EH face as the scale-explicit form $(-1/8)\cdot|E|_F^2$. The factor-of-two 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 identity. It does not inhabit geometric continuum-symbol convergence, the RS ledger convergence statement, or gap-action recovery.
The gate itself is the boolean NormalizationGatePass, defined as the constant true once option C is landed.
proof idea
One-line reflexivity. The gate is defined as the boolean constant true, so rfl discharges equality to true with no lemmas and no computation.
why it matters
This boolean is the shared certificate that the 4D EH normalization restatement is active. Downstream, gate_passes_under_restatement_C pairs it with equality of the unit-Frobenius EH coefficient to the exact algebraic value; gate_passes_with_discrete_bookkeeping pairs it with the factor-two identity recovering the frozen preflight coefficient and the discrete-face evaluation. Both the Bloch-symbol audit package and the norm-gate audit package conjoin it as a required true flag alongside coupling-table size, specialized-tendsto status, and the explicit non-claims that SRS is uninhabited and gap-action recovery remains false.
In the broader Recognition gravity stack it marks closure of the honesty gate after the historical unit-Frobenius mismatch, without pretending continuum or ledger recovery has been flipped.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.