toyModel
plain-language theorem explainer
A concrete toy instance of the CPM Model structure is defined over the singleton state space, with all cost constants positive and all functionals constantly equal to one. Auditors of the standalone CPM consistency layer cite this as an explicit witness that the required positivity hypotheses can be satisfied simultaneously. The definition is a direct record construction whose nonnegativity fields are discharged by norm_num.
Claim. Let $U$ be the unit type. The toy model is the structure $M$ of type Model$(U)$ whose constants satisfy $K_{net}=1$, $C_{proj}=2$, $C_{eng}=1$, $C_{disp}=1$, and whose four functionals (defect mass, orthogonal mass, energy gap, test) are each the constant function returning 1 on the unique element of $U$.
background
The Model structure packages a tuple of positive constants together with four real-valued functionals on an arbitrary state space. The upstream LawOfExistence module supplies the cmin_pos lemma: if $0 < K_{net} ∧ 0 < C_{proj} ∧ 0 < C_{eng}$ then $0 < cmin$. Dispersion is imported from the LorentzEmergence module as the sum of axis dispersions over three dimensions. The module itself is the standalone CPM certificate layer that certifies generic consequences for any Model and consistency of the assumptions via a concrete witness.
proof idea
The definition builds the Model record by setting the Constants field to the explicit tuple and discharging the four nonnegativity fields with norm_num. The four functionals are defined as constant maps returning 1. The three predicate fields (projection_defect, energy_control, dispersion) are proved by introducing the unit argument and applying norm_num.
why it matters
This definition supplies the concrete witness used by the CPMMethodCert structure and by the exampleCertificates list in ConstantsAudit. It directly enables the three positivity lemmas toyModel_cmin_pos, toyModel_defect_pos, and toyModel_energy_pos. Within the Recognition framework it closes the consistency check for the CPM layer that sits beneath the forcing chain and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.