knet_eight_tick
plain-language theorem explainer
The result establishes that the covering-derived net constant for radius one-eighth in three dimensions equals four-thirds cubed. Researchers modeling the Coercive Projection Method in Recognition Science cite it to fix the eight-tick normalization. The proof is a one-line wrapper that unfolds the covering definition and evaluates the arithmetic.
Claim. For covering radius $ε = 1/8$ and dimension $d = 3$, the net constant satisfies $K_{net} = (1/(1-2ε))^d = (4/3)^3$.
background
The module supplies the abstract Coercive Projection Method in three parts: projection-defect inequality, coercivity factorization controlled by energy gaps, and aggregation from local tests to membership. The fundamental time quantum is one tick, with one octave defined as eight ticks. The covering net constant is given by the formula $K_{net}(ε,d) = (1/(1-2ε))^d$ whenever $ε < 1/2$.
proof idea
The proof is a one-line wrapper that applies the definition of the covering net constant and then normalizes the resulting arithmetic expression.
why it matters
This pins the eight-tick K_net value inside the CPM aggregation principle of the Law of Existence. It supplies the concrete normalization required by the eight-tick octave and the three spatial dimensions in the forcing chain. An alternative expression (9/7)^2 is recorded separately in the gravity module for refined analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.