pith. sign in
module module high

IndisputableMonolith.Gravity.WeakFieldSuperposition

show as:
view Lean formalization →

This module establishes additive splitting of J-cost for superposed weak strains, with the cross term bounded as O(ε₁ε₂). Gravitational coherence and acoustic levitation calculations cite it when linearizing combined fields. The derivations rest on direct substitution into the closed-form identity J(1+ε) = ε²/(2(1+ε)) to isolate quadratic leading terms.

claimFor small strains ε₁, ε₂, J(1 + ε₁ + ε₂) = J(1 + ε₁) + J(1 + ε₂) + O(ε₁ ε₂), where the exact relation is J(1 + ε) = ε² / (2(1 + ε)).

background

Recognition Science obtains the J-cost from the forcing chain T0-T8, yielding the exact functional form J(x) = (x + x^{-1})/2 - 1 that reduces to ε²/(2(1+ε)) for strains written as 1 + ε. The module sits inside the gravity domain and imports CoherenceFall for defect measures together with EnergyProcessingBridge for energy relations under the Recognition Composition Law.

proof idea

The module defines WeakFieldPair and proves lemmas Jcost_additive_leading, superposition_cross_term, and cross_term_factored by algebraic expansion of the exact J identity, followed by order estimates that separate the quadratic terms from the bilinear remainder. SuperpositionJustification assembles the results into a single usable statement.

why it matters in Recognition Science

The module supplies the weak-field superposition rule required by AcousticPhaseLevitation for combined gravitational-acoustic calculations. It bridges the exact RCL to practical approximations inside the D=3, eight-tick structure of the gravity chain.

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)