ObservableExtractionMechanism
plain-language theorem explainer
ObservableExtractionMechanism equips any type S with a non-constant map to the reals. It is invoked in the recognition forcing theorems to convert observables into RecognitionStructure instances via equality of extracted values. The declaration is a bare structure definition requiring no lemmas or reduction steps.
Claim. An observable extraction mechanism on a set $S$ consists of a function $extract: S → ℝ$ together with a witness that there exist $s_1, s_2 ∈ S$ such that $extract(s_1) ≠ extract(s_2)$.
background
The RecognitionForcing module establishes that recognition structures are forced by the underlying cost foundation. ObservableExtractionMechanism supplies the interface that turns an observable into a recognition relation by declaring when two elements yield the same real value. The sole upstream dependency is the ILG action $S[g, ψ; C_lag, α] := S_EH[g] + S_ψ[g,ψ]$, whose minima supply the physical events that later become recognition events.
proof idea
Structure definition. The two fields are introduced directly; no lemmas or tactics are applied.
why it matters
The structure is the input type for recognition_from_extraction, which constructs the corresponding RecognitionStructure, and for recognition_unique and the master theorem recognition_forcing_complete. It therefore supplies the concrete bridge from cost-derived observables to recognition in the forcing argument. The construction sits inside the larger claim that recognition is forced by the cost foundation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.