same_product_same_magnitude
plain-language theorem explainer
Equal factor-pair products on DistinctionNat display equal Archimedean magnitudes. Anyone proving that magnitude is a product-only observable, or assembling the chart-transition certificate, cites this. The proof is a two-step term: unfold the magnitude projection and rewrite by the product equality.
Claim. For any $a,b,c,d$ in the base-neutral distinction orbit, if the factor-pair products agree ($a\cdot b = c\cdot d$), then the Archimedean magnitudes of those products agree: $|a\cdot b|_{\mathrm{Arch}} = |c\cdot d|_{\mathrm{Arch}}$.
background
In the Primitive Recognition Calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction (an inductive copy of the naturals). A factor pair is two such orbit positions; the positional chart records only their product via factorPairProduct a b := a * b.
The displayed scalar is the Archimedean magnitude archimedeanMagnitude n := n.toNat, i.e. the ordinary natural number underlying the orbit position. The module's theme is the chart-transition obstruction: magnitude sees products, not individual factors, so distinct factorizations can share one displayed magnitude (the concrete witness is $2\cdot 6 = 3\cdot 4$).
This lemma is the cheap half of that story: product equality immediately forces magnitude equality. It is pure transport along the definition of the display map.
proof idea
Term-mode, two tactics. Unfold archimedeanMagnitude so both sides become .toNat of the respective products. Rewrite with the hypothesis that the products are equal. No arithmetic lemmas are needed; equality of the underlying orbit positions is enough.
why it matters
This is the "same product, same magnitude" field of ChartTransitionCertificate, the Prop packaging the chart-transition obstruction surface. The assembled certificate chart_transition_certificate plugs it in directly, alongside product-to-Nat display and the explicit $2\cdot 6 = 3\cdot 4$ ambiguity.
Downstream, productMagnitudeObservable_magnitudeOnly uses it to show that the product-magnitude observable is magnitude-only: equal products yield equal observations. In the Recognition factorization layer this pins the cheap chart direction before the harder claims that magnitude underdetermines left and right factors. It is scaffolding for the obstruction surface, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.