module module high

`IndisputableMonolith.Foundation.OntologyPredicates`

The module defines the operational notion of existence in Recognition Science as positive configurations that minimize J-cost to zero defect. Researchers in foundational physics and modal ontology cite it when deriving being from cost selection. It assembles this predicate by importing and combining results from discreteness forcing and the law of existence.

claimA configuration $x$ exists in the Recognition Science sense if and only if $x > 0$ and the defect of $x$ under the J-cost function is zero.

background

Recognition Science starts from the J-cost $J(x) = ½(x + x^{-1}) - 1$, whose unique minimum at $x=1$ forces discrete structure as detailed in the DiscretenessForcing module. The LawOfExistence module establishes that existence corresponds exactly to vanishing defect. PhiForcing adds self-similarity constraints that select the golden ratio. This module collects these elements into predicates for existence and stability.

proof idea

This module is primarily definitional. It imports the Cost, LawOfExistence, DiscretenessForcing, and PhiForcing modules to introduce the existence predicate and auxiliary notions such as stabilization and truth predicates. The argument structure relies on the upstream forcing chains without adding new derivations.

why it matters in Recognition Science

It supplies the existence predicate that downstream modules use to resolve Gödel self-reference in GodelDissolution and to derive logical consistency from cost in LogicFromCost. It also underpins the initial condition analysis and modal ontology questions. This realizes the selection mechanism from the T5 J-uniqueness and T6 phi fixed point in the unified forcing chain.

scope and limits

Does not identify specific zero-defect configurations beyond the general predicate.
Does not prove the uniqueness or existence of such configurations.
Does not extend to continuous or quantum regimes.
Does not compute numerical values for constants like alpha or G.

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