Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RealNullSetoid

show as:
view Lean formalization →

Packages the exact analytic blocker needed to form the null-distance quotient of recognition reals: the J-cost rational distance admits a local triangle modulus. Anyone building PRCRealNull or the null setoid cites this layer. The module states the modulus target, reduces setoid formation to transitivity of null distance, and records a conditional certificate once the modulus is supplied.

claimThe $J$-cost-derived rational distance $d$ on Cauchy data has a local triangle modulus: for every $\varepsilon>0$ there is $\delta>0$ such that $d(x,y)<\delta$ and $d(y,z)<\delta$ imply $d(x,z)<\varepsilon$. Under that modulus, null distance ($d=0$) is an equivalence relation, and the quotient $\mathrm{PRCRealNull}$ is well-defined as a setoid of recognition reals.

background

Primitive Recognition Calculus builds reals from Cauchy-style data over a $J$-cost geometry rather than from classical absolute value. Upstream, RealCauchy supplies the Cauchy sequences and the rational distance induced by the unique cost $J(x)=(x+x^{-1})/2-1$ (T5). Null pairs are those at $J$-distance zero; the quotient by that relation is the intended carrier of recognition reals.

Forming a setoid needs reflexivity, symmetry, and transitivity of null distance. Reflexivity and symmetry are cheap; transitivity is the analytic obstruction. The module isolates that obstruction as a local triangle modulus: small legs force a small hypotenuse at every positive tolerance. That is strictly weaker than a global Lipschitz or metric triangle inequality, but enough to close null-transitivity.

Sibling targets name the modulus hypothesis, the implication from modulus to null-transitivity, the setoid constructor from a transitive null relation, the quotient type, and a conditional certificate packaging the claim until the modulus is proved.

proof idea

Definition and interface module, not a closed proof. It declares the triangle-modulus target as a Prop, proves the pure logical reductions (modulus implies null-transitivity; transitive null relation yields a setoid; setoid yields the quotient type and ofRat embedding), and exposes realNullSetoidClaim plus a conditional certificate that waits on the modulus. No analytic estimate is discharged here; the heavy inequality work is deferred to the triangle module that imports this one.

why it matters in Recognition Science

Without a null setoid there is no quotient carrier for recognition reals, so every later PRC construction (kernel calculus, $J$-cost metric geometry, mass ladder bookkeeping) stalls. Downstream, PRCJCostDistanceTriangle is the natural home for proving the modulus, and Kernel imports the setoid layer to work on the quotient. In the forcing chain this sits under T5 $J$-uniqueness: the distance is $J$-derived, and the modulus is the remaining analytic gate before null classes behave like points. The conditional certificate marks an explicit scaffold seam rather than a silent sorry in consumer modules.

scope and limits

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (10)