def definition def or abbrev

`RSExists`

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

formal statement (Lean)

  37def RSExists (x : ℝ) : Prop := Jcost x = 0

proof body

Definition body.

  38
  39/-- RSExists iff x = 1 (the unique J-cost minimiser). -/

used by (25)

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

CostFirstExistenceCert in IndisputableMonolith.Foundation.CostFirstExistence decl_use
rsExists_iff_one in IndisputableMonolith.Foundation.CostFirstExistence decl_use
discrete_minimum_stable in IndisputableMonolith.Foundation.DiscretenessForcing decl_use
discreteness_forced in IndisputableMonolith.Foundation.DiscretenessForcing decl_use
stable_existence_requires_discrete in IndisputableMonolith.Foundation.DiscretenessForcing decl_use
complete_godel_dissolution in IndisputableMonolith.Foundation.GodelDissolution decl_use
GodelDissolutionTheorem in IndisputableMonolith.Foundation.GodelDissolution decl_use
godel_not_obstruction in IndisputableMonolith.Foundation.OntologyPredicates decl_use
mp_forces_existence in IndisputableMonolith.Foundation.OntologyPredicates decl_use
mp_physical in IndisputableMonolith.Foundation.OntologyPredicates decl_use
nothing_not_rs_exists in IndisputableMonolith.Foundation.OntologyPredicates decl_use
ontology_summary in IndisputableMonolith.Foundation.OntologyPredicates decl_use
RSExists in IndisputableMonolith.Foundation.OntologyPredicates decl_use
RSExists_cfg in IndisputableMonolith.Foundation.OntologyPredicates decl_use
rs_exists_iff_defect_zero in IndisputableMonolith.Foundation.OntologyPredicates decl_use
rs_exists_iff_law_exists in IndisputableMonolith.Foundation.OntologyPredicates decl_use
rs_exists_one in IndisputableMonolith.Foundation.OntologyPredicates decl_use
rs_exists_unique in IndisputableMonolith.Foundation.OntologyPredicates decl_use
rs_exists_unique_one in IndisputableMonolith.Foundation.OntologyPredicates decl_use
RSReal in IndisputableMonolith.Foundation.OntologyPredicates decl_use
RSReal_gen in IndisputableMonolith.Foundation.OntologyPredicates decl_use
RSReal_synth in IndisputableMonolith.Foundation.OntologyPredicates decl_use
rs_true_classical_iff in IndisputableMonolith.Foundation.OntologyPredicates decl_use
ledger_self_grounding in IndisputableMonolith.Information.SimulationHypothesisStructure decl_use
is_implies_ought in IndisputableMonolith.Philosophy.ObjectiveMoralityStructure decl_use

depends on (3)

Lean names referenced from this declaration's body.

cost in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4 decl_use
cost in IndisputableMonolith.Foundation.ObserverForcing decl_use
RSExists in IndisputableMonolith.Foundation.OntologyPredicates decl_use