c_value_derivation
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 in Recognition Science
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.
scope and limits
- Does not derive the cone constants K_net, C_proj or C_eng from more primitive axioms.
- Does not prove any of the three abstract CPM parts (A/B/C).
- Does not apply the normalized constant to a concrete physical model.
formal statement (Lean)
354theorem c_value_derivation :
355 (1 : ℝ) / ((9/7)^2 * 2 * 1) = 49/162 := by
proof body
Term-mode proof.
356 norm_num
357
358/-- RS cone coercivity constant is 1/2. -/