ObservableExtractionMechanism
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.
claimAn 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 in Recognition Science
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.
scope and limits
- Does not assert existence of such a mechanism for every type S.
- Does not specify continuity or differentiability of extract.
- Does not identify S with any concrete physical configuration space beyond the ILG action.
- Does not relate extract to the J-function or recognition cost.
- Does not impose any invariance or symmetry conditions on the map.
formal statement (Lean)
87structure ObservableExtractionMechanism (S : Type) where
88 extract : S → ℝ
89 nonconstant : ∃ s₁ s₂ : S, extract s₁ ≠ extract s₂
90