cmin
plain-language theorem explainer
The cmin definition supplies the coercivity constant as the reciprocal of the product of K_net, C_proj and C_eng from an abstract Constants bundle. Analysts working on the Coercive Projection Method cite it to normalize the minimal factor controlling defect size via energy gaps. It is realized as a direct noncomputable definition carrying the simp attribute.
Claim. $c_ {min}(C) := 1/(K_{net}(C) · C_{proj}(C) · C_{eng}(C))$ for a Constants structure $C$ whose components $K_{net}$, $C_{proj}$, $C_{eng}$ are non-negative reals.
background
The LawOfExistence module formalizes the Coercive Projection Method in three abstract parts: projection-defect inequality, coercivity factorization in which the energy gap controls defect, and aggregation from local tests. The sibling Constants structure bundles four non-negative reals Knet, Cproj, Ceng, Cdisp that parameterize these relations. Upstream imports supply only generic lists of narrative families, kinship systems, ore classes and musical modes that lie outside the core CPM logic.
proof idea
The declaration is a one-line algebraic expression that directly inverts the product of the three relevant fields of the input Constants record.
why it matters
cmin supplies the explicit coercivity factor required by downstream results such as cone_cmin_consistent, eight_tick_cmin_numerical and eight_tick_cmin_value. It realizes the B part of the CPM core by providing the normalization for energy-gap control of defects. It appears in examples verifying positivity and the specific value 49/162 for the eight-tick model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.