c_value_derivation
plain-language theorem explainer
The derivation establishes that the minimum coercivity constant c_min equals 49/162 by substituting the cone factors K_net = (9/7)^2, C_proj = 2 and C_eng = 1 into the reciprocal expression. Researchers formalizing the Coercive Projection Method in Recognition Science cite this normalized value when fixing the energy-gap scale in coercivity statements. The proof is a one-line numerical simplification that confirms the arithmetic identity without further lemmas.
Claim. $c_ {min} = 1 / (K_{net} · C_{proj} · C_{eng}) = 1 / ((9/7)^2 · 2 · 1) = 49/162$.
background
The module supplies an abstract formalization of the Coercive Projection Method (CPM) in three parts: A (projection-defect inequality), B (coercivity factorization in which the energy gap controls defect size), and C (aggregation principle that local tests imply global membership). This declaration records an optional concrete normalization for the coercivity constant used inside part B. The supplied doc-comment states the explicit substitution c_min = 1 / (K_net · C_proj · C_eng) with the numerical values (81/49) · 2 · 1.
proof idea
The proof is a one-line wrapper that applies norm_num to verify the arithmetic equality directly.
why it matters
The result supplies the explicit numerical value of the RS cone coercivity constant required by the Law of Existence module. It closes the constant-normalization step that downstream CPM statements in coercivity factorization can reference. No parent theorems are listed in the used-by edges, indicating the constant is currently a leaf normalization rather than an active dependency.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.