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

ExternalPhaseField

show as:
view Lean formalization →

ExternalPhaseField structures an external phase potential as a real-valued function psi on positions, with its gradient defined by direct differentiation. Researchers modeling acoustic levitation or coherence-modified gravity in Recognition Science cite it to represent opposing fields from standing waves or superconductors. The definition is a direct structure declaration whose gradient operation feeds into cancellation arguments without additional lemmas.

claimAn external phase field is a function $psi : Position → ℝ$ together with its gradient $∇psi(h) := d psi / dh$ at each position $h$.

background

The AcousticPhaseLevitation module treats gravity as a coherence-restoring process that can be offset by external phase contributions. ExternalPhaseField supplies the mathematical carrier for any such offset, whether acoustic standing waves, rotating superconductors, or phase-locked electromagnetic fields. Upstream, the construction relies on the eight-tick phase definition (periodic with period 2π) and the Defect functional that vanishes when structural checks pass; LedgerFactorization supplies the underlying J-calibration for potentials.

proof idea

The declaration is a direct structure definition with a single field psi. Its gradient is introduced as the one-line wrapper deriv ext.psi h, which extracts the ordinary derivative without further reduction or tactic steps.

why it matters in Recognition Science

ExternalPhaseField supplies the type parameter for the acoustic_levitation theorem, which states that exact gradient cancellation yields zero modified coherence defect. It thereby realizes the framework's claim that any phase source opposing the gravitational gradient produces levitation. The structure also supports the anti-coherence coupling reduction and complete-cancellation results, linking directly to eight-tick resonance and the phi-ladder processing environment.

scope and limits

formal statement (Lean)

  63structure ExternalPhaseField where
  64  psi : Position → ℝ
  65
  66/-- The gradient of the external field at a given position. -/
  67def ExternalPhaseField.gradient (ext : ExternalPhaseField) (h : Position) : ℝ :=

proof body

Definition body.

  68  deriv ext.psi h
  69
  70/-! ## 2. Modified Coherence Defect -/
  71
  72/-- Total potential when BOTH gravitational and external phase fields are present,
  73    in a frame accelerating with `a`.
  74    Φ_total(z) = Φ_grav(h_cm + z) + Φ_ext(h_cm + z) + a·z
  75    (linearized around center of mass) -/

used by (21)

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

depends on (19)

Lean names referenced from this declaration's body.