recognition_is_cost_structure
plain-language theorem explainer
Recognition events carry a J-cost that vanishes exactly when the event ratio equals one and is strictly positive otherwise. Physicists deriving the forcing chain from cost to recognition would cite this result to ground the cost-structure property. The proof combines the zero-cost lemma for unit ratio with the positivity lemma for nontrivial ratios, closing the biconditional via algebraic manipulation of the J expression.
Claim. For every recognition event $e$ with positive ratio $r$, $r=1$ if and only if $J(r)=0$, and $r≠1$ implies $J(r)>0$, where $J(x)=(x+x^{-1})/2-1$.
background
RecognitionEvent is the structure with source, target, and positive real ratio recording a directed recognition between agents. The recognition_cost of such an event is defined as LedgerForcing.J applied to the ratio. The module proves that recognition is forced by the cost foundation, using the fact that J(x)≥0 with equality precisely at x=1.
proof idea
The proof intros e and refines the goal into the biconditional pair and the positivity clause. It applies self_recognition_zero_cost for the forward implication. The converse assumes zero cost, simplifies J(ratio), and uses field_simp together with nlinarith to obtain (ratio-1)^2=0, hence ratio=1. The positivity direction is discharged directly by nontrivial_recognition_positive_cost.
why it matters
This supplies the cost-structure property required by the master theorem recognition_forcing_complete, which asserts that observable distinctions force recognition structures. It corresponds to the T5 J-uniqueness step in the forcing chain, where the cost function enforces self-similarity and the eight-tick octave. It closes the interface between ledger forcing and the recognition composition law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.