eh_target_neg_quarter
plain-language theorem explainer
The independently frozen 4D Einstein–Hilbert transverse-traceless continuum coefficient equals $-1/4$ in the banked conventions. Continuum-limit and algebraic-closer work cites this as the rigid target the lattice symbol must hit without free rescaling. The proof is a one-line term wrapper of the preflight reflexivity lemma.
Claim. The frozen linearized Einstein–Hilbert continuum coefficient on Frobenius-normalized transverse-traceless polarizations in four dimensions equals $-1/4$.
background
This module studies the second variation of 4D Regge calculus about a flat seed, aiming to elevate the nonlinear action to a Schläfli-reduced edge Hessian and compare its Bloch continuum face to continuum GR. In the closed 3D analogue the match is complete; in 4D the flat Freudenthal Schläfli identities are theorems, but full off-flat pathwise elevation remains open.
The quantity here is not extracted from the lattice. It is the independently frozen EH TT coefficient used in the same conventions as the 3D closer: a pure continuum target equal to $-1/4$. Upstream preflight records it as a definition and proves the numerical identity by reflexivity. The Bloch probe direction symbolDir and Frobenius-normalized axis TT polarizations fix the face on which lattice symbols are later evaluated.
Matching is required to be scale-free: the geometry-derived full symbol must attain this value; no free density or incidence factor may be introduced to force agreement.
proof idea
One-line term wrapper. It applies the preflight lemma that unfolds the definition of the frozen coefficient, which is definitionally -(1/4) and therefore holds by reflexivity. No lattice computation or continuum limit is invoked.
why it matters
Pins the rigid continuum target against which every 4D Regge TT symbol face is judged. Module tier tags already record that the candidate reduced Hessian’s Bloch face on normalized axis TT at the standard symbol direction equals $-1/16$, not $-1/4$, while the density-dictionary survivor is already $1$. The residual is therefore Schläfli elevation of the nonlinear action, not another incidence rescale.
Downstream closers and falsifier arithmetic use this equality as the frozen EH benchmark. It does not flip gap-action recovery and does not inhabit the full RS-to-EH 4D convergence statement. Framework-wise it sits in the gravity continuum-limit stack that must eventually recover Einstein–Hilbert structure once the open pathwise Schläfli elevation is closed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.