ExtendedObject
plain-language theorem explainer
ExtendedObject defines a finite-size object via center-of-mass position in the reals, positive extent, and the positivity witness. Acoustic levitation and coherence-coupling theorems cite it to compute how external phase gradients modify gravitational defects at the object's location. The declaration is a direct structure with one inequality field and no further proof obligations.
Claim. An extended object is a triple $(h_{cm}, e, p)$ where $h_{cm} : Position$, $e : ℝ$, and $p$ is a proof that $e > 0$.
background
Position is the abbreviation for the real numbers and serves as the spatial coordinate in this one-dimensional gravity model. The CoherenceFall module develops linear approximations to total potential in accelerating frames, Φ_tot(z) ≈ Φ_grav(h_cm + z) + a·z, to track coherence-restoring accelerations for objects of finite size. The upstream UniversalForcingSelfReference.for structure records the meta-realization axioms that underwrite the self-reference properties used in all coherence calculations.
proof idea
This is a structure definition. The three fields h_cm, extent, and extent_pos are introduced directly; no lemmas or tactics are invoked.
why it matters
ExtendedObject supplies the object type for the LEVITATION THEOREM (acoustic_levitation) and its siblings complete_cancellation_is_levitation and anti_coherence_reduces_coupling. These results show that an opposing external phase gradient can drive effective gravitational coupling to zero, deriving acoustic levitation from RS coherence principles. The structure thereby extends point-particle models to finite bodies within the T5–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.