subspaceModel
plain-language theorem explainer
A concrete model instance over the unit type with net coupling and projection constants both equal to one supplies a test case for the subspace shortcut lemmas in the CPM abstraction. Researchers validating the projection-defect inequality would cite this construction. The definition proceeds by direct record construction with numerical verification of the nonnegativity axioms.
Claim. Define a model $M$ over the unit type by setting the constants bundle to $K_{net}=1$, $C_{proj}=1$, $C_{eng}=2$, $C_{disp}=1$, with defect mass, ortho mass, energy gap, and tests all equal to the constant function with value 1. The projection-defect relation, energy control, and dispersion conditions hold by direct numerical check.
background
The Model structure consists of a Constants bundle together with four functions from the index type to reals: defectMass, orthoMass, energyGap, and tests. The Constants structure packages four nonnegative reals Knet, Cproj, Ceng, Cdisp. The module supplies sample instantiations of this abstract model to validate the core theorems on defect-ortho inequalities. The upstream lemma defect_le_ortho_of_Knet_one_Cproj_one states that if the CPM constants satisfy K_net = 1 and C_proj = 1, then the projection-defect inequality simplifies to D ≤ orthoMass.
proof idea
The definition constructs the record by assigning the constant values 1, 1, 2, 1 for the four constants and the constant function 1 for each of the four functionals. It discharges the four nonnegativity fields and the three functional conditions via norm_num.
why it matters
This definition supplies the test case for the subspace shortcut lemmas defect_le_ortho_of_Knet_one_Cproj_one and defect_eq_ortho_of_subspace_case. It appears in the CPM examples module whose purpose is to demonstrate usage of the core theorems and validate the infrastructure. It touches the subspace case of the projection-defect relation in the CPM setting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.