logPotentialOf_flat
plain-language theorem explainer
The declaration shows that a constant recognition potential of unity on any finite collection of simplices produces a vanishing log-potential field. Workers on the simplicial discretization of the J-cost action cite this identity to confirm the flat-space base case of the field-curvature bridge. The argument is a term-mode reduction that applies function extensionality followed by the definition of the log-potential operator and the elementary identity that the logarithm of one vanishes.
Claim. Let $n$ be a natural number and let $ψ$ be the constant function on the $n$ simplices with value $1$. Let $ε$ be the log-potential field defined by $ε(i) = log ψ(i)$. Then $ε$ is the zero function.
background
The module constructs the map from a scalar recognition-potential field $ψ$ on 3-simplices to the edge-length field required for a Regge action. The log-potential $ε$ is the pointwise natural logarithm of $ψ$, so that differences $ε_i - ε_j$ encode the leading-order relative edge-length changes under linearization. The local setting is the simplicial ledger that closes the identification between the J-cost Dirichlet energy and the linearized Regge action with coupling $κ = 8 φ^5$. Upstream, the Constants module supplies the identity $κ_{Einstein} = 8 φ^5$ obtained by substituting the RS-native definitions $G = λ_{rec}^2 c^3 / (π ℏ)$ and $ℏ = φ^{-5}$ with $λ_{rec} = c = 1$.
proof idea
The proof applies function extensionality to reduce the equality of functions to a pointwise claim. It then unfolds the definition of the log-potential operator and invokes the standard lemma that the real logarithm of unity equals zero.
why it matters
This flat-case identity is invoked inside the certification theorem that assembles the bridge from J-cost to Regge action under the linearization hypothesis. It supplies the zero-curvature sector of the field-curvature identity in the Gravity from Recognition draft. The parent result is the edgeLengthFromPsiCert theorem that packages the full map from $ψ$ to edge lengths together with the flat Regge sum and flat J-cost evaluations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.