pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi

show as:
view Lean formalization →

This module defines the log-potential assignment ε : Fin n → ℝ with ε_i = ln ψ(σ_i) on a simplicial 3-complex together with the derived conformal edge length field. It supplies the exact object referenced by laplacian_action in the ContinuumBridge. Researchers proving the discrete-to-continuum passage in Recognition Science cite it as the source of the potential used for Regge action identification. The module contains only definitions and no proofs.

claimThe module introduces the log-potential assignment $ε : Fin n → ℝ$ given by $ε_i = ln ψ(σ_i)$ and the conformal edge length field $ℓ_{ij} = ℓ_0 exp((ε_i + ε_j)/2)$ together with the associated hinge datum and deficit angle functional.

background

The module belongs to the SimplicialLedger hierarchy that replaces the fixed cubic lattice with a coordinate-free 3-complex sheaf. It imports Constants (τ₀ = 1 tick), Cost (J-functional), the parent SimplicialLedger (sheaf representation unifying local and global J-cost), and ContinuumBridge (J-cost stationarity to discrete Ricci). The central object is the log-potential ε drawn directly from the laplacian_action construction that converts J-cost variations into curvature terms.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The definitions supply the log-potential and edge-length constructions required by ContinuumTheorem (Phase D of the field-curvature identity program) and by CubicDeficitDischarge (Phase A). They are also imported by CubicSimplicialEquivalence, NonlinearBridge, SimplicialDeficitDischarge, and WeakFieldConformalRegge, which together address Beltracchi §5–6 concerns on simplicial equivalence and the nonlinear regime. The module thereby prepares the identification of the J-cost functional with the Regge action S = (1/κ) Σ A_h δ_h under the conformal ansatz.

scope and limits

used by (6)

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

depends on (4)

Lean names referenced from this declaration's body.

declarations in this module (18)