IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RationalField
Defines the PRC-native rational field structure on ratio orbits: positivity as a signed numerator over a nonzero orbit denominator, together with division and elementary additive identities. Downstream Kernel, RealCauchy, and RecognizerBridge import it to treat ratios as a field before completing to reals. The module is mostly definitions and short algebraic lemmas, not a deep existence proof.
claimOn PRC ratio orbits, a ratio is positive when its signed numerator is positive and its orbit denominator is nonzero. The module equips these ratios with division $x/y$, a field-like additive structure (associativity and unit laws for addition), and the correspondence between native positivity and the image under the map to ordinary rationals being positive.
background
Primitive Recognition Calculus (PRC) builds arithmetic from recognition cost and orbit data rather than from classical $\mathbb{Q}$ as a primitive. The upstream module PRCJCost supplies the $J$-cost side of that calculus; this module turns ratio orbits into a usable rational field layer.
Positivity is PRC-native: a positive ratio is a positive signed numerator over a nonzero orbit denominator. The denominator is an orbit position, so "nonzero" is displayed as positive in the verifier but is not baked into the object definition itself. Sibling material includes normalization of positivity, the implication that positive ratios are nonzero, an explicit division operation and its toRat intertwining, and the basic additive monoid laws (associativity, zero on left and right).
The setting is foundational bookkeeping inside Foundation.PrimitiveRecognitionCalculus: enough ordered-field structure on orbits to support Cauchy completion and recognizer bridges without smuggling classical $\mathbb{Q}$ axioms as unexamined primitives.
proof idea
This is primarily a definition and interface module, not a single deep theorem. Positivity and division are introduced as defs; short lemmas relate native positivity to the sign of the rational image, show positives are nonzero, normalize positivity, and record toRat of a quotient. Additive structure is discharged by routine algebraic rewrites (associativity and zero laws). No long tactic scripts or forcing-chain arguments live here.
why it matters in Recognition Science
Kernel, RealCauchy, and RecognizerBridge all import this module, so every later PRC construction that needs ratios, ordered division, or a path from orbit arithmetic toward real completion depends on these definitions. In the Recognition Science stack this sits under Foundation: it is the rational stepping-stone between $J$-cost primitives and continuum-level recognizer calculus, before T5–T8 forcing (unique $J$, $\varphi$, eight-tick period, $D=3$) is applied at the physics layer. Without a clean native positivity and division story, Cauchy sequences and bridge maps would have to reintroduce classical rationals ad hoc.
scope and limits
- Does not construct the reals or prove completeness; that is RealCauchy's job.
- Does not force $J$-uniqueness, $\varphi$, eight-tick structure, or $D=3$.
- Does not claim classical $\mathbb{Q}$ axioms as primitives; only PRC orbit ratios.
- Does not by itself define mass ladders, $\alpha$, or physical constants.
- Does not discharge recognizer bridge theorems; only supplies the rational substrate.
used by (3)
depends on (1)
declarations in this module (31)
-
def
positive -
theorem
positive_iff_toRat_pos -
theorem
positive_normalize -
theorem
positive_not_zero -
def
div -
instance
instDiv -
theorem
div_eq -
theorem
toRat_div -
theorem
positive_ne_zero -
theorem
add_assoc' -
theorem
zero_add' -
theorem
add_zero' -
theorem
add_left_neg' -
theorem
add_right_neg' -
theorem
mul_assoc' -
theorem
one_mul' -
theorem
mul_one' -
theorem
zero_mul' -
theorem
mul_zero' -
theorem
right_distrib' -
theorem
left_distrib' -
theorem
inv_zero -
theorem
inv_mul_cancel -
theorem
div_mul_cancel -
theorem
mul_div_cancel -
def
onPRCRat -
theorem
onPRCRat_mk -
theorem
onPRCRat_toRat -
theorem
onPRCRat_normalized_representative -
structure
RationalFieldCertificate -
theorem
rational_field_certificate