def definition def or abbrev

`Possible`

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

formal statement (Lean)

 323def Possible (p : ConfigProp) (c : Config) : Prop :=

proof body

Definition body.

 324  ∃ y ∈ Possibility c, p y
 325
 326/-- Modal notation -/
 327notation:50 "□" p => Necessary p
 328notation:50 "◇" p => Possible p
 329
 330/-- Duality: □p ⟺ ¬◇¬p -/

used by (13)

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

cosmological_constant_problem in IndisputableMonolith.Cosmology.CosmologicalConstant decl_use
flat_minimizes_cost in IndisputableMonolith.Cosmology.FlatnessProblem decl_use
jcost_equilibrium_profile in IndisputableMonolith.Cosmology.GalaxyRotation decl_use
abundanceVsEta in IndisputableMonolith.Cosmology.Nucleosynthesis decl_use
observedSpectrum in IndisputableMonolith.Cosmology.PrimordialSpectrum decl_use
tensor_to_scalar in IndisputableMonolith.Cosmology.PrimordialSpectrum decl_use
attenuation_prevents_upgoing in IndisputableMonolith.Experimental.ANITAUpgoing decl_use
phi_to_e in IndisputableMonolith.Mathematics.Euler decl_use
possibility_status in IndisputableMonolith.Modal.Possibility decl_use
actual_has_zero_modal_distance in IndisputableMonolith.Philosophy.ModalOntologyStructure decl_use
s5_actuality_implies_possibility in IndisputableMonolith.Philosophy.ModalOntologyStructure decl_use
predictions in IndisputableMonolith.Quantum.PlanckScale decl_use
eight_tick_criticality in IndisputableMonolith.Thermodynamics.CriticalExponents decl_use

depends on (5)

Lean names referenced from this declaration's body.

Config in IndisputableMonolith.Gravity.ILG decl_use
Config in IndisputableMonolith.Modal.Possibility decl_use
ConfigProp in IndisputableMonolith.Modal.Possibility decl_use
Necessary in IndisputableMonolith.Modal.Possibility decl_use
Possibility in IndisputableMonolith.Modal.Possibility decl_use