IndisputableMonolith.Foundation.DAlembert.EntanglementGate
The EntanglementGate module defines separability for a combiner P satisfying F(xy) + F(x/y) = P(F(x), F(y)) and introduces the complementary notion of entangling. It supplies the second of four gates needed to force the d'Alembert equation on the log-lift. Researchers deriving inevitability results for Recognition Science functional equations cite it when closing the necessity argument. The module contains only definitions and elementary lemmas on mixed differences.
claimA combiner $P$ is separable when $P(u,v)=\alpha(u)+\beta(v)$ for some functions $\alpha,\beta$. $P$ is entangling precisely when its mixed second difference is nonzero.
background
The module sits inside the d'Alembert development that attempts to recover the Recognition Composition Law from structural axioms on a function F. Upstream, Counterexamples shows that the mere existence of some combiner P does not force the d'Alembert form on the log-lift H(t)=F(e^t)+1. NecessityGates adds the interaction condition (F(xy)+F(x/y) ≠ 2F(x)+2F(y) somewhere) but still leaves room for non-RCL solutions. EntanglementGate therefore isolates the additional property that P must mix its arguments.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the Entanglement Gate (P entangling ⇔ mixed second difference ≠ 0) that TriangulatedProof combines with the Interaction Gate from NecessityGates. Both downstream modules (AnalyticBridge and TriangulatedProof) import it to reach the Bridge Theorem asserting that structural axioms plus interaction force the d'Alembert equation on the log-lift.
scope and limits
- Does not assert existence of an entangling P for any concrete F.
- Does not reference the J-cost function or the phi ladder.
- Does not prove that separability implies the RCL identity.
- Does not contain the full inevitability theorem.
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