C_proj_value
plain-language theorem explainer
The projection bound constant in the coercive projection law of gravity is fixed at exactly 2. Researchers working on information-limited gravity models cite this when bounding the operator norm of the ILG projection kernel in the defect bound Defect(Phi) <= M * K_net * C_proj * sup T_W[Phi]. The equality follows immediately from the definition of C_proj by reflexivity.
Claim. The projection bound constant $C_{proj}$ equals 2.
background
The Coercive Projection Law of Gravity module formalizes results from the papers on the Coercive Projection Law of Gravity and Gravity as Pressure in Information-Limited Gravity. It treats the ILG energy functional as having a unique minimizer, with the net constant K_net = (9/7)^2 arising from the eight-tick epsilon = 1/8. C_proj is the projection bound constant that controls the stability of the energy minimizer in the defect bound. Upstream results include the defect functional from LawOfExistence, defined as defect(x) = J(x) for positive x, and structures for nuclear densities and ledger factorization.
proof idea
The proof is a one-line reflexivity that matches the definition of C_proj directly to the value 2.
why it matters
This declaration fixes the projection constant used in the defect bound for the ILG energy minimizer, as described in the Coercive Projection Law of Gravity paper. It contributes to the stability analysis in the CPM-Gravity framework by setting the operator norm bound on the projection kernel. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.