c_value_cone
plain-language theorem explainer
The theorem fixes the coercivity minimum for the Recognition Science cone projection constants at exactly one half. Workers instantiating the abstract Coercive Projection Method would cite this normalization when setting up the B-part coercivity factorization. The proof is a direct term-mode simplification that substitutes the three explicit constant lemmas and reduces the arithmetic.
Claim. For the cone constants with $K_{net}=1$, $C_{proj}=2$, $C_{eng}=1$, the minimum coercivity satisfies $c_{min} = (K_{net} C_{proj} C_{eng})^{-1} = 1/2$.
background
The module supplies an abstract, domain-agnostic formalization of the Coercive Projection Method in three parts: A (projection-defect inequality), B (coercivity factorization controlled by the energy gap), and C (aggregation from local tests). The definition cmin(C) := (C.Knet * C.Cproj * C.Ceng)^{-1} supplies the coercivity lower bound once the three constants are fixed. coneConstants is the RS-native record that hard-wires Knet := 1, Cproj := 2, Ceng := 1 (with the three equality lemmas cone_Knet_eq_one, cone_Cproj_eq_two, cone_Ceng_eq_one).
proof idea
One-line term proof that applies simp only on the cmin definition together with the three cone-constant equality lemmas, then finishes with norm_num.
why it matters
The result supplies the concrete numerical anchor required by the coercivity factorization step (part B) inside the Law of Existence module. It is consistent with the Recognition Science forcing chain that produces the phi-ladder and the eight-tick octave, though the module itself remains deliberately abstract so that domain-specific instantiations can plug in later. No downstream theorems are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.