IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RealNullSetoid
Module packaging the analytic blocker that turns J-cost rational distance into a null-distance setoid on Cauchy reals. It isolates a local triangle modulus: small legs force a small composed leg under any positive tolerance. Downstream Kernel and triangle modules import this to quotient by null pairs. The argument is target/certificate scaffolding around that modulus, not a closed unconditional proof.
claimFor the $J$-cost-derived rational distance $d_J$ on Cauchy reals, a local triangle modulus holds: for every $\varepsilon>0$ there is $\delta>0$ such that $d_J(x,y)<\delta$ and $d_J(y,z)<\delta$ imply $d_J(x,z)<\varepsilon$. Null pairs ($d_J=0$) then form a setoid, yielding the quotient real-null type.
background
Primitive Recognition Calculus builds reals from Cauchy data and a cost derived from the Recognition $J$-functional $J(x)=(x+x^{-1})/2-1$. Distance between rationals (and then Cauchy sequences) is read off $J$, not from an a priori metric axiom. The Recognition Composition Law constrains how $J$ multiplies, so triangle-type inequalities are analytic statements about $J$, not free postulates.
This module sits on RealCauchy: Cauchy sequences of rationals with the $J$-cost distance. The null relation is $d_J(x,y)=0$. To quotient, one needs reflexivity, symmetry, and transitivity of nullness. Transitivity is the hard step; it follows once a local triangle modulus is available: for each positive tolerance a stricter positive tolerance forces the composed leg below the original bound.
Sibling targets name that modulus, the transitive null relation, the setoid package, an ofRat embedding, and conditional certificates that discharge the setoid claim once the modulus is granted.
proof idea
Definition and interface module, not a single closed theorem. It declares modulus and setoid targets (PRCJCostDistanceTriangleModulusTarget, transitive and setoid targets), the real-null carrier PRCRealNull, and conditional certificates (PRCRealNullSetoidConditionalCertificate, real_null_setoid_conditional_certificate). The logical spine is: triangle modulus implies null-distance transitivity; transitivity yields a setoid; the setoid yields the null quotient. Unconditional discharge of the modulus lives downstream or remains a named analytic blocker.
why it matters in Recognition Science
Without a null setoid, PRC cannot form a clean real line on which later cost-distance geometry lives. Downstream Kernel imports this module as foundation for the PRC kernel, and PRCJCostDistanceTriangle consumes the triangle-modulus interface. In the broader Recognition chain, $J$-uniqueness (T5) and the composition law make $d_J$ the canonical cost distance; the local modulus is the remaining analytic gate between that cost and a Hausdorff-style real quotient. The module therefore pins the exact blocker for null-distance quotienting rather than papering over it with an axiomatic metric.
scope and limits
- Does not prove the triangle modulus unconditionally; it packages targets and certificates.
- Does not construct the full metric completion beyond the null quotient interface.
- Does not derive $J$-uniqueness or the Recognition Composition Law; those are upstream.
- Does not claim physical units or mass-ladder results; scope is pure PRC real structure.
- Does not discharge Kernel theorems; it only supplies the imported setoid scaffolding.
used by (2)
depends on (1)
declarations in this module (10)
-
def
PRCJCostDistanceTriangleModulusTarget -
theorem
PRCNullDistanceTransitiveTarget_of_triangle_modulus -
def
PRCNullDistanceSetoidOfTransitive -
def
PRCRealNull -
def
ofRat -
theorem
PRCNullDistanceSetoidTarget_of_transitive -
theorem
PRCNullDistanceSetoidTarget_of_triangle_modulus -
def
realNullSetoidClaim -
structure
PRCRealNullSetoidConditionalCertificate -
theorem
real_null_setoid_conditional_certificate