einsteinHilbertTTCoefficient4D_eq
plain-language theorem explainer
The independently frozen linearized Einstein–Hilbert TT coefficient in 4D equals $-1/4$ by definitional equality. Anyone comparing a Regge lattice symbol, candidate face, or orbit sum against the continuum EH target cites this pin. The proof is pure reflexivity on the frozen definition; no lattice input enters.
Claim. The independently frozen linearized Einstein–Hilbert transverse-traceless continuum coefficient in four dimensions equals $-1/4$.
background
This module is the first binding increment of the 4D continuum closure plan in the QG full-theory campaign. It freezes the independent continuum target, canonical mesh carrier, normalized TT data, pure-gauge family, and honesty decoys before further computation. Nothing here proves continuum recovery.
The coefficient itself is defined as $-(1/4)$, matching the closed 3D closer conventions. It is a definition, not a lattice-derived value: the later algebraic closer must observe that the geometry-derived full symbol attains it and must not introduce a free scale to force the match. The continuum EH quadratic on a Frobenius-normalized TT polarization is this constant times the Frobenius pin (already 1 on TT polarizations), with coupling kappa_einstein recorded as the Recognition field-equation constant.
Upstream, the same frozen value appears in the exact flat Hessian symbol module under the banked axisTTPlus / Preflight convention, again as $-(1/4)$.
proof idea
One-line reflexivity (rfl). The declaration unfolds the definition of the frozen coefficient, which is literally $-(1/4)$, and closes by definitional equality. No lemmas, rewrites, or arithmetic tactics are required.
why it matters
This pin is the frozen EH target that every 4D algebraic closer and falsifier compares against. Downstream, the algebraic closer re-exports it as the frozen coefficient value and uses it in honesty statements: banked one-orbit identities do not inhabit the OPEN isotropy target, and the ledger flag stays false (the m2 symbol on axisTTPlus is unequal to this coefficient). Full TT isotropy convenience lemmas package the equality with the continuum EH target.
In flat second-variation work it supplies the EH side of falsifier arithmetic: the candidate continuum face on normalized TT is $-1/16$, which is not $-1/4$, while the density dictionary survivor remains 1. The tensor algebraic closer records the residual factor-of-four identity $-1/4 = 4 \cdot (-1/16)$ against the distinct-hinge pinned moment. Transported and torus continuum modules likewise use the pin to separate decoy faces from the EH coefficient.
Framework role: it enforces the preflight contract that the EH quadratic is frozen independently of the lattice symbol, so continuum recovery (still OPEN: Tendsto props uninhabited, gap action recovery false) cannot reverse-engineer lattice weights from the answer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.