module module high

`IndisputableMonolith.Gravity.Analysis.ReggeHinge4DOrbitClassification`

Classifies the ten triangular hinges of a Freudenthal 4-simplex into S4 orbit types by vertex-mask population. Downstream 4D Bloch folds, orbit transport, and algebraic closers import these labels rather than re-deriving them. The module is definitional: pop counts, difference masks, an orbit-type enum, and small consistency lemmas.

claimOn a 4-simplex with vertices $\{0,1,2,3,4\}$, the $\binom{5}{3}=10$ increasing triples index the triangular hinges. Each hinge receives difference masks and a population pair, mapped to an orbit type in $\{(1,1),(1,2),(2,1),(1,3),(3,1),(2,2)\}$ under the Freudenthal $S_4$ action (four orbits once complements are identified).

background

In 4D Regge calculus on a Kuhn/Freudenthal triangulation, curvature lives on triangular hinges (codimension-2 faces). A single 4-simplex has five vertices and exactly $\binom{5}{3}=10$ such hinges. The parent campaign packages a 15-class edge stencil (ReggeEdgeStencil4D) and a flat-Hessian incidence skeleton (ReggeHinge4DFlatKernel); this module sits between them and the Bloch/algebraic layers.

Hinges are not all equivalent under the lattice symmetry. Two edge-difference masks on the ambient cube coordinates yield a population pair (how many axes each mask occupies). That pair is the discrete invariant that labels the six named types $(1,1)$, $(1,2)$, $(2,1)$, $(1,3)$, $(3,1)$, $(2,2)$, of which four are independent once complementation is quotiented.

Sibling definitions introduce the ordered triple index, mask population, the two difference masks per hinge slot, the orbit-type inductive, and the round-trip maps between population and type.

proof idea

Definition module with small checked lemmas, not a deep proof development. It enumerates the ten increasing vertex triples, builds per-hinge difference masks from the Freudenthal embedding, computes mask populations, and maps those populations onto a finite orbit-type enum. Consistency lemmas assert that the population of every hinge is a valid orbit type and that the type-to-pop round trip recovers the population. No continuum limit or Hessian identity is proved here.

why it matters in Recognition Science

Every 4D Bloch and closer path in the QG campaign consumes these orbit labels. ReggeBlochFold4D folds the true-weight flat Hessian on the $(1,1)$ orbit; ReggeBlochAllOrbitSymbol4D extends the factorized fold across all six types; ReggeBlochOrbitTransport4D picks covering permutations so that each slot $(s,t)$ of type ty is transported from a fixed representative. ReggeFlat4DHessianAssembly, the algebraic closers (Regge4DAlgebraicCloser, Regge4DTransportedAlgebraicCloser), and the pathwise Schläfli module all import the same classification so hinge sums stay orbit-indexed rather than ad hoc. Without a frozen orbit taxonomy, the multi-orbit symbol stack and the OPEN isotropy targets would not share a common discrete basis.

scope and limits

Does not prove continuum Einstein–Hilbert convergence or any Tendsto statement.
Does not assemble or diagonalize the flat Hessian; only labels hinges.
Does not claim the six types are inequivalent without the complement quotient.
Does not treat non-Freudenthal triangulations or curved background metrics.
Does not discharge OPEN isotropy or plus-cross targets in the algebraic closers.

used by (9)

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

IndisputableMonolith.Gravity.Analysis.Regge4DAlgebraicCloser module_import
IndisputableMonolith.Gravity.Analysis.Regge4DSchlaefliPathwise module_import
IndisputableMonolith.Gravity.Analysis.Regge4DTransportedAlgebraicCloser module_import
IndisputableMonolith.Gravity.Analysis.ReggeBlochAllOrbitSymbol4D module_import
IndisputableMonolith.Gravity.Analysis.ReggeBlochFold4D module_import
IndisputableMonolith.Gravity.Analysis.ReggeBlochOrbitTransport4D module_import
IndisputableMonolith.Gravity.Analysis.ReggeBlochStarEdgeOrigins4D module_import
IndisputableMonolith.Gravity.Analysis.ReggeFlat4DHessianAssembly module_import
IndisputableMonolith.Gravity.Analysis.ReggeHinge4DOrbitClassificationAudit module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.Analysis.ReggeEdgeStencil4D module_import
IndisputableMonolith.Gravity.Analysis.ReggeHinge4DFlatKernel module_import

declarations in this module (58)

def triangleIndexTriple L69
def maskPop L83
def triangleVertexMasks L90
def diffMaskA L95
def diffMaskB L100
def hingeTypePop L105
inductive HingeOrbitType L109
def popToOrbitType L126
theorem hingeTypePop_is_orbitType L136
def hingeOrbitType L141
theorem hingeOrbitType_toPop L144
theorem triangle_diff_masks_ok L150
def triangleTypeNat L159
def cellTriangleCount L163
theorem cellTriangleCount_t11 L166
theorem cellTriangleCount_t12 L169
theorem cellTriangleCount_t21 L172
theorem cellTriangleCount_t13 L175
theorem cellTriangleCount_t31 L178
theorem cellTriangleCount_t22 L181
theorem cellTriangleCount_values L185
theorem cellTriangleCount_sum L196
theorem oriented_slot_total L204
def isRealizableDiffPair L211
def isDisjointDiffPair L216
theorem disjoint_implies_realizable L220
theorem decoy_overlapping_not_realizable L227
theorem decoy_overlapping_is_not_disjoint L231
theorem seed_slot_masks L236
theorem seed_hinge_type_t11 L241
def permMask L248
def coordPermOf L256
def permDiffPair L264
theorem coordPerm_preserves_pop L269
theorem coordPerm_preserves_type L275
def orbitRep L282
theorem orbitRep_realizable L290
theorem orbitRep_type L294
def inOrbitOfRep L299
theorem realizable_in_type_orbit L306
theorem realizable_matches_rep_orbit L317
def complementMask L325
theorem complement_preserves_kuhn L329
theorem complement_swaps_diff_pair L336
theorem complement_swaps_type L343
inductive HingeOrbitTypeModComplement L350
theorem orbit_count_S4 L363
theorem orbit_count_S4_complement L366
def absoluteTriple L373
def permTriple L377
theorem absolute_t11_not_S4_transitive L386
structure OrbitLocalSq L398
def localSqOfDiff L404
def orbitLocalSq L407
theorem orbitLocalSq_values L410
theorem slot_localSq L421
def hinge4DOrbitClassificationStatus L428
theorem hinge4DOrbitClassificationStatus_flags L436