module module

`IndisputableMonolith.Foundation.DAlembert.EntanglementGate`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Foundation.DAlembert.AnalyticBridge module_import
IndisputableMonolith.Foundation.DAlembert.TriangulatedProof module_import

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost module_import
IndisputableMonolith.Foundation.DAlembert.Counterexamples module_import
IndisputableMonolith.Foundation.DAlembert.NecessityGates module_import

declarations in this module (17)

def IsSeparable L36
def IsEntangling L41
def crossDeriv L45
def Padd L51
theorem Padd_separable L54
theorem Padd_mixed_diff_zero L60
theorem Padd_not_entangling L67
def Prcl L74
theorem Prcl_mixed_diff L78
theorem Prcl_entangling L85
theorem Prcl_not_separable L91
theorem separable_implies_zero_mixed_diff L105
theorem separable_implies_not_entangling L113
theorem separable_with_boundary_is_additive L122
theorem no_interaction_implies_additive L155
theorem interaction_implies_entangling L173
theorem entanglement_gate_theorem L232