defect_le_constants_mul_tests
plain-language theorem explainer
The inequality aggregates the projection-defect bound with the dispersion relation to control defect mass by the product of three CPM constants times the test functional. Workers formalizing abstract coercive projection methods cite it when closing the chain from local test data to global defect estimates. The proof chains the two model axioms via multiplication by nonnegative constants followed by algebraic simplification.
Claim. Let $M$ be a model over type $β$ with constants $K_{net}$, $C_{proj}$, $C_{disp}$. For any $a$, the defect mass satisfies $D(a) ≤ (K_{net} · C_{proj} · C_{disp}) · T(a)$, where $T$ denotes the test functional.
background
The module supplies the abstract Coercive Projection Method (CPM) in three layers: projection-defect (A), energy control (B), and aggregation (C). A Model $β$ packages four real-valued functionals on $β$ together with four constants; its projection_defect field asserts defectMass $a$ ≤ $K_{net}$ · $C_{proj}$ · orthoMass $a$. The dispersion field, imported from the LorentzEmergence module, supplies the second link orthoMass $a$ ≤ $C_{disp}$ · tests $a$. Constants $K_{net}$ and $C_{proj}$ originate in the eight-tick structure and projection-kernel bound respectively.
proof idea
One-line wrapper that applies the projection_defect axiom to obtain defectMass $a$ ≤ $K_{net}$ · $C_{proj}$ · orthoMass $a$, then invokes dispersion to bound orthoMass $a$ ≤ $C_{disp}$ · tests $a$. The calc block multiplies the second inequality on the left by the nonnegative product $K_{net}$ · $C_{proj}$ (using mul_le_mul_of_nonneg_left and the nonnegativity lemmas for the constants) and finishes with ring.
why it matters
This is the aggregation step (C) of the CPM core. It is invoked by the trivialModel example, by the subspace-equality lemma defect_eq_ortho_of_subspace_case, and by the standalone CPMMethodCert structure. The result therefore closes the abstract path from projection bounds through dispersion to test-controlled defect estimates, consistent with the Recognition Science forcing chain that fixes $K_{net}$ via the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.