module module moderate

`IndisputableMonolith.Gravity.Analysis.ReggeHinge4DStarKernel12`

Packages the 12-member star of a seed hinge in the 4D Freudenthal triangulation: incidence masks, membership, near/far square-edge classes, and flat Gram/apex numerics used by deficit kernels. Gravity analysts cite it when assembling the flat Regge Hessian or Bloch symbols from committed star data. Structure is definitional incidence plus completeness lemmas over the imported 15-class stencil and dihedral flat kernel.

claimOn the 4D Freudenthal lattice, fix a seed hinge. The module defines its local star of cardinality $12$, with membership predicates, cube translations and hinge masks, a partition of incident square edges into near and far classes, and the flat numerical ingredients (hinge Gram determinant and apex dot products) that feed the star deficit kernel at zero curvature.

background

In 4D Regge calculus the curvature degrees of freedom live on triangular hinges. The second variation of the action at flat space is assembled from area gradients and deficit responses summed over the star of 4-simplices incident to each hinge. This module sits in the QG full-theory kernel chain after the 15-class edge stencil (ReggeEdgeStencil4D), the Freudenthal hinge-incidence and flat-Hessian skeleton (ReggeHinge4DFlatKernel), and the seed-hinge dihedral cosine kernel (ReggeHinge4DDihedralKernel).

Those upstream layers supply Freudenthal incidence and the provisional finite TT quadratic; they never redefine the stencil API. Here the local geometry is specialized to one seed hinge: cube translations, local hinge masks, a StarMember type, an explicit 12-element star list with length and completeness theorems, and the near/far flat square-edge split together with flat Gram-determinant and apex-dot numerics used by deficit weights.

proof idea

Definition-heavy analysis module, not a single theorem. It introduces star incidence data (masks, membership, the enumerated 12-star) and proves bookkeeping facts: star list length, completeness relative to the hinge-containment predicate, and cardinality $12$. Near/far square-edge classifiers and the flat scalars hingeGramDet_near / apexDotNum_near are closed-form definitions on the imported dihedral and flat kernels. No deep analytic argument; the work is combinatorial packaging so downstream Hessian and Bloch folds can consume a committed star kernel.

why it matters in Recognition Science

This is the committed 12-star kernel that later modules treat as the local deficit building block. ReggeFlat4DHessianAssembly assembles per-orbit star deficit kernels with Heron area gradients into the flat second-variation quadratic, replacing the provisional weight-1 aggregate of the edge stencil. ReggeBlochAllOrbitSymbol4D and ReggeBlochTransportedAllOrbit4D fold those kernels over the six $S_4$ hinge types into continuum-facing Bloch symbols and $m^2$ moments. Regge4DExactActionSymbol uses the same star data in the $H_{\mathrm{fold}}$ pivot that annihilates vertex-gauge modes and sends normalized TT to $-1/4$. The companion audit module requires every public theorem here to print only in [propext, Classical.choice, Quot.sound].

scope and limits

Does not derive continuum Einstein–Hilbert or prove the full 4D Regge action equals GR off shell.
Does not assemble the global flat Hessian; that is deferred to ReggeFlat4DHessianAssembly.
Does not define Bloch folds, orbit transport, or the exact $H_{\mathrm{fold}}$ symbol.
Does not treat curved (non-flat) hinges or nonzero deficit beyond flat kernel numerics.
Does not redefine the 15-class edge stencil or dihedral cosine API.

used by (5)

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.ReggeBlochTransportedAllOrbit4D module_import
IndisputableMonolith.Gravity.Analysis.ReggeFlat4DHessianAssembly module_import
IndisputableMonolith.Gravity.Analysis.ReggeHinge4DStarKernel12Audit 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 (109)

inductive CubeTranslate L61
def localHingeMasks L66
def containsHinge L70
structure StarMember L73
def starMembers L78
theorem starMembers_length L82
theorem starMembers_complete L84
theorem star_cardinality L88
def nearFlatSqEdges L95
def farFlatSqEdges L98
theorem hingeGramDet_near L102
theorem apexDotNum_near L104
theorem apex3NormSqNum_near L106
theorem apex4NormSqNum_near L108
theorem hingeGramDet_far L111
theorem apexDotNum_far L113
theorem apex3NormSqNum_far L115
theorem apex4NormSqNum_far L117
theorem cosDihedral_near_flat L120
theorem cosDihedral_far_flat L125
def flatAngleRight L132
theorem flatAngleRight_eq L133
def starFlatAngleSum L134
theorem star_flat_angle_sum_two_pi L135
def starFlatCosines L138
theorem starFlatCosines_match_orbits L141
def nearCoordPath L148
def farCoordPath L151
def nearCosKernel L154
def farCosKernel L161
lemma hasDerivAt_quadPoly L170
lemma hasDerivAt_numForm_zeroDot L182
lemma hasDerivAt_near_slot L211
lemma hasDerivAt_far_slot L238
lemma near_path0_polys L265
theorem hasDerivAt_near_slot0 L275
lemma near_path1_polys L284
theorem hasDerivAt_near_slot1 L294
lemma near_path2_polys L303
theorem hasDerivAt_near_slot2 L313
lemma near_path3_polys L322
theorem hasDerivAt_near_slot3 L332
lemma near_path4_polys L341
theorem hasDerivAt_near_slot4 L351
lemma near_path5_polys L360
theorem hasDerivAt_near_slot5 L370
lemma near_path6_polys L379
theorem hasDerivAt_near_slot6 L389
lemma near_path7_polys L398
theorem hasDerivAt_near_slot7 L408
lemma near_path8_polys L417
theorem hasDerivAt_near_slot8 L427
lemma near_path9_polys L436
theorem hasDerivAt_near_slot9 L446
theorem hasDerivAt_near_coord L455
lemma far_path0_polys L470
theorem hasDerivAt_far_slot0 L480
lemma far_path1_polys L489
theorem hasDerivAt_far_slot1 L499
lemma far_path2_polys L508
theorem hasDerivAt_far_slot2 L518
lemma far_path3_polys L527
theorem hasDerivAt_far_slot3 L537
lemma far_path4_polys L546
theorem hasDerivAt_far_slot4 L556
lemma far_path5_polys L565
theorem hasDerivAt_far_slot5 L575
lemma far_path6_polys L584
theorem hasDerivAt_far_slot6 L594
lemma far_path7_polys L603
theorem hasDerivAt_far_slot7 L613
lemma far_path8_polys L622
theorem hasDerivAt_far_slot8 L632
lemma far_path9_polys L641
theorem hasDerivAt_far_slot9 L651
theorem hasDerivAt_far_coord L660
def chainRight L677
def nearDeficitKernel L678
def farDeficitKernel L679
theorem nearDeficitKernel_eq_chain L681

… and 29 more