Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Factorization.ChartTransition

show as:
view Lean formalization →

Defines native factor pairs for an orbit position n and the archimedean magnitude of a pair (the product). Shows that equal products need not share left or right factors, via the concrete 2·6 = 3·4 witness, and packages a chart-transition certificate. ResidueOrbit imports this layer. Argument is elementary Nat arithmetic plus a small certificate structure.

claimA factor pair for an orbit position $n$ is a pair $(a,b)$ of naturals with $a\cdot b$ corresponding to $n$. The archimedean magnitude of a pair is that product. Equal magnitude does not force equal left factors or equal right factors: $2\cdot 6 = 3\cdot 4$ with $2\neq 3$ and $6\neq 4$. Proper divisors yield nontrivial factorizations. A chart-transition certificate records such underdetermination.

background

This module sits in the Primitive Recognition Calculus factorization layer, importing the Euclidean orbit infrastructure. Orbit positions are treated as natural numbers; a factorization is a pair of factors whose product recovers the position.

The central objects are a native factor-pair type for an orbit position $n$, the product map on pairs, and an archimedean magnitude extracted from that product. Magnitude is the coarse invariant visible without choosing a chart (ordered factorization).

The module then isolates the elementary fact that magnitude alone does not determine either factor: distinct pairs can share a product. That underdetermination is the mathematical content of a chart transition between factor presentations of the same orbit position.

proof idea

Definition-heavy module with short Nat lemmas. Factor pairs and product/magnitude maps are introduced first. Equality of products for the pairs $(2,6)$ and $(3,4)$ is checked by computation; inequality of the corresponding left and right factors is immediate. Those facts feed two underdetermination lemmas (left factor and right factor). A proper-divisor construction supplies nontrivial factorizations. The chart-transition certificate bundles the underdetermination witness for downstream use. No deep tactics; the load-bearing step is the explicit $2\cdot 6=3\cdot 4$ example.

why it matters in Recognition Science

Chart transitions matter once orbit positions are factored and residue data is read in a chosen chart: the same magnitude can sit over distinct factor presentations, so invariants must be checked for chart independence. Downstream, ResidueOrbit imports this module to work with residue data on factorized orbits without silently identifying distinct charts.

In the broader Recognition foundation, this is bookkeeping for the discrete orbit/factor side of the primitive recognition calculus, not a forcing-chain (T0–T8) step. It keeps factorization language native before residue and Euclidean orbit structure are combined. The certificate is the reusable handle for “same product, different factors” wherever later lemmas need an explicit transition witness.

scope and limits

used by (1)

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 (13)