ProcessingField
plain-language theorem explainer
ProcessingField packages a real-valued potential function on the height coordinate. Acoustic levitation and coherence-coupling theorems cite it when an external phase gradient must cancel the gravitational gradient. The declaration is a bare structure definition introducing one field of type Position → ℝ.
Claim. A processing field is a function $Φ : ℝ → ℝ$ that supplies the gravitational potential at each height.
background
Position is the real line used as the one-dimensional height coordinate. The CoherenceFall module expresses gravitational effects through coherence defects whose magnitude depends on the derivative of this potential. The single upstream dependency is the abbrev that sets Position := ℝ.
proof idea
This is a structure definition with no proof obligations or computational content.
why it matters
The structure supplies the gravitational potential input to every downstream theorem in AcousticPhaseLevitation, including acoustic_levitation (which requires deriv field.phi to be cancelled by an external field) and anti_coherence_reduces_coupling. It therefore supplies the concrete link between the Recognition Science coherence defect and a classical gravitational gradient without invoking general relativity or the full T0-T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.