LogPotential
plain-language theorem explainer
LogPotential n is the function type assigning a real number ε_i to each of n vertices, with ε_i defined as the natural logarithm of the recognition potential ψ evaluated at the corresponding simplex. Researchers deriving the field-curvature identity in the Recognition framework cite this type when expressing conformal edge lengths and the Laplacian action in terms of potential differences. The declaration is a direct type abbreviation with no further computational content.
Claim. For positive integer $n$, a log-potential assignment is any function $ε : Fin n → ℝ$ such that $ε_i = ln ψ(σ_i)$, where $ψ$ denotes the recognition potential on simplices and $σ_i$ labels the $i$-th vertex.
background
The module supplies the map from the scalar recognition-potential field $ψ$ on 3-simplices to an edge-length field $L_e$ on edges, required to define a Regge action. LogPotential n is the type of assignments $ε : Fin n → ℝ$ with $ε_i = ln ψ(σ_i)$. This object is the common domain for the Laplacian action in ContinuumBridge and for the conformal edge-length field defined in the same file.
proof idea
The declaration is a one-line type abbreviation that identifies LogPotential n with the function type Fin n → ℝ. No lemmas are applied; the definition is transparent and serves as the common domain for laplacian_action and conformal_edge_length_field.
why it matters
This definition supplies the domain for the log-potential field ε used in the field-curvature identity theorems. It feeds directly into bridge_chain_complete and field_curvature_identity_einstein in ContinuumTheorem, where the identity laplacian_action G ε = (1/κ_Einstein) · regge_sum holds once the linearization hypothesis is discharged. The construction closes the tautology in the Gravity from Recognition draft by naming the map from ψ to edge lengths, with κ = 8 φ^5. It touches the open question of discharging ReggeDeficitLinearizationHypothesis from explicit Cayley-Menger or Piran-Williams computations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.