config_to_recognition
plain-language theorem explainer
The definition maps a Configuration (a positive real value) to a LedgerForcing.RecognitionEvent by setting the ratio to that value and fixing source and target indices at zero. Researchers tracing cost minima to recognition events cite it as the explicit witness constructor. It is a direct record literal that inherits the positivity proof from the input configuration.
Claim. For a configuration $c$ with value $v>0$, the recognition event has source index 0, target index 0, ratio $v$, and positivity witness $0<v$.
background
The RecognitionForcing module establishes that recognition structures are forced by the underlying cost foundation. Configuration is the local structure holding a single positive real value together with its positivity proof. LedgerForcing.RecognitionEvent is the structure that records an event via source and target indices, a positive ratio, and the corresponding positivity witness. This local Configuration specializes the multi-entry version from InitialCondition, whose total defect sums individual J-costs, while the RecognitionEvent type appears in parallel definitions in ObserverForcing and InformationIsLedger that treat physical facts as positive ledger ratios.
proof idea
The definition is a one-line record constructor. It sets source and target to zero, copies the ratio directly from the configuration value, and supplies the positivity proof from the configuration field.
why it matters
This definition supplies the concrete witness used by the downstream theorem cost_minima_are_recognition, which asserts that every configuration yields a recognition event whose ratio equals the configuration value. It thereby supports the module claim that recognition is forced by cost minima and sits inside the Recognition Science forcing chain that extracts recognition structures from the J-cost foundation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.