IsSeparable
plain-language theorem explainer
A binary combiner P from pairs of reals to reals is separable when it decomposes exactly as the sum of a univariate function of the first argument and one of the second. Researchers working on the DAlembert entanglement gate and the AnalyticBridge lemmas cite this definition to separate additive behavior from the interacting 2uv term in the Recognition Composition Law. The declaration is supplied directly as an existential statement over two real-valued functions with no further proof steps.
Claim. A function $P : ℝ × ℝ → ℝ$ is separable if there exist functions $α, β : ℝ → ℝ$ such that $P(u,v) = α(u) + β(v)$ for all real $u,v$.
background
The Entanglement Gate module characterizes combiners P by whether their mixed second derivative vanishes. The additive combiner P(u,v) = 2u + 2v has zero cross-derivative and is separable, while the RCL combiner P(u,v) = 2uv + 2u + 2v has cross-derivative 2 and is entangling. This distinction encodes the physical claim that observing a composite xy is not merely the sum of separate observations of x and y.
proof idea
This declaration is a definition. It encodes separability by the direct existential quantification over univariate maps α and β that satisfy the additive decomposition for every pair of inputs. No lemmas or tactics are applied; the body simply states the quantified statement matching the module doc-comment.
why it matters
The definition supplies the predicate used in downstream AnalyticBridge results, including differentiation_key_lemma that connects combiner type to ODE type and separable_combiner_forces_flat that derives G'' = 1 from separability. It marks the boundary between the additive case and the entangling case required by the Recognition Composition Law, supporting the emergence of interaction terms inside the T0-T8 forcing chain while preserving the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.