IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RationalField
Defines the PRC-native rational field structure: ratio orbits with a positivity predicate (signed numerator over a nonzero orbit denominator) and the induced division and additive laws. Foundation material for anyone building the recognizer calculus over Q before Cauchy completion. Mostly definitional scaffolding plus elementary algebraic identities.
claimA PRC ratio orbit is positive when it has a positive signed numerator over a nonzero orbit denominator. The module equips these orbits with division $x/y$, a map to ordinary rationals, and the standard field identities (associativity and unit laws for addition, compatibility of division with the rational embedding).
background
Primitive Recognition Calculus (PRC) rebuilds arithmetic from recognition cost before importing classical analysis. The companion module on the J-cost supplies the cost functional $J$ that later forces $\varphi$ and the eight-tick structure; this module stays at the rational layer.
The central object is a ratio orbit: a signed numerator paired with an orbit-position denominator. Nonzero for the denominator is a display/verifier condition, not part of the object definition itself. Positivity is the PRC-native predicate on those orbits (positive signed numerator, nonzero denominator), with lemmas relating it to the ordinary positivity of the embedded rational.
Division is introduced as an instance on this type, with equalities showing that the embedding into $\mathbb{Q}$ intertwines PRC division with ordinary rational division. Additive monoid laws appear in primed form (associativity, left and right zero) as the first algebraic skeleton of a field.
proof idea
Definition module with elementary algebraic lemmas, not a deep proof development. Positivity is introduced as a predicate; companion lemmas normalize it, show it excludes zero, and equate it with positivity of the rational image. Division is a structure instance plus equational lemmas (div_eq, compatibility of toRat with division). Additive identities are short rewrites of the underlying representation. No forcing-chain or analytic argument lives here.
why it matters in Recognition Science
Feeds three downstream PRC modules: Kernel (core recognizer operations), RealCauchy (Cauchy completion from the rational layer to reals), and RecognizerBridge (linking the native calculus to the broader Recognition stack). Without a clean rational field and positivity, the later passage to real Cauchy sequences and the recognizer bridge has no carrier.
In the wider framework this sits below the forcing chain (T5 J-uniqueness through T8 dimension): it is pre-analytic substrate so that cost, $\varphi$, and octave structure can be stated over a rigorously positive ordered field rather than an ad hoc quotient.
scope and limits
- Does not construct real numbers or prove completeness; that is RealCauchy.
- Does not derive J-uniqueness, phi, or the eight-tick octave.
- Does not define the full ordered-field axiom set beyond listed additive and division lemmas.
- Does not address physical constants, mass ladder, or alpha bounds.
- Denominator nonzeroness is a display condition, not an internal field axiom proof.
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