gate_cost_uniqueness
plain-language theorem explainer
Gate 1 in the inevitability structure records that the cost functional J is uniquely fixed by symmetry, convexity, and normalization. Any zero-parameter framework deriving observables must either match this J or violate the gate. The definition is a direct record that sets the name to T5, marks it proven from the upstream uniqueness theorem, and states the violation condition for alternatives.
Claim. The cost-uniqueness gate is the NecessityGate record with name ``T5: Cost Uniqueness'', proven flag true (from the T5 uniqueness theorem), and violation meaning ``Alternative cost functional $J' ≠ J$ with same symmetry/convexity/normalization''.
background
Recognition Science organizes alternatives into necessity gates that must be violated by any non-RS framework. A NecessityGate is a structure containing a name string, a boolean proven flag, and a string describing the meaning of a violation. This module formalizes the choke points under the cost-as-foundation view, where selection occurs by minimizing a unique cost J. The first gate addresses options about the cost itself: under analyticity plus symmetry plus convexity plus normalization, J is unique and equals (x + x^{-1})/2 - 1. Upstream results supply the cost definitions: the J-cost of a recognition event, the derived cost from a multiplicative recognizer, and the general Cost quantity.
proof idea
The definition is a direct record literal that hard-codes the name, sets proven to true citing the T5 uniqueness result in Cost/T5Uniqueness.lean, and records the violation meaning for an alternative cost functional.
why it matters
This gate is the first entry in all_gates and is checked inside the inevitability theorem, which states that any alternative zero-parameter framework either reduces to RS or violates at least one gate. It corresponds to the T5 J-uniqueness step in the forcing chain and closes the bucket of options about the cost functional itself. The downstream inevitability theorem quotes the gate list to make the no-alternatives claim precise.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.