module module

`IndisputableMonolith.Gravity.QuantumChannel.MediatorUniversalityBoundary`

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

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.QuantumChannel.AmplitudeLinearForced module_import

declarations in this module (17)

def densityOf L50
theorem densityOf_phase_invariant L54
theorem trace_densityOf L78
theorem densityOf_single_ne_zero L83
def conjugationChannel L92
theorem conjugationChannel_reproduces L100
theorem conjugationChannel_trace_preserving L110
theorem per_update_density_mediator_exists L120
def basis0 L130
def basis1 L133
def swap01 L136
def swapMatrix L139
theorem swapMatrix_unitary L142
theorem swapMatrix_mulVec_basis0 L146
theorem densityOf_basis0_ne_densityOf_basis1 L158
theorem no_universal_density_mediator L165
theorem mediator_universality_boundary L189