Pith. sign in
module module low

IndisputableMonolith.Gravity.Analysis.ReggeHinge4DOrbitClassificationAudit

show as:
view Lean formalization →

Audit layer over the Regge 4D triangle-hinge orbit classification inside the Freudenthal/Kuhn cell. Researchers assembling the flat Hessian from per-orbit star kernels cite it to confirm combinatorial bookkeeping is closed. The module imports the classification and checks counts, mask coverage, and orbit representatives against the 24 Kuhn simplices and 15-class stencil masks; it introduces no new orbits.

claimAudit of the orbit classification of 4D Regge triangle hinges under the Freudenthal–Kuhn cell decomposition, checking consistency of the $24$ Kuhn simplices and the $15$-class edge-stencil masks that index per-orbit star kernels for the flat Hessian.

background

In the Recognition Science quantum-gravity campaign, the flat Hessian of the Regge action is built from star kernels indexed by orbits of triangle hinges in a 4D triangulation. The upstream module classifies those orbits inside the Freudenthal/Kuhn cell. Its doc states it is a "combinatorial prerequisite for assembling the flat Hessian from per-orbit star kernels" and that it "imports the 24 Kuhn simplices / vertexMask API of ReggeHinge4DFlatKernel and the 15-class mask utilities of ReggeEdgeStencil4D; never redefines them."

This audit module sits one layer above that classification. Its role is combinatorial hygiene: confirm that the orbit partition, mask assignments, and hinge incidences close under those APIs before the data feed Hessian assembly. Domain is Gravity analysis; the only import is the classification module itself.

proof idea

This is an audit module, not a single-spine theorem package. It imports the orbit-classification module and runs consistency checks (orbit counts, mask coverage, representative completeness) against the 24 Kuhn simplices and the 15-class stencil masks. Expect definition-level tallies and decidable equalities rather than deep algebraic argument. No new classification lemmas are introduced here.

why it matters in Recognition Science

The upstream classification is the combinatorial gate for flat-Hessian assembly from per-orbit star kernels in the QG full-theory campaign. Downstream Hessian construction needs the orbit table to be exhaustive and non-overlapping; this audit records that check. The page graph currently lists no used_by edges, so the module closes a local verification obligation rather than feeding a named parent theorem yet. It does not touch the T0–T8 forcing chain, RCL, or continuum limits; its scope is pure 4D Regge hinge combinatorics.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.