IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCCompletenessIndependence
The cost axioms of Primitive Recognition Calculus do not force order-completeness of the scalar field. Any proper subfield of the reals (including countable ones and the explicit tower field T) can carry a genuine J-cost while failing to have least upper bounds inside itself. Completeness is therefore independent of the cost laws and coincides exactly with being the continuum. Cite when separating analytic structure from the Recognition Composition Law.
claimOrder-completeness of a scalar field $K$ is independent of the PRC cost axioms. There exist subfields $K \subset \mathbb{R}$ that admit a cost $J$ satisfying the genuine cost laws (including $J(x)=(x+x^{-1})/2-1$) yet fail to contain least upper bounds of bounded subsets. Completeness holds if and only if $K$ is (order-isomorphic to) the continuum.
background
Primitive Recognition Calculus equips a scalar field with a cost functional $J$ obeying the Recognition Composition Law and related positivity and normalization axioms. The companion module PRCCostOnField develops those axioms on an abstract field; the present module asks whether those same axioms already force the least-upper-bound property.
The key auxiliary notion is a relativized supremum: $s$ is a least upper bound of $S$ lying inside a subfield $K$ when $s\in K$, $s$ bounds $S$, and every $K$-element that bounds $S$ is at least $s$. Order-completeness of $K$ would supply such an $s$ for every nonempty $S\subset K$ that is bounded above in $K$.
The ambient comparison object is $\mathbb{R}$ with its standard order and the unique continuous cost $J(x)=\cosh(\log x)-1$ (equivalently $(x+x^{-1})/2-1$), which does have the LUB property.
proof idea
The module builds a short chain of counterexamples and a positive characterization. First it defines the relativized LUB predicate, then shows that any proper subfield of $\mathbb{R}$ fails to be complete in that sense, with a countable specialization and an explicit incomplete tower field $T$. Separately it records that $\mathbb{R}$ itself has LUBs. The cost side is discharged by verifying that the standard $J$-cost meets the full cost-requirement package on those incomplete carriers, yielding the two independence theorems: completeness is not forced by the bare cost axioms, nor by the genuine cost laws. The final result identifies completeness with the continuum.
why it matters in Recognition Science
In the Recognition Science forcing chain, T5 fixes the unique cost $J$ and T6–T8 extract $\varphi$, the eight-tick period, and $D=3$ from self-similarity and discrete structure. Those steps live on the cost and combinatorial side; they do not smuggle in Dedekind completeness. This module makes that separation precise: any derivation that needs the continuum (analytic spectra, measure, or continuous limits) must postulate completeness separately rather than claim it follows from RCL or the cost axioms alone. Downstream work that builds continuous physics on PRC can therefore cite the independence theorems when justifying an explicit completeness hypothesis, and the final continuum characterization pins the exact extra assumption required.
scope and limits
- Does not derive the form of $J$ itself; uniqueness of $J$ is upstream (T5).
- Does not construct physical units, masses, or coupling constants from incompleteness.
- Does not claim every incomplete field admits a cost; only that cost axioms permit incomplete carriers.
- Does not address topological or metric completeness beyond order-LUB.
- Does not feed a named downstream theorem in the current graph (used_by is empty).
depends on (2)
declarations in this module (9)
-
def
IsLUBIn -
theorem
subfield_not_complete -
theorem
countable_subfield_not_complete -
theorem
T_not_complete -
theorem
real_has_lub -
theorem
completeness_not_forced_by_cost_axioms -
theorem
jcost_isCostRequirements -
theorem
completeness_not_forced_by_genuine_cost_laws -
theorem
completeness_is_exactly_the_continuum