nontrivial_recognition_positive_cost
plain-language theorem explainer
Nontrivial recognition events with ratio different from 1 carry strictly positive J-cost. Researchers establishing cost structures in Recognition Science cite this to separate trivial self-recognition from all other cases. The proof reduces the claim to the elementary inequality x + x^{-1} > 2 for x > 0, x ≠ 1, via squaring and linear arithmetic.
Claim. Let $e$ be a recognition event with positive ratio $r$ satisfying $r ≠ 1$. Then the associated J-cost satisfies $J(r) > 0$, where $J(r) = (r + r^{-1})/2 - 1$.
background
Recognition events are structures carrying a positive real ratio between source and target. The recognition cost of such an event is defined as the J-function applied directly to this ratio. The module proves that recognition structures are forced from the underlying cost foundation, relying on the non-negativity of J established in ObserverForcing and LedgerForcing.
proof idea
The proof rewrites the cost as LedgerForcing.J applied to the ratio. It shows (ratio - 1)^2 > 0 by sq_nonneg together with a contradiction to the ratio ≠ 1 hypothesis. nlinarith then yields ratio^2 + 1 > 2·ratio; field_simp and lt_div_iff convert this to ratio + ratio^{-1} > 2. linarith finishes the argument that J(ratio) > 0.
why it matters
The result is invoked inside recognition_is_cost_structure to obtain the strict positivity half of the cost characterization. It is also applied in primeEulerEvent_cost_pos to guarantee positive cost for prime Euler events. Within the framework it supplies the non-triviality step that links positive cost to genuine recognition, consistent with J-uniqueness in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.