total_potential_in_frame
The definition supplies the total potential felt by an extended object in a locally accelerating frame by linearly approximating the gravitational potential around its center of mass and superposing the inertial contribution. Researchers studying equivalence-principle effects or coherence loss in gravitational fields would cite this construction. The body executes a first-order Taylor expansion of the supplied phi function plus the term a times relative height z.
claimLet $Phi$ be the potential function of a processing field, $h_{cm}$ the center-of-mass position of an extended object with positive extent, $a$ the frame acceleration, and $z$ the relative height. Then the total potential is $Phi(h_{cm}) + Phi'(h_{cm}) cdot z + a cdot z$.
background
A ProcessingField is a structure containing a potential function phi mapping Position to real numbers. An ExtendedObject consists of a center-of-mass height h_cm together with a positive extent. The module Gravity.CoherenceFall develops expressions for potential differences across falling objects to quantify coherence defects. Upstream results supply the phi accessor and derivative operator, while related structures encode nuclear densities in phi-tiers and variance functionals on discrete domains.
proof idea
The definition implements the linear approximation directly: it evaluates the gravitational potential at the center of mass, adds the first derivative times z, and adds the inertial term a*z. No lemmas are invoked beyond the structure projections and the derivative operator.
why it matters in Recognition Science
This definition is invoked by coherence_defect to compute the absolute difference in total potential between the head and feet of the object. It supplies the local-frame potential needed to quantify how acceleration restores or disrupts coherence. The construction aligns with the equivalence principle by combining gravitational and inertial potentials linearly.
scope and limits
- Does not include quadratic or higher terms in the Taylor expansion of the potential.
- Does not account for non-uniform gravitational fields beyond the linear term.
- Does not specify the orientation of the acceleration vector a.
- Does not incorporate relativistic corrections.
formal statement (Lean)
49def total_potential_in_frame (field : ProcessingField) (obj : ExtendedObject) (a : ℝ) (z : ℝ) : ℝ :=
proof body
Definition body.
50 -- Taylor expand phi around h_cm: phi(h_cm) + phi'(h_cm) * z
51 let phi_grav := field.phi obj.h_cm + (deriv field.phi obj.h_cm) * z
52 -- Inertial potential from acceleration a (pointing up? a is vertical acceleration)
53 -- If object accelerates down (a < 0), inertial force is up.
54 -- Potential Φ_acc such that F = -∇Φ_acc. F_inertial = -a, hence Φ_acc = a * z.
55 let phi_acc := a * z
56
57 phi_grav + phi_acc
58
59/-- Coherence Defect: Variance of the potential across the object.
60 If Potential is flat, Defect is 0.
61-/