defect_bound_constant
plain-language theorem explainer
The defect bound constant is the product of the eight-tick net factor K_net and the ILG projection bound C_proj. Researchers formalizing the coercive projection law of gravity cite it when controlling the stability of the energy minimizer in the ILG functional. The definition is a direct multiplication of the two referenced constants with no further reduction.
Claim. Let $K_{net} = (9/7)^2$ be the net constant from the eight-tick structure and $C_{proj} = 2$ the bound on the projection operator norm. The defect bound constant is then $K_{net} · C_{proj}$.
background
The module formalizes the Coercive Projection Law of Gravity, including the unique energy minimizer of the ILG functional and the equivalence of the ILG modified Poisson equation to standard Poisson with effective pressure source. The defect bound states that Defect(Phi) ≤ M · K_net · C_proj · sup T_W[Phi], with the product K_net · C_proj controlling stability of the minimizer. K_net equals (9/7)^2 from the eight-tick structure (epsilon = 1/8, with the factor 9 arising from the full cycle including the return tick). C_proj equals 2 as the operator norm bound on the ILG projection kernel.
proof idea
One-line definition that multiplies the referenced constants K_net and C_proj. No lemmas or tactics are invoked beyond the direct product of the two upstream definitions.
why it matters
This supplies the controlling constant in the defect bound for the ILG energy minimizer and feeds the downstream theorem defect_bound_constant_value, which evaluates the product to 162/49. The construction rests on the eight-tick octave (T7) from the Recognition Science forcing chain and the projection bound from the CPM paper. It supports the pressure-equivalence result that the ILG weight operator is positive and that no per-galaxy retuning is needed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.