Regge4DSchlaefliPathwiseStatus
plain-language theorem explainer
Status record for the Freudenthal 4-simplex pathwise Schläfli program at ten hinges and ten edges. It packages seven boolean flags: closed-form flat summands, seed geometric match, nonvacuous flat witness, seed-angle differentiability, flat directional kill, full off-seed pathwise identity, and gap-action recovery. Gravity auditors cite it to read which Gate-A2-style inputs are closed versus still open. The declaration is a pure structure definition with no proof body.
Claim. A status bundle of seven booleans for the 4D Regge pathwise Schläfli program: (i) flat closed-form summands present; (ii) seed hinge row matches area times angle kernel; (iii) a nonvacuous flat $n_H=n_E=10$ Schläfli witness with strictly positive areas exists; (iv) the seed dihedral angle is differentiable along every squared-edge path; (v) the flat directional remainder vanishes for every velocity; (vi) the full pathwise identity off the flat seed is present; (vii) gap-action recovery is flipped.
background
The module lifts the 3D Gate-A2 input (tetrahedron six-edge closed-form Schläfli) to the Freudenthal/Kuhn 4-simplex, where both the hinge count and the edge count equal ten. Work sits in discrete Regge calculus: squared edge lengths are the coordinates, triangle hinges carry areas and dihedral angles, and the classical Schläfli relation constrains their first variation.
Tier tags split closed material from open goals. Closed: edge/hinge combinatorics, flat hinge areas, the flat Schläfli summand table with vanishing column sums, seed-row match to hingeArea · angleKernel, a nonvacuous flat SchlaefliIdentityN witness, seed-angle HasDerivAt along squared-edge paths, and the flat directional Schläfli kill for every affine velocity through the flat seed. Open: full pathwise identity on nondegenerate 4-simplices off the flat seed, remapped derivatives for every hinge row, elevation to a candidate, and convergence of the RS action to Einstein–Hilbert in 4D.
The structure does not itself prove any of those statements; it only names the checklist used by the module-level status value.
proof idea
No proof. The declaration is a structure (record type) with seven Bool fields and an empty body. Inhabitation is deferred to the sibling definition that assigns concrete true/false values from the theorems already proved in the module.
why it matters
Gives a single machine-readable dashboard for how far the 4D pathwise Schläfli ladder has climbed toward the open targets named in the module doc: full off-seed pathwise identity on nondegenerate 4-simplices, elevation to a Regge candidate, and $S_{\mathrm{RS}}\to$ Einstein–Hilbert in 4D. The downstream value regge4DSchlaefliPathwiseStatus fills the closed flags (flat closed form, seed geometric match, nonvacuous witness, seed-angle derivative, flat directional present) while leaving full pathwise and gap-action recovery unset, matching the explicit module notes that those two are not flipped here.
In the broader Recognition gravity stack this is bookkeeping for the discrete variational identity that must hold before continuum recovery arguments can fire. It does not touch the forcing chain (T0–T8), RCL, or the $\phi$-ladder mass formula; its job is local to Regge analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.