theorem proved term proof

`possible_not_impossible`

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

formal statement (Lean)

 138theorem possible_not_impossible (x : ℝ) : RSPossible x → ¬RSImpossible x := by

proof body

Term-mode proof.

 139  intro hposs himp
 140  exact absurd hposs ((impossible_is_non_positive x).mp himp)
 141
 142/-! ## V. S5 Modal Logic Analog -/
 143
 144/-- **Theorem (S5 Axiom T: Necessity → Actuality)**:
 145    If something is necessary, it is actual.
 146    (The J-minimizer exists = the actual world is real.) -/

depends on (12)

Lean names referenced from this declaration's body.

V in IndisputableMonolith.Cosmology.InflatonPotentialFromJCost decl_use
T in IndisputableMonolith.Foundation.Breath1024 decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
V in IndisputableMonolith.Foundation.SpectralEmergence decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
T in IndisputableMonolith.Gap45.SyncMinimization decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
impossible_is_non_positive in IndisputableMonolith.Philosophy.ModalOntologyStructure decl_use
RSImpossible in IndisputableMonolith.Philosophy.ModalOntologyStructure decl_use
RSPossible in IndisputableMonolith.Philosophy.ModalOntologyStructure decl_use
V in IndisputableMonolith.RRF.Core.Glossary decl_use