module module moderate

`IndisputableMonolith.Gravity.Analysis.ReggeHinge4DStarKernel`

Defines the 4D Freudenthal hinge star: the finite set of cube translates whose simplices meet a fixed triangular hinge, with opposite/orthogonal edge classes and Gram data at flat. Gravity analysts cite it when assembling true-weight flat Hessians and Bloch folds. Structure is combinatorial enumeration plus algebraic identities on masks and edge pairings, not continuum analysis.

claimOn the 4D Freudenthal lattice, fix a seed triangular hinge. The star is the finite list of cube translates whose local hinge masks contain that hinge; its cardinality is fixed, and each star member carries opposite and orthogonal flat-square edge classes together with the associated Gram-determinant and apex-dot numerators at the flat background.

background

This module sits in the QG full-theory campaign after the 15-class edge stencil and the flat/dihedral hinge kernels. Those layers package Freudenthal incidence and the seed-hinge cosine data at flat; they never redefine the stencil API. The present file lifts from a single seed hinge to the full star of cubes that touch it.

A cube translate is a lattice shift of the reference 4-cube. Local hinge masks mark which triangle hinges live in each translate. A star member is one such translate that contains the seed hinge; starMembers enumerates them completely, with a proved length and cardinality. Opposite and orthogonal flat-square edge classes record how the two faces of the hinge sit relative to the remaining edges in each member, feeding Gram determinants and apex inner-product numerators used later as true weights.

Notation stays discrete and combinatorial: no continuum limit is taken here. The flat background is the same zero-curvature reference used by the dihedral and flat kernels upstream.

proof idea

Definition-and-enumeration module with supporting lemmas, not a single deep theorem. Cube translates and hinge masks are introduced first; membership is the predicate that a mask contains the seed hinge. Completeness and length of the star list are proved by exhaustive case analysis on the finite Freudenthal incidence table. Opposite/orthogonal edge-class maps and the Gram/apex identities are algebraic reductions on those finite tables, reusing the flat and dihedral kernels rather than re-deriving cosine expansions.

why it matters in Recognition Science

The star is the missing local assembly unit between seed-hinge kernels and global second-variation symbols. Downstream, ReggeFlat4DHessianAssembly consumes the per-orbit star deficit kernels with Heron area gradients to replace the provisional weight-1 aggregate of the edge stencil. Bloch modules (ReggeBlochFold4D, all-orbit and transported folds, local-incidence Path B) expand the star as a sum over cube-translate bases with phase decoration. The exact-action symbol module uses the same star data when checking that the true Regge Hessian annihilates vertex gauge modes and sends normalized TT to $-1/4$. The audit module re-imports this file for kernel checks. Without a committed star cardinality and opposite-edge Gram layer, the flat Hessian and continuum $m^2$ moments have no local support.

scope and limits

Does not define the continuum Bloch symbol or $m^2$ moment; those live in downstream fold modules.
Does not assemble the full flat Hessian quadratic; only star membership and edge/Gram ingredients.
Does not treat curved (non-flat) backgrounds or nonzero deficit beyond seed data.
Does not re-prove the 15-class stencil or dihedral cosine kernel; both are imported.
Does not claim continuum TT eigenvalues; oracle $H_{\mathrm{fold}}$ checks sit elsewhere.

used by (7)

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

IndisputableMonolith.Gravity.Analysis.Regge4DExactActionSymbol module_import
IndisputableMonolith.Gravity.Analysis.ReggeBlochAllOrbitSymbol4D module_import
IndisputableMonolith.Gravity.Analysis.ReggeBlochFold4D module_import
IndisputableMonolith.Gravity.Analysis.ReggeBlochLocalIncidence4D module_import
IndisputableMonolith.Gravity.Analysis.ReggeBlochTransportedAllOrbit4D module_import
IndisputableMonolith.Gravity.Analysis.ReggeFlat4DHessianAssembly module_import
IndisputableMonolith.Gravity.Analysis.ReggeHinge4DStarKernelAudit 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 (114)

inductive CubeTranslate L56
def localHingeMasks L63
def containsHinge L69
structure StarMember L72
def starMembers L77
theorem starMembers_length L82
theorem starMembers_complete L84
theorem star_cardinality L88
def oppFlatSqEdges L95
def orthFlatSqEdges L99
theorem hingeGramDet_opp L103
theorem apexDotNum_opp L105
theorem apex3NormSqNum_opp L107
theorem apex4NormSqNum_opp L109
theorem hingeGramDet_orth L112
theorem apexDotNum_orth L114
theorem apex3NormSqNum_orth L116
theorem apex4NormSqNum_orth L118
theorem cosDihedral_opp_flat L121
theorem cosDihedral_orth_flat L133
theorem arccos_one_div_sqrt_two L140
def flatAngleSeedOpp L151
def flatAngleOrth L152
theorem flatAngleSeedOpp_eq L154
theorem flatAngleOrth_eq L156
def starFlatAngleSum L158
theorem star_flat_angle_sum_two_pi L160
def starFlatCosines L164
theorem starFlatCosines_match_orbits L169
def oppCoordPath L178
def oppCosKernel L181
lemma hasDerivAt_quadPoly L186
lemma hasDerivAt_numForm_opp L198
lemma hasDerivAt_opp_slot L249
lemma opp_path0_polys L277
lemma opp_path1_polys L287
lemma opp_path2_polys L297
lemma opp_path3_polys L307
lemma opp_path4_polys L317
lemma opp_path5_polys L327
lemma opp_path6_polys L337
lemma opp_path7_polys L347
lemma opp_path8_polys L357
lemma opp_path9_polys L367
theorem hasDerivAt_opp_slot0 L377
theorem hasDerivAt_opp_slot1 L386
theorem hasDerivAt_opp_slot2 L395
theorem hasDerivAt_opp_slot3 L404
theorem hasDerivAt_opp_slot4 L413
theorem hasDerivAt_opp_slot5 L422
theorem hasDerivAt_opp_slot6 L431
theorem hasDerivAt_opp_slot7 L440
theorem hasDerivAt_opp_slot8 L449
theorem hasDerivAt_opp_slot9 L458
theorem hasDerivAt_opp_coord L468
def orthCoordPath L485
def orthCosKernel L488
lemma hasDerivAt_numForm_orth L495
lemma hasDerivAt_orth_slot L521
lemma orth_path0_polys L548
lemma orth_path1_polys L558
lemma orth_path2_polys L568
lemma orth_path3_polys L578
lemma orth_path4_polys L588
lemma orth_path5_polys L598
lemma orth_path6_polys L608
lemma orth_path7_polys L618
lemma orth_path8_polys L628
lemma orth_path9_polys L638
theorem hasDerivAt_orth_slot0 L648
theorem hasDerivAt_orth_slot1 L657
theorem hasDerivAt_orth_slot2 L666
theorem hasDerivAt_orth_slot3 L675
theorem hasDerivAt_orth_slot4 L684
theorem hasDerivAt_orth_slot5 L693
theorem hasDerivAt_orth_slot6 L702
theorem hasDerivAt_orth_slot7 L711
theorem hasDerivAt_orth_slot8 L720
theorem hasDerivAt_orth_slot9 L729
theorem hasDerivAt_orth_coord L739

… and 34 more