module module high

`IndisputableMonolith.Gravity.Analysis.ReggeHinge4DStarKernel22`

Catalogues absolute vertex masks for the (2,2) hinge class in the Freudenthal 4-cube, together with the local star membership of those hinges. Gravity analysts building the 4D Regge flat Hessian and Bloch symbols cite it for the combinatorial star of a (2,2) seed hinge. The module is definitional: it enumerates cube corners, containment predicates, and proves star cardinality and completeness by finite case analysis.

claimIn the Freudenthal triangulation of the 4-cube, fix the absolute $(2,2)$ hinge class. The module defines the absolute hinge vertex masks, the cube-corner incidence relation, local hinge masks at a corner, and the star membership set of a $(2,2)$ hinge. It asserts that the star has a fixed finite cardinality and that the enumerated members exhaust every 4-simplex containing the hinge.

background

Recognition Science's QG campaign packages 4D Regge calculus on the Freudenthal subdivision of the hypercube. Edges fall into a 15-class stencil (ReggeEdgeStencil4D); hinges (codimension-2 faces carrying curvature) are typed by bipartitions of the four edge directions, written $(p,q)$ with $p+q=4$. The six S4 hinge types are $(1,1)$, $(1,2)$, $(2,1)$, $(1,3)$, $(3,1)$, $(2,2)$.

Upstream, ReggeHinge4DFlatKernel supplies Freudenthal hinge incidence and the flat-Hessian skeleton; ReggeHinge4DDihedralKernel adds the seed-hinge dihedral cosine kernel at flat geometry. Neither redefines the stencil API. This module isolates the absolute (coordinate-fixed) vertex masks for the $(2,2)$ class and the combinatorial star of such a hinge: the set of 4-simplices incident on it.

Notation is mask-based: a vertex or hinge is a bit-mask inside the 4-cube; containment and star membership are Boolean predicates on those masks. The star is the discrete support on which deficit angles and area covectors later assemble into the second variation of the Regge action.

proof idea

Definition module with finite combinatorial lemmas, not a deep analytic argument. Absolute hinge masks and cube-corner types are closed enumerations. Containment predicates (cornerContainsMask, containsHinge) are Boolean checks on bit-masks. Star membership is the filtered list of local 4-simplices meeting a fixed $(2,2)$ hinge.

Length, completeness, and cardinality statements are proved by exhaustive evaluation over the finite mask set (decide/native_decide style case splits), confirming the star list has the expected size and misses no incident simplex. No continuum analysis and no curvature identities appear here.

why it matters in Recognition Science

The $(2,2)$ star is one of the six orbit seeds consumed when the flat 4D Hessian is assembled. Downstream, ReggeFlat4DHessianAssembly pairs committed per-orbit star deficit kernels with Heron area gradients to replace the provisional weight-1 aggregate of the edge stencil. Bloch-symbol modules (ReggeBlochAllOrbitSymbol4D, ReggeBlochTransportedAllOrbit4D) fold over all six hinge types, including $(2,2)$, to produce the factorized and transported $m^2$ moments of the continuum-facing symbol.

An audit companion (ReggeHinge4DStarKernel22Audit) constrains every public theorem here to the standard axiom set [propext, Classical.choice, Quot.sound]. In the broader RS gravity chain this is a kernel-checked combinatorial brick: without a certified $(2,2)$ star, the all-orbit Hessian and Bloch folds cannot claim complete hinge coverage.

scope and limits

Does not define star kernels for hinge types other than (2,2).
Does not compute dihedral angles, deficits, or Hessian entries.
Does not prove continuum limits or Bloch-symbol identities.
Does not transport masks under S4; absolute (coordinate-fixed) masks only.
Does not replace or redefine the 15-class edge stencil API.

used by (4)

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

IndisputableMonolith.Gravity.Analysis.ReggeBlochAllOrbitSymbol4D module_import
IndisputableMonolith.Gravity.Analysis.ReggeBlochTransportedAllOrbit4D module_import
IndisputableMonolith.Gravity.Analysis.ReggeFlat4DHessianAssembly module_import
IndisputableMonolith.Gravity.Analysis.ReggeHinge4DStarKernel22Audit module_import

depends on (3)

Lean names referenced from this declaration's body.

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

declarations in this module (76)

def absHingeMasks L62
abbrev CubeCorner L66
def cornerContainsMask L71
def cornerContainsHinge L74
def localMask L79
def localHingeMasks L81
def containsHinge L84
structure StarMember L88
def starMembers L93
theorem starMembers_length L96
theorem starMembers_complete L98
theorem star_cardinality L103
theorem only_origin_corner_contains_hinge L108
def t22FlatSqEdges L117
theorem hingeGramDet_t22 L121
theorem apexDotNum_t22 L123
theorem apex3NormSqNum_t22 L125
theorem apex4NormSqNum_t22 L127
theorem cosDihedral_t22_flat L130
def flatAngleT22 L137
theorem flatAngleT22_eq L139
def starFlatAngleSum L141
theorem star_flat_angle_sum_two_pi L143
def starFlatCosines L147
theorem starFlatCosines_match_orbit L149
def t22CoordPath L155
def t22CosKernel L158
lemma hasDerivAt_quadPoly L170
lemma hasDerivAt_numForm_t22 L184
lemma hasDerivAt_t22_slot L210
lemma t22_path0_polys L237
lemma t22_path1_polys L247
lemma t22_path2_polys L257
lemma t22_path3_polys L267
lemma t22_path4_polys L277
lemma t22_path5_polys L287
lemma t22_path6_polys L297
lemma t22_path7_polys L307
lemma t22_path8_polys L317
lemma t22_path9_polys L327
theorem hasDerivAt_t22_slot0 L337
theorem hasDerivAt_t22_slot1 L345
theorem hasDerivAt_t22_slot2 L353
theorem hasDerivAt_t22_slot3 L361
theorem hasDerivAt_t22_slot4 L369
theorem hasDerivAt_t22_slot5 L377
theorem hasDerivAt_t22_slot6 L385
theorem hasDerivAt_t22_slot7 L393
theorem hasDerivAt_t22_slot8 L401
theorem hasDerivAt_t22_slot9 L409
theorem hasDerivAt_t22_coord L417
def chainT22 L435
def t22DeficitKernel L438
theorem t22DeficitKernel_eq_chain L440
def starSlotClass L446
def assembleStarMember L456
def fullStarClassKernelAssembled L460
def fullStarClassKernel L463
lemma sum_fin10 L480
lemma member_eval L491
lemma sum4 L506
theorem fullStarClassKernel_eq L514
theorem fullStarClassKernel_values L522
def swap01Mask L542
theorem swap01Mask_bounds L548
def swap01Class L552
theorem fullStarClassKernel_nonvacuous L557
theorem fullStarClassKernel_swap01 L560
theorem fullStarClassKernel_swap23 L564
def fullStarDirectional L568
lemma sum15_all L571
theorem fullStar_uniformScale_decoy L585
theorem fullStar_homothety_stationary L591
structure Hinge4DStarKernel22Status L616
def hinge4DStarKernel22Status L625
theorem hinge4DStarKernel22Status_flags L634