pith. machine review for the scientific record. sign in
structure definition def or abbrev high

ExtendedObject

show as:
view Lean formalization →

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.

claimAn 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 in Recognition Science

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.

scope and limits

Lean usage

theorem levitation_example (field : ProcessingField) (ext : ExternalPhaseField) (obj : ExtendedObject) (h : deriv ext.psi obj.h_cm = -(deriv field.phi obj.h_cm)) : modified_coherence_defect field ext obj 0 = 0 := acoustic_levitation field ext obj h

formal statement (Lean)

  38structure ExtendedObject where
  39  h_cm : Position
  40  extent : ℝ
  41  extent_pos : extent > 0
  42
  43/-! ## Frame Dependent Refresh Rate -/
  44
  45/-- Total Potential in a frame accelerating with `a` at position `h` (relative to CM).
  46    Φ_tot(z) ≈ Φ_grav(h_cm + z) + a * z
  47    (Linear approximation for local frame)
  48-/

used by (28)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.