antiGravField
plain-language theorem explainer
The definition constructs an opposing external phase field by negating the gravitational potential function of a processing field. Researchers modeling acoustic levitation or coherence-modified gravity in the Recognition Science setting cite this construction to establish gradient cancellation. It proceeds by a direct record assignment that sets the external psi component to the pointwise negation of the input phi.
Claim. Let $Φ$ be the potential function of a processing field. The associated anti-gravitational field is the external phase field $Ψ$ defined by $Ψ(h) = -Φ(h)$ for every position $h$.
background
ProcessingField is the structure whose phi component supplies the real-valued gravitational potential on positions. ExternalPhaseField is the parallel structure whose psi encodes an external contribution; its doc-comment states that it represents any mechanism (acoustic standing waves, rotating superconductors, phase-locked electromagnetic fields) that modifies the local processing environment. The module combines both via modified coherence defect, which measures the net effect on an extended object at a chosen acceleration.
proof idea
The declaration is a direct definition that builds the ExternalPhaseField record by setting its psi field to the negation of the input ProcessingField's phi. No lemmas are applied and no tactics are used.
why it matters
It supplies the explicit opposing field required by the cancellation theorem antiGravField_cancels and the concrete levitation theorem, both of which conclude that the negated field produces zero coherence defect at zero acceleration. The construction therefore realizes the phase-based counteraction of gravitational gradients inside the Recognition Science treatment of gravity. It leaves open the physical realization of the required external field.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.