c_coercive
plain-language theorem explainer
The definition supplies the coercivity constant c = 49/162 drawn from the Coercive Projection Model paper. Researchers analyzing energy minimization in information-limited gravity models cite this value when establishing uniqueness of minimizers for the ILG functional. The constant is introduced directly as a rational number originating from the eight-tick net structure and projection bounds.
Claim. The coercivity constant is defined by the equality $c = 49/162$. This constant is used to guarantee that the information-limited gravity energy functional admits a unique minimizer.
background
The module formalizes the Coercive Projection Law of Gravity together with pressure equivalence results. Core objects include the ILG energy functional, the net constant K_net arising from epsilon = 1/8 in the eight-tick octave, and the weight operator that satisfies w >= 1 implies positivity of the quadratic form. The declaration comment states that c = 49/162 arises from the eight-tick net constant and projection bound, ensuring the functional has a unique minimizer.
proof idea
The declaration is a direct definition that assigns the rational value 49/162. No lemmas are invoked; downstream results such as c_coercive_pos and c_coercive_value simply unfold the definition and apply norm_num.
why it matters
The constant populates the CoerciveProjectionCert structure and is referenced by c_coercive_pos, c_coercive_value, and c_coercive_approx. It supplies the numerical ingredient required by the CPM paper for uniqueness of the ILG minimizer and connects to the eight-tick octave (T7) in the forcing chain. No open scaffolding is closed here; the value is taken as given from the source paper.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.