trivialModel
plain-language theorem explainer
The trivialModel definition supplies a CPM Model over the unit type in which defect mass, orthogonal mass, energy gap and test functionals are identically zero while the four coercivity constants equal one. Workers validating the abstract CPM infrastructure cite it as the zero-case sanity check confirming that the core inequalities hold vacuously. The definition is a direct record construction whose non-negativity and inequality fields are settled by norm_num.
Claim. Define the model over the singleton type by setting the constants record to all entries equal to 1, the defect-mass and orthogonal-mass maps to the zero function, the energy-gap and test maps to the zero function, and verifying non-negativity of the constants together with the projection, energy-control and dispersion inequalities by direct computation.
background
The Model structure from LawOfExistence packages a Constants record with four real-valued maps on the state type: defectMass, orthoMass, energyGap and tests. Upstream theorems defect_le_constants_mul_energyGap and defect_le_constants_mul_tests establish the two inequalities any such Model must obey: defect mass is bounded by the product of K_net, C_proj and C_eng times the energy gap, and likewise for the dispersion bound. The module supplies concrete instances that exercise these theorems, beginning with the zero case.
proof idea
The definition directly assembles the Model record by assigning the constant 1 to each field of C, the zero function to each of the four maps, and discharging the seven proof obligations (four non-negativity statements and three inequalities) with the norm_num tactic.
why it matters
This definition opens the CPM.Examples module and supplies the baseline instance against which the coercivity and aggregation theorems are checked. It precedes the subspace and RS-cone models, confirming that the abstract CPM framework remains consistent when all physical quantities vanish before non-trivial applications are introduced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.