`PredictedObservable`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.OptionAFalsifierRegistry
domain: Foundation
line: 77 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.OptionAFalsifierRegistry on GitHub at line 77.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

used by

formal source

  74  decide
  75
  76/-- Observable predicted by the Lean structural theorem plus RS hypothesis. -/
  77inductive PredictedObservable where
  78  | tensorRank125
  79  | strataRatioPhiPower
  80  | multiplicativeTherapyResponse
  81  | fiveBitAddressBound
  82  | fortyStableFiveTransient
  83  | reverseEriksonOrder
  84  | unitResponseCoefficient
  85  | qSpaceSpanSequence
  86  | regulatoryCeiling70
  87  deriving DecidableEq, Repr, Fintype
  88
  89theorem predictedObservable_count : Fintype.card PredictedObservable = 9 := by
  90  decide
  91
  92/-- What empirical pattern would count as a failure of the associated claim. -/
  93inductive FailureMode where
  94  | singleAxisDecoderSuffices
  95  | noSmallPhiPowerRatio
  96  | additiveTherapyResponse
  97  | depthExceedsFiveBits
  98  | nonFortyPlateauSpectrum
  99  | nonReverseDementiaOrder
 100  | nonUnitSharedCoefficient
 101  | nonQSpaceSpanCollapse
 102  | moduleExceedsCeiling70
 103  deriving DecidableEq, Repr, Fintype
 104
 105theorem failureMode_count : Fintype.card FailureMode = 9 := by
 106  decide
 107

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.