Padd
plain-language theorem explainer
Padd defines the additive combiner P(u, v) = 2u + 2v as the separable counterexample in entanglement gate analysis. Researchers contrasting interaction terms under the Recognition Composition Law cite it to isolate cases with vanishing cross derivatives. The definition is introduced by direct assignment of the linear expression.
Claim. The additive combiner is defined by $P(u, v) := 2u + 2v$.
background
The Entanglement Gate module requires that any combiner P satisfy a nonzero mixed second derivative to encode interaction: observing the composite xy is not merely the sum of separate observations of x and y. The additive combiner Padd supplies the separable baseline where this derivative vanishes. The module quotes the physical reading that entanglement arises precisely from the 2uv term in the Recognition Composition Law.
proof idea
The declaration is a direct definition that assigns the expression 2 * u + 2 * v. No lemmas, tactics, or reductions are applied.
why it matters
Padd supplies the separable counterexample required by the Entanglement Gate Theorem, which states that J-cost has interaction and therefore any consistent combiner must be entangling while Padd is not. It is invoked in Padd_not_entangling, Padd_mixed_diff_zero, Fquad_consistency, and additive_not_entangling. This isolates the necessity of the cross term from the Recognition Composition Law against additive structures that fail the interaction test.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.