eight_tick_cmin_consistent
plain-language theorem explainer
The theorem confirms that c_min for the eight-tick constants bundle equals the reciprocal of the product of its K_net, C_proj and C_eng components. Auditors running consistency checks in the CPM module cite this result to validate the eight-tick parameter set. The proof is immediate by reflexivity because the cmin definition is literally that reciprocal expression.
Claim. Let $C$ be the eight-tick constants bundle. Then the coercivity constant satisfies $c_min(C) = (K_net(C) · C_proj(C) · C_eng(C))^{-1}$.
background
The CPM Constants Audit module supplies machine-checkable verification that constants satisfy required properties derived from Recognition Science invariants, including consistency checks between constant sets. The cmin definition returns the reciprocal of the product of the three fields Knet, Cproj and Ceng; it is kept as a top-level definition rather than a field to avoid duplication. The eightTickConstants construction supplies the specific bundle for eight-tick geometry with the listed numerical values for those fields.
proof idea
One-line wrapper that applies reflexivity. The equality holds definitionally once the cmin definition is unfolded against the eightTickConstants record.
why it matters
The result feeds the consistency section of the audit report and the printConsistency routine. It closes the definitional check for the eight-tick constants that appear in the T7 eight-tick octave step of the forcing chain. No open scaffolding remains for this particular equality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.