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 an η-completion: regular sequences, their equivalence, and the η map. Anyone building reals or ordered fields from bare integers without a ℚ display layer would cite it. The module is mostly definitions plus elementary algebraic identities for crossDiff and reflexivity/symmetry of sequence equivalence.

claimFor integer rationals $a,b$ (pairs of integers with positive denominator), the cross-difference is the integer $\mathrm{cd}(a,b) := a_n b_d - b_n a_d$, the numerator of $a-b$. A regular sequence is a sequence of such rationals with a controlled Cauchy modulus. Two regular sequences are equivalent when their pairwise cross-differences vanish in the limit. The module packages $\eta$ (and $\eta$-regularity) as the completion map sending a rational into the corresponding constant regular sequence class.

background

This sits in the Primitive Recognition Calculus grow path: number structure is rebuilt from integers and an integer-rational type, deliberately avoiding Lean’s native $\mathbb{Q}$ pretty-printing and field API. The imported IntegerRational layer supplies fractions as numerator/denominator pairs; IntegerOrder supplies the ordered comparison needed for Cauchy control.

The cross-difference $\mathrm{cd}(a,b)=a_n b_d-b_n a_d$ is the integer numerator of $a-b$. Working with this integer keeps equality, ordering, and vanishing conditions inside $\mathbb{Z}$, which matches the module doc: it “avoids the $\mathbb{Q}$ display entirely.”

From that primitive the module introduces regular sequences (Cauchy sequences of integer rationals with an explicit modulus), the equivalence relation that identifies sequences with vanishing cross-differences, and the $\eta$ embedding of a single rational as a constant regular sequence. Sibling lemmas record the basic algebra: $\mathrm{cd}(a,a)=0$, swap sign, and a triangle identity.

proof idea

Definition-heavy module, not a single theorem. crossDiff is introduced as the bilinear integer $a.num\cdot b.den-b.num\cdot a.den$. Short lemmas then discharge the expected identities (self-vanishing, swap, triangle, and vanishing under cross-equality) by direct expansion in $\mathbb{Z}$.

RegularSeq, equiv, eta, eta_seq, and eta_regular are type/structure definitions. equiv_refl and equiv_symm are the first two equivalence laws, proved from the crossDiff identities and the regular-sequence modulus. No deep analytic argument appears at this M0a stage; the work is algebraic bookkeeping that later completion steps can quote.

why it matters in Recognition Science

η-completion is the grow-path bridge from integer rationals to a Cauchy real layer inside Recognition Science’s foundation stack, before continuum structure is fed into the forcing chain (T0–T8) and cost calculus. Cross-difference is the integer witness that lets equality and Cauchy conditions stay native to $\mathbb{Z}$, which keeps later Recognition Composition Law and J-cost developments free of an opaque rational field.

No downstream used_by edges are recorded yet for this module, so it currently acts as a leaf definition package for later Grow/completion files. Parent consumers will be whatever constructs limits, addition of regular sequences, or the ordered field of η-classes. Until those land, this file closes the M0a scaffolding: regular sequences plus the η embedding and the first equivalence laws.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (23)