canonicalAmplitudeLinearManyBodyProp_holds
plain-language theorem explainer
The D3 amplitude-linearity package holds unconditionally: binary physical-channel linearity, its many-body PiTensorProduct lift, and the Track-2 handoff endpoint are all inhabited. Gravity auditors cite it when closing the master theorem without free hypotheses. The proof is a three-field term packing two certificate inhabitance lemmas with the Track-2 endpoint theorem.
Claim. The strengthened D3 proposition is true: there exists a physical-channel amplitude-linearity certificate, there exists a many-body physical-channel amplitude-linearity certificate (finite $N$-body ledger via $\Pi$-tensor product), and the Track-2 many-body handoff endpoint holds.
background
The unconditional master-theorem module supplies zero-argument, theorem-built witnesses for the five inputs that the older conditional quantum-gravity master theorem took as free arguments. D3 is the amplitude-linearity slot: physical quantum channels must act linearly on amplitudes, not merely on probabilities.
The local proposition strengthens plain binary-channel linearity by requiring three conjuncts: a nonempty binary physical-channel amplitude-linearity certificate; a nonempty many-body certificate (sitewise binary closure lifted through a finite $\Pi$-tensor product ledger); and the Track-2 many-body endpoint from the handoff integration lane. Upstream, that endpoint is itself the one-statement T0–T8 many-body physical-channel amplitude-linearity result.
In the Recognition setting this is the operator-level content needed so that the recognition register (finite-dimensional, eight-tick) feeds a linear amplitude map into the gravity master theorem rather than a postulated axiom.
proof idea
Pure term-mode construction of a triple. The first component is the inhabitance theorem for the binary physical-channel amplitude-linearity certificate. The second is the inhabitance theorem for the many-body certificate (the binary closure lifted to any finite many-body channel ledger). The third is the Track-2 many-body endpoint theorem from the handoff integration module, which reduces to the single T0–T8 many-body physical-channel amplitude-linearity statement. No further tactics: the three Nonempty/endpoint facts assemble the conjunction directly.
why it matters
This is the proved content behind the canonical theorem-built D3 witness. Downstream, canonicalAmplitudeLinearForcedWitness packages the proposition together with this hold proof into the unconditional amplitude-linearity record consumed by the master theorem closure surface.
Without it, the master theorem would still need an external amplitude-linearity hypothesis. With it, the D3 slot is discharged by certificates already forced in the quantum-channel lane and the Track-2 handoff, aligning with the finite-dimensional recognition register (eight-tick octave, T7) rather than infinite-dimensional Stone theory. It is one of the five unconditional legs that replace the older conditional master-theorem argument list.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.