ExternalPhaseField
plain-language theorem explainer
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.
Claim. An 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.