cost
plain-language theorem explainer
Definition cost maps each recognition event to the J-cost of its state. Researchers deriving observer structures from coherent recognition or acoustic thresholds from J-cost cite this when reducing event costs to the base J function. It is a direct one-line wrapper around Cost.Jcost applied to the event state.
Claim. Let $e$ be a recognition event with positive real state $s$. The cost of $e$ is $J(s)$, where $J$ is the J-cost function.
background
RecognitionEvent is the structure consisting of a field state : ℝ together with the positivity witness state_pos : 0 < state. The ObserverForcing module uses this cost as the opening step in its seven-step argument that any nontrivial coherent recognition structure forces an observer-like substructure via a persistent zero-cost reference frame. The J-cost function itself is supplied by the upstream Cost module and obeys the Recognition Composition Law together with non-negativity on positive reals.
proof idea
This is a one-line wrapper that extracts the state field of the RecognitionEvent structure and applies the imported Cost.Jcost function.
why it matters
The definition supplies the cost measure appearing in downstream results such as costRateEL_const_one, costRateEL_iff_const_one, and SpeechIntelligibilityCert. It realizes the first clause of the module doc-comment's forcing argument, linking every recognition event to the phi-ladder costs that later force the identity tick (J = 0) as the unique persistent reference. This anchors the transition from RecognitionEvent to the observer in the T5-T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.