pith. sign in
module module high

IndisputableMonolith.Foundation.SimplicialLedger.CubicDeficitDischarge

show as:
view Lean formalization →

The CubicDeficitDischarge module recovers the conformal parameters ε_i from self-loop edge lengths via L_ii = a exp(ε_i) on the cubic lattice. Researchers closing the discrete-to-continuum bridge in Recognition Science cite it when linearizing Regge deficits for the field-curvature identity. The module supplies explicit recovery maps, cubicDeficit and cubicArea functionals, and their basic properties as definitions and short lemmas.

claimGiven a conformal edge-length field satisfying $L_{ii}=a\exp(\varepsilon_i)$, the recovery map is $\varepsilon_i=\log(L_{ii}/a)$. The module defines the associated cubic deficit functional and cubic area on the hypercubic lattice together with their non-negativity and singleton cases.

background

The module operates inside the SimplicialLedger hierarchy that converts the RS recognition ledger into Regge calculus. It imports Constants (τ₀ = 1 tick), ContinuumBridge (J-cost functional equals the Regge action up to κ = 8φ⁵), and EdgeLengthFromPsi (scalar recognition potential ψ on 3-simplices determines all edge lengths). These upstream results supply the J-cost stationarity condition and the identification of ψ with geometric data required for the discrete Ricci tensor.

Sibling definitions inside the module implement recoverEps, recoverEps_conformal, cubicDeficit, cubicArea, and their singleton and product variants. The local setting is the hypercubic lattice before passage to a full simplicial triangulation, exactly the setting needed for Phase A of the field-curvature program.

proof idea

This is a definition module, no proofs. It consists of explicit recovery functions (recoverEps, recoverEps_conformal) built from logarithm and exponential, followed by direct definitions of cubicDeficit and cubicArea together with elementary lemmas (non-negativity, singleton cases, product identity) that follow by algebraic substitution.

why it matters in Recognition Science

The module supplies the cubic-specific linearization and discharge tools required by ContinuumTheorem (Phase D of the field-curvature identity at κ = κ_Einstein) and by SimplicialDeficitDischarge (Phase C5). It also supplies the cubic side of the cubic-simplicial equivalence addressed in CubicSimplicialEquivalence, thereby completing the concrete lattice case of the paper's Theorem 5.1.

scope and limits

used by (3)

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

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (19)