factorPairProduct_toNat
plain-language theorem explainer
The verifier Nat of a factor-pair product equals the ordinary product of the two verifier Nats. Anyone building chart-transition or factorization certificates cites this to connect the positional product chart to ordinary arithmetic. The proof unfolds the product definition and applies the existing orbit multiplication recovery lemma.
Claim. For any two distinction-orbit positions $a$ and $b$, if $p$ is the product orbit $a\cdot b$ (the quantity the positional chart displays), then the verifier natural number of $p$ equals the product of the verifier natural numbers of $a$ and $b$: $\mathrm{toNat}(p)=\mathrm{toNat}(a)\cdot\mathrm{toNat}(b)$.
background
DistinctionNat is the base-neutral finite orbit of repeated distinction (K2.12): an inductive type with zero and successor, the primitive recognition calculus stand-in for counting by successive distinctions. Its verifier map toNat sends an orbit position to the corresponding Lean natural number by reading off the iteration count.
Orbit multiplication is defined on DistinctionNat so that the verifier display recovers ordinary Nat multiplication (K4.7): $(a\cdot b).\mathrm{toNat}=a.\mathrm{toNat}\cdot b.\mathrm{toNat}$. The same recovery already exists for the more abstract LogicNat layer in ArithmeticFromLogic.
In this module, factorPairProduct is the positional chart's view of a pair: it is literally $a\cdot b$. The chart is deliberately product-only; magnitude is the Archimedean display of that product. The local setting is chart transition for factorization: when two different pairs share a product, they share displayed magnitude, so the cheap chart underdetermines the factors.
proof idea
One-line style term proof after a definitional unfold. Unfold factorPairProduct (which is $a\cdot b$), then apply OrbitArithmetic.toNat_mul on $a$ and $b$. That lemma is the induction on the right factor establishing that orbit multiplication matches Nat multiplication under toNat. No extra algebraic work is needed here.
why it matters
Feeds chart_transition_certificate as the product_display field: the certificate packages that the positional chart's product agrees with verifier multiplication, that equal products give equal magnitudes, and that an explicit ambiguous product (2·6 = 3·4) exists. Without this equality, the certificate could not tie the chart's displayed product back to ordinary arithmetic.
In the Primitive Recognition Calculus factorization story, this is the bridge from orbit algebra to the verifier Nat layer used by magnitude and ambiguity lemmas (same_product_same_magnitude, magnitude_underdetermines_left/right_factor). It is foundation plumbing rather than a forcing-chain landmark (T5–T8), but it is required for any later claim that factorization charts are product-blind in the Archimedean display.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.