NormalizationGatePass
plain-language theorem explainer
Boolean honesty gate for the 4D continuum Einstein–Hilbert normalization, fixed to true under the landed scale-explicit restatement. Gravity auditors and Regge–Bloch symbol packages cite it to record that the historical unit-Frobenius coefficient clash is closed without claiming ledger convergence. The body is the constant true; companion theorems discharge equality by rfl.
Claim. The 4D continuum Einstein–Hilbert normalization honesty gate evaluates to $\mathsf{true}$. Under the scale-explicit restatement, the continuum EH face is $(-1/8)\,\|E\|_F^2$ per unit Frobenius (not the frozen preflight value $-1/4$), and the gate records that this accounting is accepted.
background
The module is the normalization honesty gate for the 4D continuum EH target in the Regge exact-flat Hessian analysis. A historical FAIL (session 4d-srs-closure) arose because preflight demanded the frozen coefficient $-1/4$ on unit-Frobenius transverse-traceless modes, while the exact algebraic mass-squared face is $-1/8$ per unit Frobenius; $-1/4$ is the axis-TT-plus face where $|H|_F^2=2$.
Restatement option (C) landed: the continuum EH face is written scale-explicitly as $(-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 ttSecondDifference). It does not inhabit geometric ContinuumSymbolIs Tendsto, does not inhabit the ledger $S{\mathrm{RS}}$ converges to EH in 4D, and does not flip 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
One-line definition: the gate is the Boolean constant true. No lemmas are applied. The companion theorem normalizationGatePass_true is rfl against that definition. Downstream packages conjoin the gate with coefficient identities (unit-Frobenius EH equals exact face; frozen equals bookkeeping times unit-Frobenius) rather than re-proving the flag.
why it matters
Marks closure of the 4D EH normalization honesty check after option-C restatement, so audit packages can assert the gate without reopening the $-1/4$ vs $-1/8$ clash. Downstream: gate_passes_under_restatement_C and gate_passes_with_discrete_bookkeeping package the flag with the unit-Frobenius and bookkeeping identities; bloch_symbol_audit_package and norm_gate_audit_package include NormalizationGatePass = true in their audit conjunctions; exact_unit_coefficient_is_the_regge_face ties the banked $-1/8$ to the discrete Regge face.
In the Recognition gravity stack this is bookkeeping hygiene for the continuum EH target of the Regge exact-flat Hessian, not a forcing-chain (T0–T8) step. It deliberately leaves specialized Tendsto, SRS inhabitation, and gap-action recovery false in the Bloch audit, so the gate does not pretend continuum or ledger closure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.