self_recognition_zero_cost
plain-language theorem explainer
Recognition events with ratio exactly 1 incur zero J-cost. Researchers deriving recognition structures from cost foundations cite this to close the fixed-point case. The term proof introduces the ratio hypothesis, unfolds recognition_cost via simp, and normalizes J(1) to zero.
Claim. For any recognition event $e$ with ratio $e.ratio = 1$, the J-cost satisfies $J(e.ratio) = 0$.
background
The Recognition Forcing module shows recognition structures emerge from cost minimization. A LedgerForcing.RecognitionEvent consists of source, target, and positive real ratio. recognition_cost is defined as LedgerForcing.J applied to the ratio, where J(x) = (x + x^{-1})/2 - 1. Upstream results establish J(1) = 0 and non-negativity of costs for recognition events.
proof idea
Term-mode one-liner. The intro tactic binds the ratio-equals-1 hypothesis. simp unfolds recognition_cost, substitutes the hypothesis into LedgerForcing.J, and norm_num reduces the arithmetic expression J(1) to zero.
why it matters
Supplies the zero-cost direction in the downstream theorem recognition_is_cost_structure, which states the full biconditional for cost structure. It realizes the J-uniqueness fixed point (T5) where ratio 1 yields the identity recognition with no cost, anchoring the forcing chain from cost to recognition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.