IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCCompletenessIndependence
The module separates order-completeness of the scalar field from the Primitive Recognition Calculus cost axioms. It shows that J-cost and the genuine cost laws hold on incomplete ordered subfields of the reals, so completeness is not forced by those laws. Completeness is identified with the continuum (every nonempty bounded-above set has a least upper bound in the field). Anyone arguing that RS forces R rather than a thinner ordered field cites this independence package.
claimRelative least upper bounds: $s\in K$ is an LUB of $S$ in a subfield $K\subseteq\mathbb{R}$ if $s$ bounds $S$ and $s\le$ every upper bound of $S$ that lies in $K$. The module proves that countable and other proper subfields of $\mathbb{R}$ fail order-completeness, that the standard $J$-cost meets the cost-requirement axioms on such fields, and therefore that completeness is not a consequence of the cost axioms; it is exactly the continuum property of $\mathbb{R}$.
background
Primitive Recognition Calculus equips an ordered field with a cost functional whose algebraic skeleton is fixed by the Recognition Composition Law and the unique $J$-cost $J(x)=(x+x^{-1})/2-1$ (T5). The companion module on cost-on-a-field packages those axioms so they can be checked on any ordered field, not only on $\mathbb{R}$.
Order-completeness is the separate demand that every nonempty $S$ bounded above has a least upper bound inside the field. The relativized predicate used here asks only for an LUB that lives in a designated subfield $K$: it bounds $S$ and is $\le$ every $K$-element that bounds $S$. That is the notion completeness of $K$ would always supply.
The Cost import supplies the concrete $J$-cost and the requirement interface; the PRC-cost-on-field import supplies the field-level cost laws against which independence is measured.
proof idea
The module is a short independence argument, not a single theorem. It first defines relative LUBs in a subfield. It then exhibits incomplete subfields (countable subfields, a named thin field $T$, and generic proper subfields) and records that $\mathbb{R}$ itself has LUBs. Separately it checks that $J$-cost satisfies the cost-requirement interface on those structures. Combining the two directions yields the two headline statements: completeness is not forced by the cost axioms, nor by the genuine cost laws, and completeness is exactly the continuum property.
why it matters in Recognition Science
In the Foundation layer this module blocks a common overclaim: that the PRC/J-cost package already forces the scalar continuum. Downstream work that needs $\mathbb{R}$ (measures, limits, continuum spectra) must import completeness as an independent hypothesis rather than derive it from T5 or the cost laws. The package sits next to the forcing chain (T5 $J$-uniqueness, T6 $\varphi$, T7 eight-tick, T8 $D=3$) and clarifies that those forcings do not smuggle Dedekind completeness. With no external used-by edges yet, it is a leaf that hardens the foundation boundary between cost algebra and analytic completeness.
scope and limits
- Does not derive Dedekind completeness from J-cost or RCL.
- Does not claim every incomplete ordered field carries a PRC cost model.
- Does not construct the reals; it only uses standard LUB existence on R.
- Does not address topological or metric completeness beyond order-LUBs.
- Does not alter mass, alpha, or forcing-chain (T5–T8) results.
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