J_nonneg
plain-language theorem explainer
J establishes non-negativity of the recognition cost for positive ratios. Researchers modeling observer forcing or multiplicative recognizers cite this bound when deriving energy minima. The tactic proof rewrites J(x) algebraically to a squared term over a positive denominator and invokes non-negativity of squares and division.
Claim. For every real number $x > 0$, the function $J(x) := (1/2)(x + x^{-1}) - 1$ satisfies $J(x) >= 0$.
background
The function J is defined by J(x) = (1/2)(x + 1/x) - 1. It is the unique cost satisfying d'Alembert's equation plus normalization and calibration from T5 in the forcing chain. The Modal.Possibility module places this lemma in the setting of recognition events whose costs derive from J via the cost definition in ObserverForcing.
proof idea
The proof unfolds the definition of J. It rewrites the expression to (x-1)^2 / (2x) by field_simp followed by ring. It then applies div_nonneg, citing sq_nonneg on the numerator and a linarith fact establishing positivity of the denominator.
why it matters
This lemma secures the non-negativity property required for J-costs in recognition events, supporting the non-negativity claim attached to ObserverForcing.cost. It instantiates the T5 J-uniqueness result from the foundation, ensuring costs remain non-negative along the phi-ladder. No downstream uses appear yet, but the result closes a basic positivity fact needed for modal statements.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.