canonicalAmplitudeLinearForcedWitness
plain-language theorem explainer
Packages the many-body amplitude-linearity proposition as the canonical D3 witness structure for the unconditional RS quantum-gravity master theorem. Gravity auditors and master-assembly proofs cite it as the zero-argument D3 input. It is a structure instance that wires the already-proved many-body prop and its holds lemma into the AmplitudeLinearForcedUnconditional interface.
Claim. The canonical D3 witness is an inhabitant of the unconditional amplitude-linearity interface whose sole content field is the many-body amplitude-linearity proposition, with the corresponding holds certificate attached.
background
The module MasterTheoremUnconditional closes the older conditional master theorem by supplying five theorem-built witnesses as zero-argument inputs. D3 is the amplitude-linearity slot: the claim that recognition amplitudes remain linear under many-body composition, forced rather than postulated.
The interface AmplitudeLinearForcedUnconditional is a structure with a proposition field (the linearity statement) and a holds certificate. Upstream, the many-body proposition and its proof already exist as sibling declarations; this definition only names them as the canonical D3 package.
RS time is measured in ticks ($\tau_0 = 1$). Related foundation material (identity event at the $J$-cost minimum, entropy as total defect, eight-tick Clifford grading) sits in the dependency cone but is not re-proved here.
proof idea
One-line structure instance. The amplitude-linearity field is set equal to the sibling many-body proposition canonicalAmplitudeLinearManyBodyProp; the holds field is filled by the sibling certificate canonicalAmplitudeLinearManyBodyProp_holds. No new tactics or algebraic work occur at this site.
why it matters
D3 is one of the five formerly external master inputs. Downstream, rs_quantum_gravity_master_unconditional and endpointRoute_master_theorem_valid both pass this witness into RSQuantumGravityMaster. The non-circularity audit uses it in all_witness_fields_hold and discloses via d3_amplitude_field_is that the field is definitionally the many-body content (two certificate inhabitations plus the many-body endpoint). The master non-circularity certificate then records that this witness holds without assuming any master clause. In the RS forcing chain this sits under the gravity assembly surface rather than T0–T8 themselves; it is the amplitude-linearity leg of the unconditional QG package.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.