WeakFieldPair
plain-language theorem explainer
WeakFieldPair packages a gravitational processing field together with an external one so that their pointwise sum defines the combined field. Gravity modelers working in the Recognition Science weak-field limit cite the structure when they need to decompose coherence defects or gradients into independent contributions. The definition is a direct pointwise addition of the phi components with no extra hypotheses or lemmas.
Claim. Let $F_g$ and $F_e$ be processing fields. A weak-field pair is the structure $(F_g, F_e)$ whose combined field satisfies $F(h) = F_g(h) + F_e(h)$ at every position $h$.
background
ProcessingField, imported from CoherenceFall, is the structure that assigns to each position a real-valued phi representing local J-cost. In the Recognition framework gravitational and external contributions remain independent in the weak regime, so their effects add linearly. Upstream ledger factorization supplies the J-cost calibration while phi-forcing derived results fix the quadratic near-balance behavior that makes the addition consistent.
proof idea
The definition is a one-line wrapper that constructs the combined ProcessingField by pointwise addition of the two phi components. No lemmas or tactics are invoked; the construction is purely structural.
why it matters
WeakFieldPair supplies the data type used by gradient_superposition and coherence_defect_of_combined, which in turn justify the linear addition step inside CoherenceFall. It occupies the weak-field superposition slot in the gravity forcing chain and is compatible with the eight-tick octave and RCL composition law. The structure leaves open the question of how to extend the same additivity beyond the weak regime.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.