C_proj
plain-language theorem explainer
C_proj supplies the rational constant 2 that upper-bounds the operator norm of the ILG projection kernel in the Coercive Projection Law of Gravity. Researchers constructing defect estimates for energy minimizers in information-limited models cite this value when scaling projection terms alongside K_net. The definition is a direct constant assignment taken from the Hermitian rank-one bound analysis in the CPM paper.
Claim. The projection bound constant satisfies $C_ {proj} = 2$.
background
The Coercive Projection Law module formalizes results from the papers on the unique energy minimizer of the ILG functional and gravity as pressure. It introduces the projection-defect inequality D ≤ K_net · C_proj · ||proj_{S⊥}||² together with energy control bounds, using the net constant K_net = (9/7)^2 that arises from eight-tick epsilon = 1/8. C_proj specifically caps the operator norm of the ILG projection kernel, with the value 2 taken from the Hermitian rank-one bound J''(1)=1.
proof idea
This is a one-line definition that directly assigns the rational number 2 to C_proj with no lemmas or tactics applied.
why it matters
C_proj enters the Hypothesis structure for CPM instances on GalerkinState N, where it scales the projection defect term in the inequality D ≤ K_net · C_proj · ||proj||². It appears in audit functions that export verified constants and check cone_cmin_consistency = (K_net · C_proj · C_eng)⁻¹. The constant supports the eight-tick octave and coercivity analysis for the ILG modified Poisson equation within the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.