magnitude_underdetermines_right_factor
plain-language theorem explainer
Equal products of distinction numbers need not share the same right factor: 2·6 and 3·4 agree as products while 6 ≠ 4. Anyone arguing that Archimedean magnitude (orbit product data) cannot serve as a factor oracle cites this finite obstruction. The proof is a one-line pairing of the product identity with the inequality of the right factors.
Claim. The factor-pair products satisfy $\mathrm{prod}(2,6)=\mathrm{prod}(3,4)$ while the right factors are unequal: $6\neq 4$ in the distinction naturals. Thus magnitude data alone does not determine the right factor.
background
In the chart-transition layer of Primitive Recognition Calculus, a factor pair is two distinction naturals, and the positional chart records only their product. The definition factorPairProduct is ordinary multiplication on DistinctionNat; the Archimedean magnitude of an orbit position is what that product displays.
The module isolates a finite obstruction: distinct pairs can share a product. Upstream, two_six_product_eq_three_four states the concrete equality $2\cdot 6=3\cdot 4$ after transport to ordinary naturals, and six_ne_four records $6\neq 4$ by injectivity of toNat. Together they show that reading only the product (magnitude) cannot recover which right factor was used.
This sits next to the twin left-factor statement and feeds the reusable nontrivial-factorization endpoint used when a period witness supplies a proper gcd divisor.
proof idea
One-line term proof: pair the two already-proved facts. The first conjunct is two_six_product_eq_three_four (product equality via toNat_inj and simplification of multiplication). The second is six_ne_four (inequality of right factors by congruence on toNat and simp). No further arithmetic is done here.
why it matters
Recognition Science treats magnitude as chart data, not as a factorization oracle. This lemma is the right-factor half of that obstruction: same product, different right factor. It sits beside magnitude_underdetermines_left_factor and supports the narrative that period-readout factoring must come from a proper divisor (gcd layer), not from magnitude alone.
Downstream the module aims at nontrivialFactorization_of_proper_divisor and ChartTransitionCertificate; those close the path from a proper nonunit divisor to a native nontrivial factorization. No parent theorem currently lists this declaration as a direct dependency, so its role is local certificate material inside the factorization chart-transition story rather than a forcing-chain landmark (T0–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.