knet_from_cone_projection
plain-language theorem explainer
The theorem establishes that the net constant equals one under intrinsic cone projection within the Coercive Projection Method. Researchers applying CPM to Recognition Science models cite it to eliminate covering-radius overhead when the target is a cone rather than a general set. The proof is a direct reflexivity step on the hardcoded value inside the coneConstants structure.
Claim. In the Coercive Projection Method, the net constant for intrinsic cone projection satisfies $K_{net}=1$.
background
The Law of Existence module supplies the abstract A/B/C skeleton of the Coercive Projection Method: projection-defect inequalities, coercivity factorization via energy gaps, and aggregation of local tests. The coneConstants definition supplies the RS-native values Knet := 1, Cproj := 2, Ceng := 1, Cdisp := 1 together with a norm_num proof of nonnegativity. This keeps the core logic domain-agnostic so that concrete instantiations can plug in later without measure-theoretic scaffolding.
proof idea
The proof is a one-line wrapper that applies reflexivity directly to the Knet field of the coneConstants structure.
why it matters
The result removes covering-loss terms from the CPM argument precisely when the projection target is an intrinsic cone, feeding the generic Law of Existence logic. It aligns with the eight-tick octave and three-dimensional setting by adopting the trivial covering number for that geometry. No downstream uses are recorded, so integration with specific domain models remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.