actuality_is_j_minimum
plain-language theorem explainer
The declaration proves that the actual world coincides with the unique minimum of the J-cost functional. It asserts that x = 1 is actual while every other positive real is merely possible. A philosopher of physics or modal logician working inside the Recognition Science framework would cite the result when grounding actuality in cost minimization. The proof is a direct term-mode construction that splits the conjunction and invokes the defect-zero characterization.
Claim. Let $J(x) = (x + x^{-1})/2 - 1$ be the J-cost and let defect$(x) := J(x)$ for $x > 0$. Then RSActual$(1) $ holds and, for all $x > 0$ with $x ≠ 1$, RSActual$(x)$ fails, where RSActual$(x)$ is defined to mean that $x$ is the unique J-minimizer (i.e., defect$(x) = 0$).
background
In the Recognition Science treatment of modal metaphysics (PH-013), possibility, necessity, and actuality are defined via the J-cost functional. The defect functional satisfies defect$(x) := J(x)$ for positive $x$, with the upstream facts that defect$(1) = 0$ and, for $x > 0$, defect$(x) = 0$ if and only if $x = 1$. RSActual$(x)$ is defined by RSActual$(x) := RSNecessary$(x)$, which the module identifies with being the unique J-minimizer. The module resolves modal questions by grounding them in cost minimization: necessity is unique minimization, possibility requires positive ratio and finite cost, and actuality is the configuration selected by the minimization process.
proof idea
The proof is a term-mode construction. Constructor splits the conjunction. The first conjunct is discharged by the pair consisting of a norm_num computation together with the lemma defect_at_one. The second conjunct proceeds by intro, assuming $0 < x$, $x ≠ 1$, and RSActual$(x)$; the assumption RSActual$(x)$ yields defect$(x) = 0$, so defect_zero_iff_one produces the contradiction $x = 1$.
why it matters
This theorem completes one of the central claims of the RS modal resolution in PH-013: actuality coincides with the unique J-minimum. It directly supports the module's listed downstream claims that necessary implies actual and actual implies possible. Within the broader framework it anchors the accessibility relation, since the unique cost minimum at $x = 1$ is reachable from any positive configuration by a J-decreasing path. The result closes the modal ontology by showing that only the identity configuration is selected by cost minimization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.