logPotentialOf
plain-language theorem explainer
logPotentialOf converts a recognition-potential assignment ψ on n simplices into the additive log-potential field ε with ε_i = ln ψ_i. Workers on the field-curvature identity and the simplicial ledger cite this map when translating scalar potentials into perturbations for edge-length fields. The construction is the direct pointwise application of the natural logarithm.
Claim. Given a recognition potential assignment ψ : Fin n → ℝ, the associated log-potential is the map ε : Fin n → ℝ defined by ε(i) = ln(ψ(i)).
background
The module supplies the missing map from a scalar recognition-potential field ψ on 3-simplices to the geometric edge-length content needed for a Regge action. LogPotential is the type alias Fin n → ℝ that stores the values ε_i = ln ψ(σ_i); the same object appears in the definition of the Laplacian action inside ContinuumBridge. The canonical conformal ansatz then sets each edge length to a · exp((ε_i + ε_j)/2), which collapses to the constant a when all ε vanish.
proof idea
The definition is a one-line wrapper that applies the real logarithm componentwise to the input potential ψ.
why it matters
This definition supplies the concrete translation step required by the field-curvature identity in the Gravity from Recognition draft. It is used inside EdgeLengthFromPsiCert to state the bridge theorem that equates the J-cost Dirichlet energy with the linearized Regge action once the ReggeDeficitLinearizationHypothesis is discharged. The parent result logPotentialOf_flat shows that the flat vacuum ψ ≡ 1 produces the zero log-potential, anchoring the perturbative expansion around flat space.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.