cost_minima_are_recognition
plain-language theorem explainer
Every configuration consisting of a positive real value corresponds to a recognition event whose ratio equals that value. Researchers tracing the cost-to-recognition forcing in Recognition Science would cite this when connecting ledger minima to event structures. The proof is a one-line wrapper applying the config_to_recognition constructor followed by reflexivity on the ratio field.
Claim. For every configuration $c$ consisting of a positive real value $v$, there exists a recognition event $e$ such that the ratio of $e$ equals $v$.
background
In the RecognitionForcing module, Configuration is the structure with a single field value : ℝ together with the positivity hypothesis 0 < value. LedgerForcing.RecognitionEvent is the structure carrying source, target, ratio : ℝ and the positivity witness ratio_pos. The module proves recognition is forced by the cost foundation, using the sibling definition config_to_recognition that builds an event by setting source and target to zero and ratio to the configuration value.
proof idea
The proof is a one-line wrapper that applies config_to_recognition to the input configuration and closes the existential with rfl on the ratio equality.
why it matters
This result feeds directly into the master theorem recognition_forcing_complete, which assembles the full forcing statement that every observable difference yields a nonempty recognition structure. It supplies the concrete link from cost-minimizing configurations to recognition events inside the Recognition Forcing module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.