c_coercive_value
plain-language theorem explainer
The declaration fixes the coercivity constant at exactly 49/162. Modelers of information-limited gravity who need a concrete bound for unique energy minimizers cite this fraction directly. The proof is a one-line reflexivity step that matches the upstream definition without further computation.
Claim. The coercivity constant satisfies $c = 49/162$.
background
The Coercive Projection Law module formalizes the ILG energy functional having a unique minimizer once a coercivity bound holds. The constant arises from the eight-tick net constant together with a projection bound, as described in the module documentation. The 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
The proof is a one-line wrapper that applies reflexivity to the definition of c_coercive.
why it matters
This value supplies the concrete coercivity bound required for uniqueness of the ILG energy minimizer. It sits inside the Coercive Projection Law and connects to the eight-tick octave of the Recognition Science framework, where the net constant K_net = (9/7)^2 follows from epsilon = 1/8. The result supports the module claim that no per-galaxy retuning is consistent with energy minimization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.