module module

`IndisputableMonolith.Gravity.QuantumChannel.PhysicalChannelAmplitudeLinear`

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 (1)

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

IndisputableMonolith.Gravity.MasterTheoremHandoffIntegration module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.QuantumChannel.AmplitudeLinearForcedSubstrate module_import
IndisputableMonolith.Gravity.QuantumChannel.SubstrateSemanticsUnconditional module_import

declarations in this module (27)

abbrev PhysicalChannelResponseOf L113
abbrev canonicalT0T8JointDynamics L123
theorem physicalChannelResponse_isAmplitudeLinear L149
def physicalChannelLinearExtension L163
theorem physicalChannelLinearExtension_eq_inducedChannel L169
theorem density_only_physicalChannelResponse_eq_zero L183
theorem not_exists_nontrivial_density_only_physicalChannelResponse L197
theorem canonicalT0T8JointDynamics_physicalChannelResponse_recognitionUpdate L216
theorem canonicalT0T8JointDynamics_recognitionUpdate_isAmplitudeLinear L220
theorem canonicalT0T8JointDynamics_recognitionUpdate_not_density_only L231
structure PhysicalChannelAmplitudeLinearCert L250
def physicalChannelAmplitudeLinearCert L282
theorem physicalChannelAmplitudeLinearCert_inhabited L294
theorem T0T8_unconditional_physical_channel_amplitude_linear_one_statement L325
abbrev ManyBodyChannelLedger L350
def IsManyBodyAmplitudeLinear L355
def binaryPhysicalChannelLinearWitness L362
theorem binaryPhysicalChannelLinearWitness_apply L369
def manyBodyPhysicalChannelLinearMap L379
def manyBodyPhysicalChannelResponse L390
theorem manyBodyPhysicalChannelResponse_isAmplitudeLinear L401
theorem manyBodyPhysicalChannelResponse_tprod L413
theorem manyBody_local_density_only_collapse L432
structure ManyBodyPhysicalChannelAmplitudeLinearCert L443
def manyBodyPhysicalChannelAmplitudeLinearCert L475
theorem manyBodyPhysicalChannelAmplitudeLinearCert_inhabited L488
theorem T0T8_many_body_physical_channel_amplitude_linear_one_statement L497