c_coercive_pos
plain-language theorem explainer
The coercivity constant equals 49/162 and is strictly positive. Researchers on the Coercive Projection Law cite this positivity to confirm the ILG energy functional has a unique minimizer. The proof is a one-line wrapper that unfolds the constant definition and applies numerical normalization to the rational inequality.
Claim. The coercivity constant satisfies $0 < c$ where $c = 49/162$.
background
The module formalizes the Coercive Projection Law of Gravity, including the unique energy minimizer from ILG and pressure equivalence. The coercivity constant is introduced as the key scalar that bounds the energy functional from below. Upstream definition states: 'The coercivity constant from the CPM paper. c = 49/162 arises from the eight-tick net constant and projection bound. This guarantees the ILG energy functional has a unique minimizer.'
proof idea
One-line wrapper that unfolds the definition of the coercivity constant and applies norm_num to verify positivity of the rational 49/162.
why it matters
This theorem supplies the coercivity_positive field inside coercive_projection_cert, which assembles the full certificate for the projection law. It directly supports the claim in the CPM paper that the ILG functional admits a unique minimizer. The constant originates from the eight-tick octave structure (epsilon = 1/8) that produces the net constant K_net = (9/7)^2.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.