eight_tick_cmin_numerical
plain-language theorem explainer
The theorem states that the coercivity minimum computed from the eight-tick constants bundle equals the rational 49/162. CPM audit code and consistency checks cite this identity to confirm arithmetic agreement with the Recognition Science eight-tick geometry. The proof is a one-line wrapper that unfolds the cmin definition and the eight-tick bundle then reduces the resulting rational expression by norm_num.
Claim. Let $c_ {min}(C) = 1/(K_{net}(C) · C_{proj}(C) · C_{eng}(C))$. For the eight-tick constants bundle with $K_{net} = (9/7)^2$, $C_{proj} = 2$, $C_{eng} = 1$, one has $c_{min} = 49/162$.
background
The CPM module verifies machine-checkable constants derived from Recognition Science invariants. The function cmin is defined as the reciprocal of the product of three positive constants Knet, Cproj and Ceng; it appears in the LawOfExistence file as a noncomputable definition kept separate to avoid duplication. The eightTickConstants bundle supplies the concrete values Knet = (9/7)^2, Cproj = 2, Ceng = 1 together with non-negativity proofs, all tied to the eight-tick octave geometry (T7). Upstream results include the inductive Structure type from CrystalStructure and probability definitions from QuantumLedger and SMatrixUnitarity, which supply the broader context for constant usage in CPM.
proof idea
The proof is a term-mode one-line wrapper. It applies simp only on the identifiers cmin and eightTickConstants to unfold the definition and the bundle record, then invokes norm_num to evaluate the resulting rational arithmetic (1/((81/49)·2)) to the reduced fraction 49/162.
why it matters
This numerical identity closes one verification step inside the CPM constants audit and is invoked by printConsistency and generateJSONReport to populate audit output. It directly supports the eight-tick octave (T7) and the D = 3 spatial dimensions that follow from the forcing chain (T0-T8). The result feeds the larger claim that CPM constants are consistent with Recognition Science invariants rather than coincidental; no open scaffolding remains for this particular arithmetic check.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.