module module high

`IndisputableMonolith.Foundation.OntologyPredicates`

OntologyPredicates supplies the operational definition of existence in Recognition Science via the predicate RSExists. A configuration counts as existing precisely when it is positive and carries zero defect under the J-cost functional. Researchers formalizing the emergence of logic or modal structure from cost minimization cite this module. The content consists of definitions together with direct equivalences to the Law of Existence theorem, without additional proof obligations.

claim$RSExists(x) : x > 0$ and $defect(x) = 0$, where $defect(x) = 0$ is the condition that $x$ is stable under the $J$-cost functional from the Law of Existence.

background

The module imports Cost, LawOfExistence, DiscretenessForcing and PhiForcing. LawOfExistence states that $x$ exists if and only if $defect(x) = 0$. DiscretenessForcing supplies the explicit form $J(x) = (x + x^{-1})/2 - 1$, whose unique minimum occurs at $x = 1$, equivalently $J(e^t) = cosh(t) - 1$. PhiForcing shows that self-similarity on a discrete ledger with this cost forces the golden ratio as the scaling factor. RSExists therefore translates the abstract Law of Existence into an operational predicate that requires both positivity and zero defect.

proof idea

This is a definition module. The central predicate RSExists is introduced directly from the two conditions in the module doc-comment. The listed siblings supply immediate equivalences (rs_exists_iff_law_exists, rs_exists_iff_defect_zero) that link the new predicate to the upstream Law of Existence statement; no further lemmas or tactic sequences are required.

why it matters in Recognition Science

The predicates defined here are imported by GodelDissolution (to dissolve self-reference obstructions), InitialCondition (to ground low-entropy initial states), LogicFromCost (to derive consistency from cost minimization) and ModalOntologyStructure (to interpret possibility and necessity). The module therefore supplies the concrete ontology required by the cost-theoretic resolution of Gödel and the Past Hypothesis. It directly implements the selection-by-cost-minimization step stated in the Law of Existence doc-comment.

scope and limits

Does not assign existence to configurations with negative values.
Does not introduce new cost functionals beyond those imported from Cost.
Does not prove existence of any particular physical object.
Does not address continuous versus discrete spectra beyond the imported discreteness results.

used by (4)

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

IndisputableMonolith.Foundation.GodelDissolution module_import
IndisputableMonolith.Foundation.InitialCondition module_import
IndisputableMonolith.Foundation.LogicFromCost module_import
IndisputableMonolith.Philosophy.ModalOntologyStructure module_import

depends on (4)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost module_import
IndisputableMonolith.Foundation.DiscretenessForcing module_import
IndisputableMonolith.Foundation.LawOfExistence module_import
IndisputableMonolith.Foundation.PhiForcing module_import

declarations in this module (46)

def RSExists L61
theorem rs_exists_iff_law_exists L64
theorem rs_exists_iff_defect_zero L73
theorem rs_exists_unique_one L80
theorem rs_exists_one L90
theorem rs_exists_unique L93
theorem nothing_unbounded_defect L104
theorem nothing_not_rs_exists L110
structure CostBridge L123
def Stabilizes L130
def RSExists_cfg L135
def RSTrue L145
def RSDecidable L153
theorem rs_true_neg_imp_neg_rs_true L158
theorem rs_true_neg_iff_neg_rs_true L167
theorem rs_true_and L185
def RSTrue_classical L211
theorem rs_true_classical_iff L213
def RSReal L222
theorem rs_real_one L226
theorem mp_physical L244
theorem mp_forces_existence L252
structure GodelDissolution L274
def godel_dissolution L283
theorem godel_not_obstruction L297
theorem ontology_summary L319
theorem rs_true_or_of_left L334
theorem rs_true_or_of_right L344
theorem rs_true_or_intro L354
theorem rs_true_or_iff L365
structure RecognitionBridge L392
def RSReal_gen L480
def RSReal_synth L484
theorem RSReal_gen_at_one L487
theorem RSReal_gen_iff L490
theorem RSReal_synth_iff L494
def phi_ladder L499
theorem one_mem_phi_ladder L502
theorem RSReal_gen_phi_one L505
theorem Jcost_val_2 L514
theorem Jcost_val_4 L517
theorem Jcost_val_5 L520
theorem Jcost_val_6 L523
theorem Jcost_val_8 L526
theorem Jcost_val_half L530
theorem Jcost_val_three_halves L534