coherence_defect
plain-language theorem explainer
Coherence defect quantifies potential variance across an extended object as the absolute difference between total potentials at its head and feet in an accelerating frame. Researchers deriving the coherence-seeking account of gravity within Recognition Science cite this when establishing equilibrium accelerations. The definition is a direct computation that invokes the total potential helper at symmetric positions around the center of mass and applies the absolute value.
Claim. The defect measuring potential variance is defined as $|Φ_{tot}(e) - Φ_{tot}(-e)|$, where the total potential is the linear approximation $Φ_{tot}(z) = ϕ(h_{cm}) + ϕ'(h_{cm}) z + a z$ for a potential function $ϕ$, center-of-mass position $h_{cm}$, and positive extent $e$.
background
The CoherenceFall module treats gravitational acceleration as the frame adjustment that eliminates potential variance across an object. A ProcessingField is a structure containing a potential function phi from Position to real numbers. An ExtendedObject is a structure specifying a center-of-mass position h_cm together with a positive extent. The supporting definition total_potential_in_frame supplies the linearized total potential Φ_tot(z) ≈ ϕ(h_cm + z) + a · z, obtained by first-order Taylor expansion of the gravitational potential plus the inertial term from frame acceleration.
proof idea
The definition directly evaluates total_potential_in_frame at the positive extent and at the negative extent, then returns the absolute value of the difference. It is a one-line wrapper that applies the total potential helper twice and performs the absolute-value operation; no lemmas are invoked inside the definition body.
why it matters
This definition supplies the concrete mechanism for the claim that gravity restores coherence. It is referenced inside LevitationInevitability to assert existence of a unique restoring acceleration and inside ForcingChainToLevitation as the first step of the chain from Recognition Science primitives to levitation. The downstream theorem falling_restores_coherence shows that the zero-defect acceleration equals the negative gradient of the potential, recovering Newtonian gravity. It thereby anchors the local gravity model to the broader forcing chain that reaches T8 dimension and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.