pith. sign in
module module high

IndisputableMonolith.Gravity.WeakFieldSuperposition

show as:
view Lean formalization →

The WeakFieldSuperposition module establishes additive splitting of J-cost for small gravitational strains, with the cross term second-order in the product of strains. Models of multi-body gravitational coherence and acoustic levitation cite these results. The argument rests on direct substitution of the exact identity J(1+ε) = ε²/(2(1+ε)) followed by algebraic isolation of the O(ε1 ε2) remainder.

claimFor small strains $ε_1, ε_2$, $J(1 + ε_1 + ε_2) = J(1 + ε_1) + J(1 + ε_2) + O(ε_1 ε_2)$, where the leading contributions are quadratic and the exact local form is $J(1+ε) = ε^2 / (2(1+ε))$.

background

The module sits in the gravity domain and imports CoherenceFall together with EnergyProcessingBridge. It works in the weak-field regime where strains remain small enough that quadratic terms dominate. The central object is the J-cost function, whose exact expression on a strained interval is given by the supplied identity.

proof idea

The module organizes its content around the exact identity J(1+ε) = ε²/(2(1+ε)). It first extracts the additive leading quadratic term, then isolates the bilinear cross term and factors it explicitly. Supporting siblings establish the O(ε1 ε2) bound and the factored remainder.

why it matters in Recognition Science

The module supplies the superposition property required by AcousticPhaseLevitation. It justifies treating combined weak strains as sums of individual J-costs plus a controlled correction, consistent with the Recognition Science forcing chain and J-uniqueness. The results close the step from single-body to multi-body gravitational coherence.

scope and limits

used by (1)

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

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)