archimedeanMagnitude
plain-language theorem explainer
The Archimedean magnitude of a finite distinction-orbit position is its verifier natural number (iteration depth). Chart-transition and factorization arguments cite it as the single scalar a product displays. The definition is a one-line projection: apply the orbit-to-Nat map.
Claim. For a finite distinction orbit $n$, the Archimedean magnitude is the natural number obtained by reading off its iteration depth: $\mathrm{mag}(n) := |n|_{\mathbb{N}}$.
background
In the primitive recognition calculus, a distinction orbit (DistinctionNat) is the base-neutral finite orbit of repeated distinction: an inductive type with zero and successor, standing for how many times a distinction has been applied. The verifier map toNat sends that orbit to ordinary Lean Nat by counting successors (zero maps to 0).
The surrounding module studies factorization of orbits and chart transitions: when two factor pairs display the same product, what scalar do they share, and what do they fail to determine? Archimedean magnitude is that displayed scalar. Upstream, ArithmeticFromLogic supplies the same iteration-count reading for logic naturals; here the orbit-level toNat is the direct source.
Locally this sits under factorization and chart-transition certificates: magnitude is the cheap, product-only observable before any claim about recovering individual factors.
proof idea
One-line definitional wrapper. The body is exactly the orbit verifier map: on input $n$, return $n.\mathrm{toNat}$. No lemmas, no tactics; the meaning is the iteration count already defined on distinction orbits.
why it matters
This is the displayed magnitude used throughout the chart-transition obstruction surface. Downstream, same_product_same_magnitude unfolds it and rewrites along product equality, so equal products yield equal magnitudes (the "cheap chart"). productMagnitudeObservable packages the magnitude of a factor-pair product as a magnitude-only observable for recognition lower bounds. ChartTransitionCertificate bundles the product-display law and the same-magnitude law as certificate fields.
In the Recognition foundation stack this separates what a product shows (Archimedean size) from what it underdetermines (left and right factors). Sibling results on magnitude underdetermining factors and on nontrivial factorizations of proper divisors rely on having this scalar named and shared. It is definitional scaffolding for the obstruction, not a forcing-chain step (T5–T8), but it is the concrete display map those factorization theorems quantify over.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.