Pith. sign in
module module moderate

IndisputableMonolith.Gravity.Analysis.ReggeHinge4DFlatKernel

show as:
view Lean formalization →

Combinatorial incidence layer for 4D Regge calculus on the Freudenthal (Kuhn) triangulation of the unit 4-cube. It enumerates the 24 axis permutations, vertex masks, and local edge-class data that label hinges and edges inside each simplex. Downstream flat-Hessian, dihedral, orbit, and star-kernel modules import this API without redefining it. The content is definitional scaffolding plus elementary mask lemmas, not a deep analytic proof.

claimOn the Freudenthal triangulation of the unit $4$-cube, the $24$ ordered simplices are indexed by permutations $\sigma\in S_4$ via axis tuples $(\sigma(0),\sigma(1),\sigma(2),\sigma(3))$. Each simplex carries a vertex mask, local edge pairs, and a local edge-class label compatible with the $15$-class $4$D edge stencil. These data form the incidence skeleton used to assemble the flat hinge Hessian.

background

Recognition Science gravity analysis builds discrete Regge kernels on Freudenthal triangulations (Kuhn cubes split into simplices). In 4D the unit cube decomposes into $24=4!$ oriented $4$-simplices, one per axis permutation. The upstream module ReggeEdgeStencil4D supplies the $15$ combinatorial edge classes of the $4$-cube and a provisional finite quadratic form; this module sits one layer above that stencil and never redefines it.

Objects introduced here are purely combinatorial: lexicographic permAxes maps an index $s\in\mathrm{Fin},24$ to $(\sigma(0),\ldots,\sigma(3))$; vertexMask records which cube vertices belong to a simplex; localEdgePair / localEdgeMask / localEdgeClass identify edges inside a simplex and attach the stencil class. Bounds lemmas (localEdgeMask_bounds, vertexMask_start/end) keep indices in range.

The setting is the QG full-theory campaign's kernel-checked path: after edge TT attachment and the $4$D stencil, one needs a stable incidence API before dihedral cosines, orbit classification, or Bloch folds can be stated.

proof idea

This is primarily a definition module. Permutations of Fin 4 are enumerated lexicographically; masks and edge pairs are computed by pure arithmetic on those permutations. Supporting lemmas are short bounds and classification facts (mask ranges, class consistency, simplexHasClass). There is no analytic curvature argument here; the module only freezes the combinatorial API that later kernels import.

why it matters in Recognition Science

Every subsequent $4$D hinge kernel treats this module as the frozen Freudenthal incidence layer. ReggeHinge4DDihedralKernel builds the seed-hinge dihedral cosine kernel at flat on top of it; ReggeHinge4DOrbitClassification uses the $24$ Kuhn simplices and vertexMask API as the combinatorial prerequisite for assembling the flat Hessian from per-orbit star kernels; ReggeHinge4DStarKernel (and the $12$/$13$ variants) import the same incidence layer plus the $15$-class stencil. ReggeBlochFold4D folds the committed true-weight flat Hessian for type-$(1,1)$ triangle hinges using the midpoint plane-wave convention tied to this skeleton. Regge4DSchlaefliPathwise lifts the $3$D six-edge Schläfli identity to the $4$-simplex ($n_H=n_E=10$). The audit module records the expected axiom footprint [propext, Classical.choice, Quot.sound]. In the RS gravity stack this is the $4$D analogue of the $3$D TT edge-class packaging that feeds hinge-aware zero-mode analysis.

scope and limits

used by (9)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (48)