cross_term_factored
plain-language theorem explainer
cross_term_factored shows that the superposition cross term for two weak strains ε₁ and ε₂ equals the difference of their normalized squared contributions. Workers on weak-field gravity models in Recognition Science cite the identity when verifying additive processing costs for independent fields. The proof is a direct algebraic reduction that applies the exact J-cost formula for one-plus strains three times.
Claim. Let ε₁, ε₂ be real numbers with ε₁ > -1, ε₂ > -1 and ε₁ + ε₂ > -1. Then the cross term in the weak-field superposition satisfies superposition_cross_term(ε₁, ε₂) = (ε₁ + ε₂)² / (2(1 + ε₁ + ε₂)) - ε₁² / (2(1 + ε₁)) - ε₂² / (2(1 + ε₂)).
background
The J-cost function J(x) = (x + x^{-1})/2 - 1 quantifies processing strain; the lemma Jcost_one_plus_exact states that J(1 + ε) = ε² / (2(1 + ε)) whenever ε > -1. In the WeakFieldSuperposition module, two independent processing fields (gravitational plus external) combine by strain addition in the weak regime, with the cross term isolated via the independence semantics of LNALSemantics and RSCoupledAxis. The local setting is the weak-field limit where combined effects remain linear sums of strains, consistent with the module's focus on processing-field superposition.
proof idea
The proof unfolds the definition of superposition_cross_term and rewrites each term by applying Jcost_one_plus_exact to the summed strain, the first strain, and the second strain under the three supplied inequalities.
why it matters
The identity supplies the algebraic detail needed for cross-term factoring in weak-field gravity, feeding the coherence_defect_of_combined and SuperpositionJustification siblings in the same module. It realizes the interaction piece of the Recognition Composition Law under the J-uniqueness (T5) step of the forcing chain and the eight-tick octave structure. No open scaffolding questions are addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.