regge4DSchlaefliPathwiseStatus_flags
plain-language theorem explainer
Status certificate for the Freudenthal 4-simplex pathwise Schläfli analysis: flat closed form, seed geometric match, nonvacuous flat witness, seed-angle differentiability, and flat directional kill are all marked present; full pathwise identity and gap-action recovery stay false. Auditors of the 4D Gate-A2 lift cite it as the single boolean ledger. Proof is one `decide` on the structure fields.
Claim. The 4-simplex pathwise Schläfli status record satisfies: flat closed-form identity is present; seed geometric match is present; a non-vacuous flat $SchlaefliIdentityN$ witness is present; the seed-hinge dihedral angle has a derivative along every squared-edge path through the flat seed; flat directional Schläfli is present; full pathwise identity off the flat seed is absent; gap-action recovery is absent.
background
This module lifts the 3D Gate-A2 input (tetrahedron six-edge closed-form Schläfli, $n_H = n_E = 6$) to the Freudenthal/Kuhn 4-simplex ($n_H = n_E = 10$). Regge calculus encodes curvature on hinges; the classical Schläfli identity relates hinge-area variations to dihedral-angle variations so that the first variation of the Regge action is well-defined.
Local objects include squared edge lengths on the 4-simplex, triangle-hinge combinatorics, flat hinge areas (Heron-type evaluations at the flat seed), and the flat Schläfli summand table whose column sums vanish. The seed-hinge row is required to match $\mathrm{hingeArea}\cdot\mathrm{angleKernel}$ from the 4D dihedral kernel.
The status structure is a boolean ledger of which tiers are closed. Upstream, the structure instance hard-codes five true flags (flat closed form, seed geometric match, nonvacuous flat witness, seed-angle HasDerivAt, flat directional present); the remaining two fields default false.
proof idea
One-line decidability proof. The status instance sets five booleans to true and leaves fullPathwisePresent and gapActionRecovery at their default false. The theorem is the seven-way conjunction of those equalities; decide discharges it by computation on Bool.
why it matters
Gives a machine-checkable progress board for the 4D Schläfli path toward Einstein-Hilbert recovery in Recognition gravity. Binding tier tags already closed: Freudenthal edge/hinge combinatorics and flat summand table; a strictly positive-area flat SchlaefliIdentityN witness (avoids the zero-measure vacuous shell lesson); seed-hinge dihedral HasDerivAt along every squared-edge coordinate; flat directional Schläfli kill along every affine velocity through the flat seed (Gate A2-style input at flat).
Explicitly open, and flagged false here: full pathwise identity on Nondeg4Simplex off the flat seed; remapped HasDerivAt for every hinge row; elevation to a Regge 4D Schläfli candidate; and $S_{RS}$ convergence to EH in 4D. The ledger also refuses to flip gap-action recovery. No downstream consumers are wired yet; the declaration is the terminal status seal of the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.