regge4DFlatSecondVariationStatus_flags
plain-language theorem explainer
Status snapshot for the 4D flat Regge second-variation program: candidate Hessian identified, Bloch face evaluated, flat Freudenthal Schläfli and directional kills present, full pathwise Schläfli absent, elevation open, gap-action recovery false. Cited by anyone auditing Gate A2 closure in 4D versus the closed 3D tetra case. Proof is a one-line decidable check on the boolean record fields.
Claim. The 4D flat second-variation status record satisfies: candidate reduced Hessian identified; its Bloch continuum face evaluated; flat Freudenthal 4-simplex Schläfli present; flat directional Schläfli present; full off-flat pathwise Schläfli absent; Schläfli elevation of the nonlinear action open; and gap-action recovery false.
background
This module tracks Gate A2 for 4D Regge gravity on a flat seed: elevate the true nonlinear Regge action to a Schläfli-reduced edge Hessian. In 3D that elevation is closed (tetra six-edge closed form to true second variation). In 4D the flat-seed Freudenthal Schläfli summand table, seed-angle derivative, and flat directional kill along every affine velocity are theorems in the pathwise Schläfli module; the full off-flat pathwise closed form is not.
The status record is a boolean dashboard of those milestones plus honesty flags: elevation still open, and the gap-action recovery bit stays false (the RS gap is the product of closure and Fibonacci factors, or the anchor display $F(Z)=\ln(1+Z/\varphi)/\ln\varphi$; neither is flipped here).
Prior failed closers (distinct-hinge fold at face $-1/16$, full two-jet $A_0\cdot K_2$, mean-local Path B, density dictionary survivor already 1) leave residual only in Schläfli elevation, not another incidence rescale.
proof idea
The status structure is a record whose fields are literal booleans (true/false as in the definition). The theorem is the conjunction of seven field equalities. The proof is a single decide tactic: each equality is decidable on Bool, so the kernel evaluates the conjunction to true.
why it matters
Pins an honest progress board for 4D Regge flat second variation against the 3D contract. THEOREM tier: candidate reduced Hessian identified with assembled/distinct-hinge geometry; Bloch face on Frobenius-normalized axis TT at symbolDir equals $-1/16$ and differs from frozen EH $-1/4$; flat Freudenthal Schläfli and directional kills present. OPEN tier: full off-flat pathwise Schläfli and therefore elevation of nonlinear $S''(0)$ to the candidate. Explicitly does not flip gap-action recovery and does not inhabit 4D continuum EH convergence. With no downstream users yet, it is the audit point for residual Schläfli elevation work rather than another fitted factor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.