IndisputableMonolith.Foundation.SimplicialLedger.InteriorFlat
The InteriorFlat module defines FlatInteriorMetric on 3-simplices to record a signature choice and the Regge axiom for flat interiors in the simplicial ledger. Discrete gravity researchers cite it when linking J-cost stationarity to Regge calculus. The module supplies axiomatic properties and default Euclidean or Minkowski cases rather than explicit isometry constructions.
claimA FlatInteriorMetric on a 3-simplex consists of a signature $s$ with $s = +1$ for Euclidean or $s = -1$ for Minkowski, a positivity witness ensuring edge lengths satisfy Cayley-Menger conditions in signature $s$, and the Regge axiom asserting that the simplex interior is isometric to the standard flat simplex of signature $s$.
background
This module sits inside the simplicial ledger, which models the RS ledger as a coordinate-free simplicial 3-complex and sheaf for local J-cost variations. It imports the ContinuumBridge, whose doc-comment states that J-cost equals the Regge action up to normalization by $8 phi^5$ and that stationarity of J-cost recovers the Regge equations. Constants supplies the base time quantum $tau_0 = 1$ tick. The central object is FlatInteriorMetric, which encodes the signature, Cayley-Menger positivity, and the flat-isometry property as a Prop because full geometric machinery lies outside the current stack.
proof idea
This is a definition module, no proofs. It declares the FlatInteriorMetric structure, default Euclidean and Minkowski instances, InteriorLoop, Hinge, NonHingeStratum, and curvature-only-on-hinges lemmas. The module relies on Mathlib imports for real numbers, inner-product spaces, and symmetric matrices to support the metric and positivity witnesses.
why it matters in Recognition Science
The definitions here supply the flat-interior axioms that let the simplicial ledger interface with the ContinuumBridge. They enable the identification of J-cost with the Regge action and the passage from discrete stationarity to the Regge equations, which in turn support the derivation of Einstein field equations. The module therefore closes part of the discrete-to-continuum gap while respecting the D=3 spatial setting and the eight-tick octave of the Recognition framework.
scope and limits
- Does not construct explicit isometries for the Regge axiom.
- Does not treat curved interiors inside a single simplex.
- Does not extend metric definitions past 3-simplices.
- Does not compute numerical edge lengths or deficit angles.
depends on (3)
declarations in this module (16)
-
structure
FlatInteriorMetric -
def
defaultEuclideanInterior -
def
defaultMinkowskiInterior -
def
InteriorLoop -
theorem
trivial_interior_loop -
theorem
interior_holonomy_trivial -
structure
Hinge -
inductive
NonHingeStratum -
def
deficitOnNonHinge -
theorem
curvature_only_on_hinges -
structure
FlatInteriorLedger -
def
canonicalEuclideanEnrichment -
def
canonicalMinkowskiEnrichment -
theorem
interior_jcost_const_consistent -
structure
InteriorFlatCert -
def
interiorFlatCert