cone_cmin_consistent
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove positivity or bounds on c_min.
- Does not cover numerical evaluation or other constant sets.
- Does not address derivations beyond the cone projection case.
formal statement (Lean)
87theorem cone_cmin_consistent :
88 cmin RS.coneConstants = (RS.coneConstants.Knet * RS.coneConstants.Cproj * RS.coneConstants.Ceng)⁻¹ := by
proof body
Decided by rfl or decide.
89 rfl
90