total_potential_in_frame
plain-language theorem explainer
Definition of total potential experienced by an extended object in an accelerating frame, formed by adding the first-order Taylor expansion of the gravitational potential around the center of mass to the inertial term a*z. Researchers working on coherence defects in Recognition Science gravity models cite this when quantifying potential gradients across finite bodies. The body is an explicit arithmetic construction that binds the two contributions separately before summing.
Claim. $Φ_{tot}(z) = ϕ(h_{cm} + z) + a z$, where ϕ is the potential function of the processing field, h_cm the center-of-mass position of the extended object, a the frame acceleration, and z the vertical offset from the center of mass.
background
ProcessingField is a structure containing a potential function ϕ : Position → ℝ. ExtendedObject is a structure containing center-of-mass position h_cm, positive extent, and the proof that extent > 0. The module Gravity.CoherenceFall develops frame-dependent potentials to study coherence defects arising from non-uniform total potential across extended objects. The supplied doc-comment states the linear approximation Φ_tot(z) ≈ Φ_grav(h_cm + z) + a * z for the local frame.
proof idea
The definition binds phi_grav to field.phi obj.h_cm plus the derivative of field.phi at h_cm multiplied by z, binds phi_acc to a * z, and returns their sum. No lemmas from the depends_on list are invoked; the construction is a direct let-expression with inline comments explaining each term.
why it matters
The definition is called by coherence_defect to obtain the absolute difference between potentials at +extent and -extent, which quantifies the coherence defect as zero only when the total potential is flat. It supplies the concrete local-frame step inside the gravity module, connecting to the Recognition Composition Law through additive potentials and to the phi-ladder via the ProcessingField structure. The downstream doc-comment notes that a flat potential yields defect zero.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.