global_minimum_is_self_recognition
plain-language theorem explainer
The theorem asserts existence of a recognition event whose ratio equals one and whose J-cost vanishes, establishing the global minimum of the recognition cost function. Researchers closing the cost-to-recognition bridge in the forcing chain would cite it when assembling the master theorem on recognition forcing. The proof is a direct term construction that builds a self-referential event and reduces the cost expression by simplification and normalization.
Claim. There exists a recognition event $e$ such that the ratio of $e$ equals 1 and the J-cost of $e$ equals 0.
background
The Recognition Forcing module proves that recognition structures are forced by the underlying cost foundation. A RecognitionEvent is a structure carrying source and target indices together with a positive real ratio; the recognition_cost of the event is defined to be the J-function applied to that ratio. The J-function satisfies the Recognition Composition Law and attains its global minimum of zero precisely when the argument is unity.
proof idea
The proof is a term-mode construction. It instantiates a RecognitionEvent with source and target both zero and ratio one (using the positivity witness one_pos), then applies simp on the recognition_cost definition and the LedgerForcing.J unfolding, followed by norm_num to confirm the cost evaluates to zero.
why it matters
This supplies the existence clause inside the cost_to_recognition_bridge master theorem that completes recognition forcing. It realizes the zero-cost self-recognition point required by the J-uniqueness step (T5) of the forcing chain and feeds directly into the assembly of recognition structures from ledger costs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.