factorPairProduct
plain-language theorem explainer
Multiplication of two distinction-orbit positions yields another orbit position: the product the positional chart can display. Chart-transition and magnitude-underdetermination arguments cite this as the only observable of a factor pair. The body is the native orbit product, nothing more.
Claim. Given distinction-orbit positions $a$ and $b$, their factor-pair product is the orbit position $a \cdot b$. The positional chart records only this product, not the ordered factors.
background
DistinctionNat is the base-neutral finite orbit of repeated distinction (K2.12): an inductive copy of the naturals built from zero and successor, with decidable equality. It carries a native multiplication and a forgetful map toNat into ordinary naturals.
This module studies factorization as a chart-transition problem. A factor pair is two orbit positions; the cheap (Archimedean) chart is allowed to see only a single magnitude built from their product. The definition here is that product, so later lemmas can compare pairs that share a product but differ as ordered factors.
The surrounding development contrasts that cheap magnitude chart with any chart that would recover the factors themselves. Concrete ambiguity already appears at $2 \cdot 6 = 3 \cdot 4$.
proof idea
One-line definition: the factor-pair product is the native multiplication on DistinctionNat. No lemmas are applied; downstream theorems unfold this abbreviation and reduce via toNat_mul or injectivity of toNat.
why it matters
This is the displayed observable of a factor pair in the chart-transition obstruction surface. ChartTransitionCertificate packages the product-display law and the same-product-same-magnitude law built on it. Immediate clients prove that equal products give equal Archimedean magnitudes, that $2\cdot 6$ and $3\cdot 4$ coincide as products, and that magnitude therefore underdetermines both the left and right factors.
Downstream, RecognitionLowerBound treats product magnitude as a magnitude-only observable, so the cheap chart cannot serve as a factor oracle. In the Primitive Recognition Calculus this is the finite combinatorial seed of the claim that positional magnitude alone does not recover factorization data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.