DistinctHingePinnedMomentVsEH
plain-language theorem explainer
Records the arithmetic mismatch between the continuum-facing distinct-hinge pinned moment (−1/16) and the frozen Einstein–Hilbert TT coefficient (−1/4). Gravity continuum-limit and algebraic-closer arguments cite it to keep the residual factor-of-four explicit. The body is a bare inequality of two real constants.
Claim. The proposition that $-1/16 \neq c_{\mathrm{EH}}$, where $c_{\mathrm{EH}}$ is the independently frozen linearized Einstein–Hilbert TT continuum coefficient (equal to $-1/4$ in the same Frobenius-normalized conventions).
background
This module treats the 4D torus continuum limit for a finite periodic Freudenthal action on side $N=j+3$, with $N^4$ sites and density weight $N^{-4}$. The bookkeeping parallels the closed 3D path: the second-difference density factor $(2/N^4)$ times the cell-sum cosine identity $N^4/2$ cancels to 1, so the canonical finite Hessian equals the distinct-hinge Bloch fold once Schläfli elevation and the 4D cell-sum identity are closed.
Axis arithmetic (measured externally) gives a distinct-hinge raw $m^2$ of $-1/4$ on the axis TT-plus / symbol direction. Dividing by $|\mathrm{dir}|^2=2$ and applying the Frobenius pin $1/2$ produces the continuum-facing coefficient $-1/16$. The Einstein–Hilbert target is frozen independently as $c_{\mathrm{EH}}=-(1/4)$ and is not lattice-derived; later closers must attain it without a free rescale.
The surviving density-dictionary factor is 1, so it cannot cancel the residual factor 4 between $-1/16$ and $-1/4$.
proof idea
Definitional wrapper: the proposition is literally the real inequality $(-1/16)\neq c_{\mathrm{EH}}$, with $c_{\mathrm{EH}}$ the frozen EH TT coefficient from the continuum preflight (and the matching banked symbol module). No tactics; discharge is deferred to the one-line theorem that unfolds this name, rewrites the EH coefficient, and closes by norm_num.
why it matters
Pins the honesty ledger for the 4D torus continuum path. Downstream, residual_factor_four_arithmetic packages the identity $c_{\mathrm{EH}}=4\cdot(-1/16)$ together with this mismatch and the surviving dictionary factor 1, making the residual factor four an explicit theorem rather than a fitted rescale. The companion honesty theorem records that the dictionary alone does not inhabit the EH continuum target and does not flip gap_action_recovery.
In the module status, continuum Tendsto still binds to the Option-C midpoint trig-poly mesh sequence; this definition keeps the legacy distinct-hinge fold from silently claiming EH recovery. It does not close the open 4D cosine cell-sum identity or the residual star-member offsets on non-$t_{11}$/$t_{12}$ orbits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.