def definition def or abbrev

`RSActual`

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

formal statement (Lean)

  61def RSActual (x : ℝ) : Prop := RSNecessary x

Definition body.

  62
  63/-- **RSImpossible**: x is impossible iff x ≤ 0 (violates ledger positivity). -/

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

actuality_is_j_minimum in IndisputableMonolith.Philosophy.ModalOntologyStructure decl_use
actuality_is_unique in IndisputableMonolith.Philosophy.ModalOntologyStructure decl_use
modal_distance_zero_iff_actual in IndisputableMonolith.Philosophy.ModalOntologyStructure decl_use
ph013_modal_certificate in IndisputableMonolith.Philosophy.ModalOntologyStructure decl_use
RSPossible in IndisputableMonolith.Philosophy.ModalOntologyStructure decl_use
s5_actuality_implies_possibility in IndisputableMonolith.Philosophy.ModalOntologyStructure decl_use
s5_necessity_implies_actuality in IndisputableMonolith.Philosophy.ModalOntologyStructure decl_use

Lean names referenced from this declaration's body.

is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
RSImpossible in IndisputableMonolith.Philosophy.ModalOntologyStructure decl_use
RSNecessary in IndisputableMonolith.Philosophy.ModalOntologyStructure decl_use