total_potential_in_frame
plain-language theorem explainer
Definition of total potential in an accelerating frame adds the gravitational potential evaluated at an object's center of mass to an inertial term linear in relative height and frame acceleration. Researchers modeling coherence defects or equivalence-principle effects in Recognition Science gravity calculations cite this expression. The definition proceeds by direct arithmetic combination of the field's potential function with the acceleration contribution.
Claim. For a field with potential function $Φ$ and an extended object whose center of mass lies at height $h_{cm}$, the total potential at relative coordinate $z$ in a frame accelerating vertically with $a$ is $Φ(h_{cm} + z) + a z$.
background
ProcessingField is a structure containing a potential function $Φ$ that maps positions to reals. ExtendedObject records a center-of-mass height $h_{cm}$ together with a positive extent. The module Gravity.CoherenceFall develops expressions for coherence defects that arise when this total potential varies across an object. Upstream structures from PhiForcingDerived supply the J-cost framework that calibrates the underlying potentials, while NucleosynthesisTiers organizes physical quantities into discrete phi-tiers.
proof idea
The definition evaluates the field's phi at the center of mass, adds the first-derivative correction times the relative coordinate $z$, and adds the product of acceleration $a$ with $z$. It is a direct arithmetic expression with no lemma applications.
why it matters
This definition is invoked by the coherence_defect computation in the same module to obtain the absolute difference in potential between the extremities of the object. It supplies the local-frame potential required for the Recognition Science analysis of gravitational coherence, linking to the phi-ladder and the derivation of three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.