Pith. sign in
module module high

IndisputableMonolith.Foundation.SimplicialLedger.InteriorFlat

show as:
view Lean formalization →

This module defines FlatInteriorMetric on 3-simplices to record a signature choice, Cayley-Menger positivity witness, and Regge axiom of flat isometry. It equips the simplicial ledger with flat Euclidean or Minkowski interiors for discrete J-cost calculations. The module supplies only definitions and properties; no proofs are present.

claimA flat interior metric on a 3-simplex consists of a signature $s \in \{-1,+1\}$, a positivity witness ensuring edge lengths satisfy the Cayley-Menger conditions for flat space of signature $s$, and the property that the simplex interior is isometric to the standard simplex in flat space of that signature.

background

The simplicial ledger represents the RS J-cost on a coordinate-free 3-complex. Constants supplies the base time quantum $\tau_0 = 1$ tick. ContinuumBridge identifies the J-cost functional with the Regge action (normalized by $\kappa = 8\phi^5$) and shows that its stationarity recovers the Regge equations.

FlatInteriorMetric encodes the local flatness assumption needed for that identification. The signature distinguishes Euclidean ($s = +1$) from Lorentzian ($s = -1$) interiors; the positivity witness guarantees embeddability in flat space via the Cayley-Menger determinant; the Regge axiom asserts the required isometry as a property.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the flat-interior data required by the simplicial ledger to interface with the continuum bridge. It thereby supports the claim that J-cost stationarity yields the Regge equations in flat regions, advancing the discrete-to-continuum step in the Recognition framework.

scope and limits

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (16)