K_net_gt_one
plain-language theorem explainer
K_net_gt_one establishes that the net constant from the eight-tick structure exceeds one. Gravity formalizations of the coercive projection law cite it to confirm the bound required for the ILG energy minimizer. The proof is a direct term reduction that unfolds the definition and normalizes the inequality.
Claim. $1 < K_{net}$ where $K_{net} = (9/7)^2$ is the net constant from the eight-tick structure.
background
The module formalizes the Coercive Projection Law of Gravity, showing the ILG energy functional has a unique minimizer with coercivity constant 49/162 and that the modified Poisson equation is equivalent to the standard form with effective pressure source. The net constant K_net = (9/7)^2 is defined from the eight-tick structure with epsilon = 1/8, where the squared factor accounts for the full cycle including the return tick.
proof idea
The proof is a one-line term proof that unfolds the definition of the net constant and applies norm_num to confirm the strict inequality in the rationals.
why it matters
It supplies the net_above_one field to the coercive_projection_cert theorem, completing the certification of positive coercivity for the ILG projection. The result implements the K_net > 1 requirement from the CPM paper and connects to the eight-tick octave (T7) in the forcing chain. No open questions remain as the inequality is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.