eightTickConstants
plain-language theorem explainer
The eightTickConstants definition supplies the concrete CPM constants bundle specialized to eight-tick geometry: Knet set to (9/7)^2, Cproj to 2, Ceng to 1 and Cdisp to 1. Researchers applying the Coercive Projection Method to the fundamental period would cite it when instantiating the abstract framework. The construction is a direct record literal whose nonnegativity fields are discharged by norm_num.
Claim. The eight-tick constants bundle is the structure with $K_{net} = (9/7)^2$, $C_{proj} = 2$, $C_{eng} = 1$, $C_{disp} = 1$ together with the assertions that each component is nonnegative.
background
The Constants structure is an abstract bundle holding four real numbers Knet, Cproj, Ceng, Cdisp together with proofs of their nonnegativity. The module supplies a domain-agnostic formalization of the Coercive Projection Method in three parts: projection-defect inequality, coercivity factorization via energy gap, and aggregation of local tests. The upstream tick definition identifies the fundamental time quantum with the remark that one octave equals eight ticks, fixing the period for which these constants are chosen.
proof idea
The definition is a direct record construction that assigns the four fields and applies norm_num to each of the four nonnegativity goals.
why it matters
This definition supplies the concrete values required by the downstream theorems eight_tick_cmin_consistent and eight_tick_cmin_numerical that establish cmin equals 49/162. It instantiates the eight-tick octave for the Law of Existence and aligns with the T7 forcing-chain landmark of the period-8 evolution step in the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.