cone_cmin_consistent
plain-language theorem explainer
The theorem confirms that c_min for the cone projection constants equals the reciprocal of the product of K_net, C_proj, and C_eng. Auditors checking CPM constant derivations from Recognition Science would cite this to verify internal definitional consistency. The proof is a direct reflexivity reduction that matches the cmin definition to the explicit product formula.
Claim. Let $c_ {min}(C) = (K_{net} · C_{proj} · C_{eng})^{-1}$ for a Constants record $C$. Then $c_{min}$(coneConstants) = (coneConstants.Knet · coneConstants.Cproj · coneConstants.Ceng)^{-1}.
background
The CPM Constants Audit module supplies machine-checkable checks that constants satisfy derivations from Recognition Science invariants. The cmin definition computes the coercivity constant as the reciprocal of the product of the three fields Knet, Cproj, and Ceng on any Constants record. coneConstants supplies the specific CPM values Knet = 1, Cproj = 2, Ceng = 1 for the cone projection model, with the remaining fields set to placeholders.
proof idea
The proof applies the reflexivity tactic. It matches the left-hand side (application of cmin to coneConstants) directly against the right-hand side expression that unfolds the definition of cmin.
why it matters
This result feeds the consistency section printed by AuditMain.printConsistency and the JSON report produced by generateJSONReport. It closes the basic definitional verification for c_min inside the CPM constant audit, confirming alignment with the upstream Law of Existence derivations. No open questions or scaffolding remain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.