module
module
IndisputableMonolith.Gravity.QuantumChannel.SubstrateSemanticsUnconditional
show as:
view Lean formalization →
used by (1)
depends on (1)
declarations in this module (11)
-
def
universalSubstrateAccessOperator -
def
canonicalAccess -
theorem
universalSubstrateAccessOperator_inducedChannel -
theorem
arisesFromSubstrateAccess_of_isAmplitudeLinear -
theorem
isAmplitudeLinear_iff_arisesFromSubstrateAccess -
theorem
channel_eq_zero_of_isAmplitudeLinear_isDensityOnly_unconditional -
theorem
not_exists_nontrivial_isAmplitudeLinear_isDensityOnly_unconditional -
structure
SubstrateSemanticsUnconditionalCert -
def
substrateSemanticsUnconditionalCert -
theorem
substrateSemanticsUnconditionalCert_inhabited -
theorem
unconditional_substrate_semantics_one_statement