crossDeriv
plain-language theorem explainer
The crossDeriv definition supplies the mixed second partial of a bivariate real function P at a point (u,v). Workers on the entanglement characterization inside the DAlembert layer cite it to separate additive from interacting combiners. The definition is a direct one-line encoding of iterated differentiation via the standard real derivative operator.
Claim. For a function $P:ℝ×ℝ→ℝ$, the cross-derivative at the point $(u,v)$ is the iterated partial $∂_u(∂_v P)(u,v)$.
background
The module introduces the Entanglement Gate as the requirement that a combiner P exhibit nonzero cross-derivative ∂²P/∂u∂v. Under this gate the additive combiner 2u+2v is separable while the RCL combiner 2uv+2u+2v is entangling; the distinction is exactly the presence or absence of the interaction term 2uv. The crossDeriv definition records that interaction term for any smooth P.
proof idea
The declaration is a direct definition that applies the real derivative operator twice: first with respect to the second argument, then with respect to the first. No lemmas are invoked beyond the standard deriv combinator from the imported analysis library.
why it matters
The definition anchors the Entanglement Gate results that follow in the same module, including the separability of the additive combiner and the entangling property of the RCL combiner. It thereby supplies the concrete differential test that distinguishes coupled from independent observations inside the Recognition Composition Law. The gate itself sits at the foundation layer that feeds the eight-tick octave and spatial-dimension derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.