pith. sign in
module module moderate

IndisputableMonolith.Gravity.CoherenceFall

show as:
view Lean formalization →

The CoherenceFall module supplies the linear approximation for total potential in an accelerating local frame together with coherence defect measures. It is used by levitation, energy bridge, and weak-field superposition calculations in the Gravity domain. This is a definition module with no proofs.

claim$Φ_{tot}(z) ≈ Φ_{grav}(h_{cm} + z) + a z$ for an accelerating frame with acceleration $a$ at displacement $z$ relative to the center of mass; the module also defines coherence_defect and related objects on Position, ProcessingField, and ExtendedObject.

background

The module operates inside the Gravity subdomain of Recognition Science and imports only Mathlib. It introduces the basic types Position, ProcessingField, and ExtendedObject, then defines total_potential_in_frame as the sum of the gravitational potential evaluated at the shifted center-of-mass coordinate plus the linear acceleration term. Additional siblings define coherence_defect, its expansion and simplification, and the statement that falling restores coherence.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the local-frame potential and defect objects required by AcousticPhaseLevitation, EnergyProcessingBridge, and WeakFieldSuperposition. It implements the linear approximation described in the module doc-comment for use in coherence calculations within the Recognition Science gravity chain.

scope and limits

used by (3)

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

declarations in this module (8)