module module high

`IndisputableMonolith.Foundation.OntologyPredicates`

Operational predicates for Recognition Science existence: a positive configuration is RS-existent exactly when its J-cost defect vanishes. The module packages uniqueness at the unit configuration, bridges to the Law of Existence, and records that the empty configuration is unbounded in defect. Downstream foundation modules import these predicates when forcing logic, initial conditions, and the T0–T8 chain. Arguments are equivalences and uniqueness facts drawn from the cost landscape.

claimA configuration $x$ is RS-existent when $x > 0$ and $\mathrm{defect}(x) = 0$. Equivalently, RS-existence coincides with the Law of Existence (zero defect). The unique positive zero-defect point is $x = 1$. The empty ("nothing") configuration has unbounded defect and is not RS-existent. Stabilization and cost-bridge predicates package the same zero-defect selection for later logic and forcing modules.

background

Recognition Science treats existence as a selection fact, not a primitive ontology. The cost functional $J(x) = \frac{1}{2}(x + x^{-1}) - 1$ (equivalently $\cosh(\log x) - 1$) has a unique minimum at $x = 1$. Defect measures departure from that minimum; the Law of Existence module states the sharp biconditional that $x$ exists if and only if $\mathrm{defect}(x) = 0$.

This module sits on Cost, LawOfExistence, DiscretenessForcing, and PhiForcing. DiscretenessForcing records that the convex bowl of $J$ in log coordinates forces discrete stable structure. PhiForcing shows the golden ratio is forced once a discrete self-similar ledger carries that $J$-cost. OntologyPredicates turns those facts into named existence and stabilization predicates used as the common vocabulary of later foundation proofs.

The operational reading, from the module doc, is selection by cost minimization: positivity plus vanishing defect, not an assumed substrate.

proof idea

Definition-and-bridge module rather than a single deep proof. Core predicate: RS-existence means positivity and zero defect. Equivalence lemmas identify that predicate with the Law of Existence and with defect-zero alone on the positive ray. Uniqueness lemmas pin the sole RS-existent point at $x = 1$ via the unique minimum of $J$. Separate facts show the empty configuration has unbounded defect, hence fails RS-existence. Cost-bridge and stabilization wrappers rephrase the same zero-defect condition for configuration-level arguments downstream. No long tactic developments; the work is packaging upstream cost and existence theorems under stable names.

why it matters in Recognition Science

Supplies the shared existence vocabulary for the foundation layer. UnifiedForcingChain imports it while claiming all of T0–T8 as inevitabilities from the cost foundation (Recognition Composition Law), including T5 $J$-uniqueness, T6 $\phi$, T7 eight-tick octave, and T8 $D = 3$. LogicFromCost uses the predicates to argue that logical consistency is a cost-minimizing state. BiconditionalSelfNegation applies them to show no real configuration satisfies $(\mathrm{defect},c = 0) \leftrightarrow \neg(\mathrm{defect},c = 0)$, with corollaries about the unique zero-defect existent at $x = 1$. InitialCondition draws on the same zero-defect selection when formalizing why the cosmos begins in a low-entropy state. Without these predicates, later modules would restate defect-zero existence ad hoc.

scope and limits

Does not derive the form of $J$ or the Recognition Composition Law; those are upstream.
Does not prove the full T0–T8 forcing chain; UnifiedForcingChain consumes these predicates.
Does not construct physical units, masses, or coupling constants from existence alone.
Does not claim classical metalanguage logic is derived; LogicFromCost handles that scope.
Does not assert empirical cosmology beyond the formal low-entropy initial-condition link.

used by (4)

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

IndisputableMonolith.Foundation.BiconditionalSelfNegation module_import
IndisputableMonolith.Foundation.InitialCondition module_import
IndisputableMonolith.Foundation.LogicFromCost module_import
IndisputableMonolith.Foundation.UnifiedForcingChain 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 (49)

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 RsAndGodelCategoricalDistinctness L286
def rs_and_godel_categorical_distinctness L297
abbrev GodelDissolution L304
def godel_dissolution L308
theorem rs_closure_vacuous_under_godel_premise L319
theorem godel_not_obstruction L326
theorem ontology_summary L345
theorem rs_true_or_of_left L360
theorem rs_true_or_of_right L370
theorem rs_true_or_intro L380
theorem rs_true_or_iff L391
structure RecognitionBridge L418
def RSReal_gen L506
def RSReal_synth L510
theorem RSReal_gen_at_one L513
theorem RSReal_gen_iff L516
theorem RSReal_synth_iff L520
def phi_ladder L525
theorem one_mem_phi_ladder L528
theorem RSReal_gen_phi_one L531
theorem Jcost_val_2 L540
theorem Jcost_val_4 L543
theorem Jcost_val_5 L546
theorem Jcost_val_6 L549
theorem Jcost_val_8 L552
theorem Jcost_val_half L556
theorem Jcost_val_three_halves L560