Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.EtaCompletionM0a

show as:
view Lean formalization →

Defines the cross-difference of integer rationals and the first layer of eta-completion: regular sequences, their equivalence, and the eta map. Anyone building a ℚ-free real completion inside Primitive Recognition Calculus cites this. The module is mostly definitions plus elementary algebraic identities for the cross-difference and reflexivity/symmetry of sequence equivalence.

claimFor integer rationals $a,b$ with numerators and denominators in $\mathbb{Z}$, the cross-difference is $\delta(a,b) := a_{\mathrm{num}} b_{\mathrm{den}} - b_{\mathrm{num}} a_{\mathrm{den}}$, the integer numerator of $a-b$. The module then introduces regular sequences of such rationals, an equivalence relation on them, and the eta embedding of a rational as a constant (or canonical) sequence, together with basic identities $\delta(a,a)=0$, antisymmetry under swap, and a triangle identity.

background

Primitive Recognition Calculus builds arithmetic from integers upward without leaning on Lean's native rationals display. The imported IntegerRational layer supplies fractions as pairs of integers (numerator, positive denominator). IntegerOrder supplies the ordered structure used to state regularity and comparison.

The cross-difference $\delta(a,b)$ is the integer $a_{\mathrm{num}} b_{\mathrm{den}} - b_{\mathrm{num}} a_{\mathrm{den}}$. It is exactly the numerator of $a-b$ after clearing denominators, so sign and vanishing of $\delta$ decide order and equality without constructing a $\mathbb{Q}$ value. Sibling facts record $\delta(a,a)=0$, the swap rule $\delta(b,a)=-\delta(a,b)$, vanishing when a cross-equality holds, and a triangle identity that supports later Cauchy-type estimates.

On top of that, the module packages regular sequences of integer rationals, an equivalence relation on those sequences, and the eta construction that sends a single rational to a sequence (the seed of the completion map). This is the M0a slice of the eta-completion grow path: enough structure to talk about representatives before proving fullness of the equivalence or completeness of the quotient.

proof idea

Definition-heavy module, not a single theorem. crossDiff is introduced as the bilinear integer expression above; its lemmas are short algebraic rewrites (self-vanishing, swap, consequence of cross-equality, triangle identity). RegularSeq, equiv, eta, and eta_seq are data definitions. equiv_refl and equiv_symm are the first two equivalence-relation obligations, discharged from the cross-difference identities and the regularity predicate. No deep analysis or completeness proof lives here; those sit further along the Grow chain.

why it matters in Recognition Science

Eta-completion is how Recognition Science obtains a real line from discrete recognition data while staying inside the integer-rational substrate. This M0a module is the local foundation: cross-difference gives a denominator-clearing defect that later feeds metric and order arguments, and eta seeds the embedding of base rationals into sequence space.

Downstream consumers (not yet wired in the graph snapshot) are the later Grow milestones that prove equiv is an equivalence relation in full, construct the quotient, and connect regular-sequence limits to the phi-ladder and forcing-chain analytics. Without a clean cross-difference, every comparison would re-enter native $\mathbb{Q}$ and break the primitive calculus invariant.

In the broader framework this sits under Foundation, upstream of cost and forcing material (J-uniqueness, eight-tick structure), by guaranteeing that continuum objects used later are built from the same integer substrate as the discrete recognition steps.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (23)