IndisputableMonolith.Geometry.FreudenthalReggeComponent
Concrete local Regge geometry on an eight-vertex Freudenthal chart (cubic cell). Defines regular triangle areas, tetrahedral dihedral angles, area weights, and their scale derivatives for a regular local star. Cited by anyone linearizing the Regge action under a conformal edge ansatz. Mostly definitions plus elementary positivity and derivative lemmas from Cayley–Menger and dihedral data.
claimA finite local Regge model on eight vertices (Freudenthal / cubic chart): regular triangle area $A(\ell)$, regular tetrahedral dihedral angle $\theta_{\mathrm{tet}}$, a concrete local star with area weights $w$, and derivative identities for $A$ and $\theta$ under uniform edge scaling, built from Cayley–Menger volumes and dihedral data.
background
Recognition Science gravity work reduces the Regge action $S = \kappa^{-1}\sum_h A_h\delta_h$ under a conformal edge ansatz $\ell_{ij}=\ell_0\exp((\xi_i+\xi_j)/2)$ and a weak-field expansion in the potentials $\xi$. Discharging the deficit linearization hypothesis on general complexes is staged: Phase C1 (Cayley–Menger volumes from edge lengths) and Phase C2 (dihedral angles from that data).
This module supplies the finite local model those phases act on. The chart has eight vertices, matching a cubic cell / Freudenthal triangulation neighborhood. Sibling objects include a local vertex type, a concrete Regge star, the area of a regular triangle, the dihedral angle of a regular tetrahedron, area weights (with symmetry), and HasDerivAt statements for area and dihedral angle under uniform scaling.
Upstream, Cayley–Menger encodes $n$-simplex volume from the $C(n+1,2)$ edge lengths; DihedralAngle builds edge and face dihedrals from that CM data; WeakFieldConformalRegge holds the algebraic core of the conformal weak-field reduction of $S$.
proof idea
Definition-heavy geometry module, not a single theorem. It assembles a regular local star on the eight-vertex Freudenthal chart: closed-form regular triangle area and regular tetrahedral dihedral angle (with equality lemmas), nonnegativity/positivity of area, symmetric area weights, and derivative lemmas showing how area and dihedral respond to uniform edge scale.
Proofs are elementary real-analytic checks (Mathlib HasDerivAt, trig inverse, basic algebra) on top of the imported Cayley–Menger and dihedral constructions. No global curvature or full deficit linearization is proved here; the module only pins the local regular model those arguments need.
why it matters in Recognition Science
Sits in the Geometry lane that feeds the weak-field conformal Regge program. The eight-vertex Freudenthal chart is the concrete local complex on which area–deficit pairs and their $\xi$-derivatives are evaluated before summing into $S$. Downstream usage is not yet wired in this graph snapshot (used_by empty), but the import edge from WeakFieldConformalRegge and the Phase C1/C2 docs make the intent clear: supply regular-star primitives so ReggeDeficitLinearizationHypothesis can be discharged on a manageable chart before general complexes.
In the broader RS forcing picture this is infrastructure for the gravity side (Regge action, conformal edges), not a T0–T8 landmark. It closes a modeling gap: without an explicit regular local star, the conformal expansion of $A_h\delta_h$ has nothing concrete to differentiate.
scope and limits
- Does not prove the full Regge deficit linearization hypothesis on general complexes.
- Does not derive Einstein or continuum GR field equations from the local star.
- Does not treat irregular edge lengths beyond the regular/uniform-scale case.
- Does not fix $\kappa$, $G$, or match post-Newtonian observables.
- Does not claim a global eight-tick or $D=3$ forcing result; chart size is local modeling only.
depends on (3)
declarations in this module (21)
-
abbrev
LocalVertex -
structure
ConcreteReggeStar -
def
regularTriangleArea -
theorem
regularTriangleArea_nonneg -
theorem
regularTriangleArea_pos -
def
regularTetrahedralDihedralAngle -
theorem
regularTetrahedralDihedralAngle_eq -
theorem
hasDerivAt_regularTriangleArea -
theorem
hasDerivAt_regularDihedral_uniformScale -
def
regularLocalStar -
def
areaWeight -
theorem
areaWeight_symm -
theorem
areaWeight_nonneg -
def
concreteWeakFieldReggeData -
def
concreteM -
theorem
concreteM_offDiag_eq_neg_areaWeight -
theorem
concreteM_rowSum_zero -
def
concreteReggeComponentComparison -
theorem
concreteReggeSecondVariation_eq_jcostDirichlet -
structure
FreudenthalReggeComponentCert -
theorem
freudenthalReggeComponentCert