module module high

`IndisputableMonolith.Gravity.Analysis.ReggeHinge4DStarKernel13`

Enumerates the 3^4 candidate unit-cube origins with offsets in {-1,0,1}^4 and proves which cubes contain a fixed 4D Freudenthal hinge. Establishes that only the origin cube meets the hinge and records the local hinge-mask star of cardinality 13. Downstream flat-Hessian and Bloch-symbol assembly cite this incidence kernel when weighting star deficit contributions.

claimCandidate cube origins are offsets $o\in\{-1,0,1\}^4$ (encoded as $\mathrm{Fin}\,3$ per axis). A hinge vertex with absolute coordinate $v\in\{0,1\}$ lies in the cube of origin $o$ iff $o\le v+1\le o+1$ on every axis. The star of cubes meeting a fixed hinge has cardinality 13, and only the origin offset contains the hinge.

background

In the 4D Regge QG campaign the edge stencil (ReggeEdgeStencil4D) packages Freudenthal 4-cube classes and a provisional finite TT quadratic. The flat-hinge kernel (ReggeHinge4DFlatKernel) and dihedral cosine kernel (ReggeHinge4DDihedralKernel) import that 15-class stencil and never redefine it; they supply hinge incidence and flat second-variation ingredients.

A hinge in the Freudenthal triangulation of the 4-torus is a 2-face shared by a star of 4-simplices. To assemble the star deficit kernel one must know which unit cubes meet that hinge. This module fixes the combinatorial model: cube origins are integer offsets with each coordinate in ${-1,0,1}$, and membership of a hinge vertex is the shifted interval test $o\le v+1\le o+1$ on each axis.

Sibling definitions encode axis projections, absolute hinge coordinates, vertex-in-cube predicates, and the local hinge-mask list used by later Hessian assembly.

proof idea

Definition-heavy incidence module, not a single deep theorem. Offsets are Fin 3 encodings of ${-1,0,1}$; axis-fit and vertex-in-cube are pure arithmetic comparisons. Cube-contains-hinge is the product of per-axis tests. Cardinality of the star and the uniqueness claim (only the origin offset contains the hinge) are finite enumerations over the $3^4$ candidates, discharging by case split / decidable search. Local hinge masks package the surviving incidence data for consumers.

why it matters in Recognition Science

Feeds the committed per-orbit star deficit kernels in ReggeFlat4DHessianAssembly, which replaces the provisional weight-1 aggregate of finiteTTQuadratic by true flat second-variation weights built from Heron area gradients and these star kernels. Bloch all-orbit and transported all-orbit folds (ReggeBlochAllOrbitSymbol4D, ReggeBlochTransportedAllOrbit4D) consume that assembly when forming the factorized m² moment over the six S4 hinge types. The companion audit module ReggeHinge4DStarKernel13Audit binds #print axioms for this file. In the QG full-theory chain this is the kernel-checked hinge-star incidence step between dihedral flat kernels and continuum-facing Bloch symbols.

scope and limits

Does not derive continuum Einstein–Hilbert limits or curvature identities.
Does not treat non-Freudenthal triangulations or irregular lattices.
Does not assemble Hessian weights or Bloch symbols; only incidence and masks.
Does not claim dynamical stability or positivity of the quadratic form.
Does not redefine the 15-class edge stencil or dihedral cosine 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.ReggeHinge4DStarKernel13Audit 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 (90)

abbrev CubeOffset L68
def offsetAxis L70
def absHingeCoord L77
def axisFits L83
def vertexInCube L86
def cubeContainsHinge L89
def originOffset L92
theorem cubeContainsHinge_origin L95
theorem star_cube_cardinality L98
theorem only_origin_contains_hinge L103
def localHingeMasks L109
def containsHinge L112
def starMembers L115
theorem starMembers_length L117
theorem starMembers_complete L119
theorem star_cardinality L123
def t13FlatSqEdges L133
theorem hingeGramDet_t13 L137
theorem apexDotNum_t13 L139
theorem apex3NormSqNum_t13 L141
theorem apex4NormSqNum_t13 L143
theorem cosDihedral_t13_flat L146
theorem arccos_one_half L158
def flatAngleT13 L164
theorem flatAngleT13_eq L166
def starFlatAngleSum L168
theorem star_flat_angle_sum_two_pi L170
def starFlatCosines L174
theorem starFlatCosines_match L176
def t13CoordPath L183
def t13CosKernel L186
lemma hasDerivAt_quadPoly L193
lemma hasDerivAt_numForm_t13 L206
lemma hasDerivAt_t13_slot L232
lemma t13_path0_polys L260
lemma t13_path1_polys L270
lemma t13_path2_polys L280
lemma t13_path3_polys L290
lemma t13_path4_polys L300
lemma t13_path5_polys L310
lemma t13_path6_polys L320
lemma t13_path7_polys L330
lemma t13_path8_polys L340
lemma t13_path9_polys L350
theorem hasDerivAt_t13_slot0 L360
theorem hasDerivAt_t13_slot1 L368
theorem hasDerivAt_t13_slot2 L376
theorem hasDerivAt_t13_slot3 L384
theorem hasDerivAt_t13_slot4 L392
theorem hasDerivAt_t13_slot5 L401
theorem hasDerivAt_t13_slot6 L409
theorem hasDerivAt_t13_slot7 L418
theorem hasDerivAt_t13_slot8 L427
theorem hasDerivAt_t13_slot9 L435
theorem hasDerivAt_t13_coord L444
def chainT13 L462
theorem chainT13_eq L464
def t13DeficitKernel L470
theorem t13DeficitKernel_eq_chain L477
def starSlotClass L491
def assembleStarMember L505
def fullStarClassKernelAssembled L509
def fullStarClassKernel L512
lemma sum_support4_4679 L522
lemma deficit_zero_off L536
lemma member_eval L541
lemma sum6 L552
lemma member0_closed L561
lemma member1_closed L571
lemma member2_closed L581
lemma member3_closed L591
lemma member4_closed L601
lemma member5_closed L611
theorem fullStarClassKernel_eq L621
theorem fullStarClassKernel_values L629
theorem fullStarClassKernel_zero_off L639
theorem fullStarClassKernel_nonvacuous L647
def swap12Mask L653
theorem swap12Mask_bounds L659
def swap12Class L663

… and 10 more