IndisputableMonolith.Gravity.QuantumChannel.SubstrateLocalAccess

declarations in this module (16)

• structure SubstrateAccessData L85
• def inducedChannel L96
• theorem inducedChannel_apply L102
• def inducedChannel_isSectionReadout L114
• def ArisesFromSubstrateAccess L136
• theorem sectionReadout_of_arisesFromSubstrateAccess L146
• theorem isAmplitudeLinear_channel_of_arisesFromSubstrateAccess L166
• theorem channel_eq_zero_of_density_only_of_arisesFromSubstrateAccess L177
• theorem not_exists_nontrivial_density_only_channel_with_substrateAccess L188
• theorem arisesFromSubstrateAccess_of_pureTensorFactorization L205
• def recognitionProbeAccess L227
• theorem canonicalCyclicJointOperator_arisesFromRecognitionProbe L240
• structure SubstrateLocalAccessCert L256
• def substrateLocalAccessCert L291
• theorem substrateLocalAccessCert_inhabited L308
• theorem substrate_local_access_one_statement L328