coercive_projection_cert
plain-language theorem explainer
The coercive_projection_cert assembles four positivity results into the CoerciveProjectionCert structure for the ILG energy functional. Researchers modeling galactic dynamics under Information-Limited Gravity cite it to confirm the functional is bounded below with coercivity constant positive and K_net exceeding one. The proof is a direct term-mode record construction that supplies the four fields from the upstream lemmas c_coercive_pos, K_net_gt_one, energy_bounded_below, and C_ilg_prefactor_pos.
Claim. The Coercive Projection Certificate holds: the coercivity constant satisfies $0 < c$, the net constant satisfies $1 < K_{net}$, the weight operator satisfies $w,f : 1 ≤ w → 0 ≤ w f^2$, and the ILG prefactor satisfies $0 < C_{ilg}$.
background
The Coercive Projection module formalizes the ILG energy functional having a unique minimizer under the coercive projection law, with coercivity constant $c = 49/162$ and net constant $K_{net} = (9/7)^2$ arising from the eight-tick octave. The CoerciveProjectionCert structure collects the four positivity conditions required for the projection kernel: coercivity positive, net above one, operator positivity, and prefactor positive. Upstream, energy_bounded_below states that operator positivity implies the energy functional is bounded below, while c_coercive_pos and K_net_gt_one are established by unfolding and norm_num.
proof idea
The proof constructs the CoerciveProjectionCert record in term mode. It assigns coercivity_positive to c_coercive_pos, net_above_one to K_net_gt_one, operator_positive to the lambda term that applies energy_bounded_below to the nonnegativity of $f^2$, and prefactor_positive to C_ilg_prefactor_pos.
why it matters
This certificate closes the positivity requirements for the Coercive Projection Law of Gravity, confirming the ILG functional admits a unique minimizer without per-galaxy retuning. It supports the pressure equivalence result in the module and the projection bound from the CPM paper. The construction directly feeds the eight-tick octave and phi-ladder constants into the gravity model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.