superposition_cross_term
plain-language theorem explainer
The superposition cross term isolates the nonlinear interaction between two weak strains ε₁ and ε₂ in the J-cost decomposition for superimposed gravitational fields. Workers on weak-field gravity models in Recognition Science cite this when separating additive and cross contributions to total energy. The definition is introduced directly as the difference Jcost(1 + ε₁ + ε₂) minus the separate terms.
Claim. The cross-term correction in the J-cost decomposition is given by $J(1 + ε_1 + ε_2) - J(1 + ε_1) - J(1 + ε_2)$, where $J$ is the J-cost function.
background
The module develops weak-field approximations for combined gravitational strains using the J-cost function. J-cost, structured in PhiForcingDerived, quantifies recognition cost for scale factors via the form (x + x^{-1})/2 - 1. Ledger factorization from DAlembert supplies the underlying multiplicative calibration of scales in (R_+, ×).
proof idea
This is a direct definition that subtracts the individual J-cost terms from the combined term to isolate the cross contribution. It applies the J-cost structure from PhiForcingDerived with no additional lemmas or tactics.
why it matters
This definition feeds the theorem cross_term_factored, which factors the cross term as ε₁ ε₂ times a rational function of the strains. It isolates nonlinear corrections in weak-field gravity, aligning with J-uniqueness from T5 in the forcing chain and the energy processing bridge. The parent result supports decomposition in the Recognition framework without addressing strong-field extensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.