Pith. sign in
module module high

IndisputableMonolith.Gravity.Analysis.ReggeHinge4DOrbitClassification

show as:
view Lean formalization →

Classifies triangle hinges of a 4-simplex into the six S4 orbit types used by the 4D Regge Bloch and flat-Hessian stack. Packages the binom(5,3)=10 vertex triples, vertex/difference masks, and population-to-orbit maps. Downstream Bloch folds and algebraic closers import this as the frozen hinge-type dictionary. Mostly definitional enumeration with small correctness lemmas.

claimCombinatorial classification of triangle hinges in a 4-simplex: the $\binom{5}{3}=10$ increasing vertex-index triples, their vertex masks and difference masks, population counts, and the six $S_4$ hinge orbit types $(1,1)$, $(1,2)$, $(2,1)$, $(1,3)$, $(3,1)$, $(2,2)$, with maps between population data and orbit labels.

background

In 4D Regge calculus on a Freudenthal (Kuhn) triangulation, curvature lives on triangular hinges (codimension-2 faces). A single 4-simplex has five vertices, so its triangular faces are exactly the $\binom{5}{3}=10$ increasing index triples. The edge-stencil and flat-kernel modules already fix the 15-class Freudenthal edge packaging and the hinge-incidence skeleton; this module does not redefine those stencils.

Orbit classification is forced by the residual $S_4$ action (coordinate permutations of the ambient 4-cube, plus complement). Two difference masks on the three vertices of a triangle determine a population pair that labels the orbit. The six types $(1,1)$, $(1,2)$, $(2,1)$, $(1,3)$, $(3,1)$, $(2,2)$ are the distinct pairs that appear; four of them form genuine $S_4$+complement orbits used in the Bloch symbol fold.

Upstream docs place this after ReggeEdgeStencil4D and inside the hinge-incidence / flat-Hessian campaign of ReggeHinge4DFlatKernel: the 15-class stencil is imported, never redefined.

proof idea

Definition module with thin correctness lemmas, not a deep proof development. It enumerates the ten increasing triples, builds vertex masks and the two difference masks per hinge slot, computes population counts, and maps those counts onto an inductive HingeOrbitType. Lemmas such as population-is-orbit-type and triangle-diff-masks-ok discharge the obvious combinatorial side conditions so downstream code can pattern-match on orbit labels without re-deriving mask arithmetic.

why it matters in Recognition Science

Frozen hinge-type dictionary for the entire 4D Regge analysis stack. ReggeBlochAllOrbitSymbol4D folds over the six $S_4$ hinge types consuming this classification; ReggeBlochFold4D specializes the $(1,1)$ orbit; ReggeBlochOrbitTransport4D builds covering permutations from orbit representatives and the difference-mask pair. Flat-Hessian assembly, pathwise Schläfli at $n_H=n_E=10$, and both algebraic closers (plain and transported) import the module so continuum preflight and TT isotropy targets share one orbit language.

In the QG full-theory campaign this is the combinatorial bridge between the edge stencil and every multi-orbit Bloch or closer argument. Without a single orbit taxonomy, the four-orbit symbol fold and the transported algebraic identities would each re-encode mask populations ad hoc.

scope and limits

used by (9)

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

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (58)