IndisputableMonolith.Foundation.DAlembert.EntanglementGate
The module defines separable and entangling combiners P for the equation F(xy) + F(x/y) = P(F(x), F(y)). Separable means P(u,v) = α(u) + β(v) for some α, β; entangling means the mixed second difference is nonzero. Researchers auditing the d'Alembert inevitability proof cite these predicates to implement the entanglement gate. The module supplies the supporting definitions and basic lemmas on mixed derivatives and additivity.
claimA combiner $P$ satisfies $F(xy) + F(x/y) = P(F(x), F(y))$. $P$ is separable if $P(u,v) = α(u) + β(v)$ for functions $α, β$. $P$ is entangling if the mixed second difference of $P$ is nonzero.
background
In the Recognition Science setting the d'Alembert equation is the target structure for the log-lift of the J-cost function. The upstream Counterexamples module shows that mere existence of some combiner P does not force this structure. NecessityGates supplies the interaction gate: F has interaction precisely when the equation fails for the trivial additive combiner. This module introduces the complementary entanglement gate on P itself.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the Entanglement Gate used by TriangulatedProof to combine four gates into the unified inevitability theorem and by AnalyticBridge to lift the condition to the log-lift H(t). It therefore closes one of the four gates required to derive the full RCL from the structural axioms.
scope and limits
- Does not prove existence of an entangling combiner under the axioms.
- Does not derive the d'Alembert equation from separability alone.
- Does not address C² smoothness or calibration conditions.
- Does not connect to the phi-ladder or spatial dimension D=3.
used by (2)
depends on (3)
declarations in this module (17)
-
def
IsSeparable -
def
IsEntangling -
def
crossDeriv -
def
Padd -
theorem
Padd_separable -
theorem
Padd_mixed_diff_zero -
theorem
Padd_not_entangling -
def
Prcl -
theorem
Prcl_mixed_diff -
theorem
Prcl_entangling -
theorem
Prcl_not_separable -
theorem
separable_implies_zero_mixed_diff -
theorem
separable_implies_not_entangling -
theorem
separable_with_boundary_is_additive -
theorem
no_interaction_implies_additive -
theorem
interaction_implies_entangling -
theorem
entanglement_gate_theorem