operator_positivity_pointwise
plain-language theorem explainer
The pointwise positivity theorem for the ILG weight operator states that if w_val >= 1 then f_val squared is at most w_val times f_val squared for any real f_val. Researchers deriving coercivity bounds in the Coercive Projection Law of Gravity would cite this to confirm the energy functional is bounded below in L2. The proof is a one-line term-mode application of nlinarith to the non-negativity of squares.
Claim. If $w >= 1$ then $f^2 <= w f^2$ for all real numbers $w, f$.
background
The module formalizes the Coercive Projection Law of Gravity from two papers: one on the unique energy minimizer from ILG and one on gravity as pressure. The ILG weight operator positivity is listed among core results, ensuring <f, w f> >= ||f||^2 in the L2 sense when w >= 1. This pointwise version is the elementary real-number fact that supports the integrated coercivity claim. Upstream structures such as OptionAEmpiricalProgram.is (collision-free) and SimplicialLedger.EdgeLengthFromPsi.is supply the broader ledger and empirical-program context, though the present theorem uses only basic real arithmetic.
proof idea
The proof is a term-mode one-liner: nlinarith [sq_nonneg f_val]. This tactic directly exploits that f_val squared is nonnegative, so the factor (w_val - 1) >= 0 forces the inequality without further rewriting.
why it matters
The declaration supplies the pointwise foundation for the module's stated claim that the ILG weight operator is positive, which in turn guarantees the energy functional is bounded below. It feeds the coercivity results (c_coercive and related siblings) that establish the unique minimizer with constant 49/162 and the net constant K_net = (9/7)^2 from the eight-tick epsilon. In the Recognition Science setting it aligns with the forcing chain by securing stability of the gravity model without per-galaxy retuning.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.