trivialModel
plain-language theorem explainer
The trivial model constructs a CPM Model over the unit type with all mass, gap, and test functionals identically zero and the four coercivity constants each equal to 1. Researchers validating the abstract CPM infrastructure cite it as the zero-point sanity check confirming that the core inequalities hold without further hypotheses. The definition is a direct record literal whose nonnegativity and interface obligations are discharged by norm_num.
Claim. Define the trivial CPM model over the singleton type by setting the net kernel, projection, energy, and dispersion constants each to 1, with defect mass, orthogonal mass, energy gap, and test functions all identically zero.
background
The Model structure packages a Constants record (four nonnegative reals K_net, C_proj, C_eng, C_disp) together with four functions from the state type to reals: defect mass, orthogonal mass, energy gap, and tests. The upstream coercivity theorem states defect mass(a) ≤ (K_net · C_proj · C_eng) · energy gap(a); the aggregation theorem states the analogous bound with C_disp and the test functional. The module supplies concrete Model instances to exercise these theorems and the LawOfExistence infrastructure.
proof idea
The definition is a direct record construction. Nonnegativity of the four constants is discharged by norm_num. Each of the three interface conditions (projection defect, energy control, dispersion) is proved by intro followed by norm_num, reducing every inequality to 0 ≤ 0.
why it matters
This definition supplies the baseline case for the CPM framework, allowing immediate verification that both the coercivity link and the aggregation theorem apply to the zero model. It anchors the example suite whose later entries introduce the RS cone and eight-tick models. In the Recognition Science setting it confirms consistency of the inequalities at the zero point before the phi-ladder or dispersion relations are engaged.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.