structure definition def or abbrev

`ObservableExtractionMechanism`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  87structure ObservableExtractionMechanism (S : Type) where
  88  extract : S → ℝ
  89  nonconstant : ∃ s₁ s₂ : S, extract s₁ ≠ extract s₂
  90

From the project-wide theorem graph. These declarations reference this one in their body.

cost_to_recognition_bridge in IndisputableMonolith.Foundation.RecognitionForcing decl_use
recognition_forcing_complete in IndisputableMonolith.Foundation.RecognitionForcing decl_use
recognition_from_extraction in IndisputableMonolith.Foundation.RecognitionForcing decl_use
recognition_unique in IndisputableMonolith.Foundation.RecognitionForcing decl_use

Lean names referenced from this declaration's body.