eightTickRecord
plain-language theorem explainer
The eight-tick constants record supplies explicit rational values for the CPM constants structure in the eight-tick setting. Workers on the Coercive Projection Method cite this record to instantiate the abstract projection-defect and coercivity inequalities with concrete covering and projection bounds. The definition assembles the record from the listed rationals and closes with a norm_num check on the derived cmin field.
Claim. The eight-tick constants record is the CPM constants record with $K_{net}=(9/7)^2$, $C_{proj}=2$, $C_{eng}=1$, $C_{disp}=1$, and $c_{min}=49/162$.
background
CPMConstantsRecord is the structure holding the net covering constant Knet, projection constant Cproj, energy control constant Ceng, dispersion constant Cdisp, and coercivity constant cmin together with provenance strings. The companion definition cmin computes the coercivity threshold as the reciprocal of the product Knet · Cproj · Ceng. The module LawOfExistence formalizes the generic Coercive Projection Method in three abstract parts: projection-defect inequality, coercivity factorization via energy gap, and aggregation of local tests.
proof idea
The definition is a direct record constructor that assigns the explicit rational values to each field and invokes norm_num to confirm consistency of the supplied cmin value with the product formula.
why it matters
This record supplies the concrete constants required by the eight-tick octave (T7) inside the CPM instantiation of the Law of Existence. It closes the provenance gap for the abstract A/B/C framework by fixing numerical values that downstream coercivity and defect lemmas can reference. No parent theorems or open questions are recorded in the current dependency graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.