d3_amplitude_field_is
plain-language theorem explainer
The D3 amplitude field of the unconditional quantum-gravity master witness is definitionally the many-body amplitude-linearity proposition: two certificate inhabitations plus the many-body endpoint. Non-circularity auditors cite this to confirm the slot is neither True nor the master conclusion. The proof is pure reflexivity against the canonical witness construction.
Claim. By definition, the amplitude-linearity component of the canonical forced amplitude-linearity witness equals the many-body amplitude-linearity proposition (two certificate inhabitations conjoined with the many-body endpoint).
background
The module audits the unconditional quantum-gravity master theorem field by field. A referee objection is that witness structures of shape $\Sigma(P:\mathrm{Prop}), P$ can be inhabited by $\langle \mathrm{True}, \mathrm{trivial}\rangle$, so the master statement is only as strong as the concrete propositions in its slots. For each atom the audit supplies an rfl-level disclosure of what proposition the field actually is, plus a standalone proof that it holds without assuming any master clause.
The D3 slot is the amplitude-linearity witness. Upstream, the canonical forced witness is built by setting its amplitude-linearity field to the many-body amplitude-linearity proposition and discharging the holds proof with the corresponding many-body theorem. Related RS landmarks include the fundamental tick $\tau_0=1$ and the eight-tick octave, which frame discrete evolution capacity, but this disclosure only identifies the proposition, not the tick calculus itself.
proof idea
One-line term proof by reflexivity. The canonical forced amplitude-linearity witness is defined with its amplitude-linearity field equal to the many-body amplitude-linearity proposition, so the equality is definitional and rfl closes it. No lemmas are unfolded beyond that construction.
why it matters
This disclosure is one atom of the non-circularity audit answering peer-review finding F1 / Rec 2: every master-conjunction field must be shown to be genuine named physics content, not a True placeholder and not secretly the master conclusion. After the M1–M3 strengthenings, T0–T8, cost-uniqueness, and BMV-positivity are carried propositions rather than trivial placeholders; D3 is handled the same way for amplitude linearity. Downstream use is local to the audit (no external dependents listed): together with the sibling field disclosures and the standalone holds proofs, it lets the master conclusion be assembled from independently proved, non-self-referential atoms. It does not itself advance the forcing chain T0–T8 or the Recognition Composition Law; it only certifies what the D3 slot contains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.