hinge4DDihedralKernelStatus_flags
plain-language theorem explainer
Status snapshot for the 4D Regge seed-hinge dihedral cosine kernel: three local deliverables are marked closed, the full lattice orbit remains open, and both EH-4d convergence and gap-action recovery stay false. Gravity/Regge analysts cite it as the machine-checked campaign ledger after the flat kernel. The proof is a pure `decide` on the boolean fields of the status record.
Claim. The seed-hinge 4D dihedral kernel status record satisfies: seed cosine at the flat point is closed; all ten coordinate derivatives are closed; the two-simplex partial deficit is closed; the full lattice orbit is open; convergence of the RS action to Einstein–Hilbert in 4d is false; and gap-action recovery is false.
background
This module is the next kernel-checked increment in the QG full-theory campaign after the flat 4D Regge hinge kernel. It works only on the seed triangle hinge ${0,e_0,e_0+e_1}$ inside its two seed-cell Freudenthal 4-simplices (permutations beginning $(0,1,\ldots)$), which share one local squared-edge vector checked against the incidence layer's local edge mask. The full lattice orbit sum over all hinges is explicitly left open.
Deliverables already proved in the module (and recorded by the status structure) are: the Gram-projection formula for the dihedral cosine as a function of the ten local squared edge lengths; its flat value $\cos=1/\sqrt{2}$ (equivalently $\cos^2=1/2$) by transcendental-free arithmetic; all ten coordinate derivatives at flat (slot 8 $\mapsto\sqrt{2}/8$, slot 9 $\mapsto-\sqrt{2}/4$, slots 0–7 $\mapsto 0$); and the two-simplex partial deficit gradient supported on edge classes $(3,7,11)$ with values $(-1/2,-1/2,+1/2)$, obtained via the arccos chain factor $-\sqrt{2}$.
The upstream definition hinge4DDihedralKernelStatus is the concrete record whose boolean fields this theorem re-exports as a single conjunction.
proof idea
One-line decidability proof. Unfold the status record (all fields are literal booleans) and run decide on the six-way conjunction. No lemmas, no algebraic rewriting, no analytic content: the theorem only certifies that the ledger matches the intended campaign flags.
why it matters
In the Recognition Science gravity stack this is the machine-checked progress marker for the 4D Regge seed-hinge dihedral kernel. It records that local cosine, ten-slot derivatives, and two-simplex partial deficit are closed, while three larger goals remain open: the full lattice orbit sum, convergence of the RS action to Einstein–Hilbert in 4d, and gap-action recovery. The module doc binds these negatives explicitly: the declaration does not complete the flat Hessian of the 4D Regge action, does not prove $S_{\mathrm{RS}}$ converges to EH in 4d, and does not reverse-engineer weights from Einstein–Hilbert. With no downstream users yet, it functions as an audit gate for the next orbit-sum and continuum-limit increments rather than as a lemma inside a larger proof.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.