PsiPotential
plain-language theorem explainer
PsiPotential supplies the potential contribution to the ψ-sector action in the ILG construction. It is referenced when forming the complete action or verifying the general-relativity limit. The definition is a direct delegation to the potential_action integrator supplied by the Fields module, using the square of the lag coupling as the effective mass-squared parameter.
Claim. The ψ-sector potential term is defined by $ (C^2/2) ∫ √(-g) ψ² d⁴x $, where C is the lag coupling and the integral employs the default volume element on the metric g.
background
In the ILG.Action module, geometry and field types are re-exported for use in the integrated Lagrangian gravity construction. The Metric abbreviation stands for the metric tensor from Geometry, while RefreshField denotes the scalar field from Fields. The lag parameter C_lag originates from the eight-tick resonance module as φ^{-5}. The potential_action routine from Fields.Integration computes the integral (m²/2) ∫ √(-g) φ² d⁴x for a given mass-squared value.
proof idea
This is a one-line wrapper that invokes Fields.potential_action on the supplied scalar field, with mass-squared set to C_lag squared, the metric, and the default volume element.
why it matters
PsiPotential is called by PsiAction and by the reduction theorems gr_limit_reduces and gr_limit_zero that recover the Einstein-Hilbert action when the lag and kinetic coefficients vanish. It supplies the mass-like term in the ψ-sector, whose coupling strength is fixed by the Recognition Science forcing chain at T5 through the value C_lag = φ^{-5}. This completes the action functional needed for the subsequent variation and field equations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.