canonicalAmplitudeLinearManyBodyProp
plain-language theorem explainer
Packages the D3 amplitude-linearity input to the unconditional gravity master theorem as a single proposition: inhabitability of the binary physical-channel certificate, inhabitability of its many-body lift, and the Track-2 many-body endpoint on the PiTensorProduct ledger. Gravity and quantum-channel auditors cite it as the strengthened D3 field. The body is a three-conjunct Prop abbreviation, not a proof.
Claim. The canonical D3 many-body amplitude-linearity proposition asserts three facts together: (i) there exists a certificate that physical-channel responses on the joint substrate are amplitude-linear by the T0--T8 forcing alone (with density-only collapse and non-vacuous dynamics); (ii) there exists a many-body certificate lifting that binary closure sitewise; (iii) any finite sitewise family of binary physical channel responses induces an amplitude-linear response on the many-body $\Pi$-tensor-product ledger, acts sitewise on pure tensors, and inherits local density-only collapse.
background
This module supplies zero-argument, theorem-built witnesses for the five inputs of the older conditional quantum-gravity master theorem. D3 is the amplitude-linearity slot: physical channel responses forced linear in amplitude by the Recognition forcing chain, not postulated.
Upstream, the binary certificate records unconditional T0--T8 closure of Track 2.C: amplitude-linearity of the physical channel on the joint substrate, density-only responses collapsing to zero, an unconditional no-go, and non-vacuous canonical joint dynamics. The many-body certificate consumes that binary cert at each site and asserts the macroscopic amplitude-linear response. The handoff endpoint (Fork C) states that a finite sitewise family of binary physical responses induces amplitude-linearity on the many-body $\Pi$-tensor-product ledger, acts sitewise on pure tensors, and inherits local density-only collapse.
The doc-comment strengthens D3 beyond the binary certificate alone to include that many-body endpoint.
proof idea
Definitional packaging only. The proposition is the conjunction of three Props: nonemptiness of the binary physical-channel amplitude-linearity certificate, nonemptiness of the many-body lift certificate, and the Track-2 many-body endpoint predicate from the handoff integration layer. No tactics or lemmas run here; discharge lives in the sibling inhabitability theorem that supplies the three witnesses.
why it matters
This is the concrete D3 field content for the unconditional master-theorem closure surface. The canonical D3 witness structure sets its amplitude-linearity clause equal to this proposition and proves it holds via the three inhabitability results. The non-circularity audit discloses that the D3 amplitude field is exactly this many-body package (two certificate inhabitations plus the endpoint), so auditors can see what was installed rather than a bare name.
In the Recognition framework it sits on the quantum-channel side of gravity: T0--T8 force amplitude-linearity of physical responses, then the many-body $\Pi$-tensor-product lift extends that to macroscopic ledgers used by the master theorem. It does not itself touch T5 J-uniqueness, phi, or the eight-tick octave, but it consumes the substrate-semantic closure those steps underwrite for Track 2.C.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.