ObservableExtractionMechanism
plain-language theorem explainer
ObservableExtractionMechanism introduces a non-constant real-valued map on a type S drawn from the ILG action, which a physicist cites when constructing recognition relations from observables. It encodes the minimal data needed to force a RecognitionStructure via extraction. The declaration is a bare structure definition with two fields and no proof obligations.
Claim. An observable extraction mechanism on a type $S$ consists of a function $extract : S → ℝ$ together with a witness that it is non-constant: there exist $s_1, s_2 ∈ S$ such that $extract(s_1) ≠ extract(s_2)$.
background
The module proves recognition is forced by the cost foundation. ObservableExtractionMechanism parametrizes a type S, the domain of the ILG action defined upstream as $S[g, ψ; C_lag, α] := S_{EH}[g] + S_ψ[g,ψ]$. Sibling definitions supply Observable, RecognitionStructure, and recognition_from_extraction, which consumes this structure to produce a recognizes relation. The local setting is the cost-to-recognition bridge in the Recognition Forcing chain.
proof idea
This is a structure definition. It directly declares the fields extract and nonconstant with no lemmas, tactics, or reduction steps.
why it matters
The definition supplies the interface for recognition_from_extraction and recognition_unique, which feed the master theorem recognition_forcing_complete asserting existence of RecognitionStructure S for every such mechanism. It closes the step linking the ILG action S to the Recognition.Recognize relation, supporting the claim that recognition arises at cost minima in the J-cost and phi-ladder framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.