module
module
IndisputableMonolith.Gravity.QuantumChannel.NoClassicalMediator
show as:
view Lean formalization →
used by (2)
depends on (1)
declarations in this module (11)
-
abbrev
T0T8ConsistentSubstrate -
theorem
no_classical_mediator_under_T0T8 -
theorem
nontrivial_density_only_impossible_under_T0T8 -
theorem
no_T0T8_substrate_with_nontrivial_classical_mediator -
theorem
channel_forced_amplitude_linear_under_T0T8 -
theorem
T0T8ConsistentSubstrate_inhabited -
theorem
track2D_headline -
structure
NoClassicalMediatorCert -
def
noClassicalMediatorCert -
theorem
noClassicalMediatorCert_inhabited -
theorem
no_classical_mediator_one_statement