Padd
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not assert nonzero cross derivative or entanglement.
- Does not satisfy or derive from the Recognition Composition Law.
- Does not apply outside real arguments.
- Does not perform derivative or difference computations.
formal statement (Lean)
51def Padd (u v : ℝ) : ℝ := 2 * u + 2 * v
proof body
Definition body.
52
53/-- Padd is separable: P(u,v) = 2u + 2v = α(u) + β(v). -/