c_value_eight_tick
plain-language theorem explainer
Computation of the coercivity constant for the eight-tick geometry yields exactly 49/162. Workers in the Coercive Projection Method cite this explicit normalization when fixing the minimal energy scale for eight-tick projections. The argument is a direct substitution into the reciprocal definition of c_min followed by rational arithmetic reduction.
Claim. The coercivity constant defined by $c = 1/(K_{net} C_{proj} C_{eng})$ evaluates to $49/162$ on the eight-tick constants bundle where $K_{net}=(9/7)^2$, $C_{proj}=2$ and $C_{eng}=1$.
background
The module formalizes the Coercive Projection Method in three abstract parts: projection-defect inequality, coercivity factorization via energy gap, and aggregation of local tests. The constant c_min is introduced as the reciprocal $1/(K_{net} C_{proj} C_{eng})$ to bound the energy gap that controls defect size. The eight-tick constants bundle supplies the specific values $K_{net}=(9/7)^2$, $C_{proj}=2$, $C_{eng}=1$ drawn from the eight-tick geometry. Upstream, $C_{proj}=2$ is the projection bound from the CPM paper and $K_{net}=(9/7)^2$ arises from the net factor in the eight-tick structure with one tick out of eight.
proof idea
The proof is a one-line term wrapper. It applies simp to unfold the definition of c_min and the eight-tick constants bundle, then invokes norm_num to reduce the resulting rational expression (81/49 * 2 * 1) to its reciprocal 49/162.
why it matters
This declaration supplies the concrete numerical value of the coercivity constant required by the Law of Existence in the CPM core. It instantiates the eight-tick octave (T7) from the forcing chain and supplies the normalization used in energy-gap bounds. No downstream theorems yet cite it, leaving open its insertion into concrete mass-ladder or Berry-threshold calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.