magnitude_underdetermines_left_factor
plain-language theorem explainer
Equal products need not share the left factor: the pairs (2,6) and (3,4) have the same product in DistinctionNat, yet 2 ≠ 3. Anyone treating Archimedean magnitude as a factor oracle in the chart-transition layer should cite this finite obstruction. The proof is a one-line pairing of the product identity with the inequality of the left legs.
Claim. The factor-pair products of the orbit positions $2$ with $6$ and $3$ with $4$ coincide, while the left factors differ: $\mathrm{prod}(2,6)=\mathrm{prod}(3,4)$ and $2\neq 3$ in the distinction naturals. Thus magnitude data alone cannot recover the left factor in general.
background
In the Primitive Recognition Calculus factorization layer, a factor pair is two distinction-naturals whose product is what the positional chart actually sees. The definition factorPairProduct is ordinary multiplication on DistinctionNat; its doc states that the positional chart sees only that product. Orbit positions are built from verifier naturals via ofNat.
Archimedean magnitude is the scalar display of an orbit position. The local module studies when that magnitude (equivalently, the product) fails to determine the factors. Upstream, two_six_product_eq_three_four records the concrete ambiguity: "2 * 6 and 3 * 4 are different factor pairs with the same product. This is the finite obstruction behind 'magnitude is not a factor oracle.'" The companion inequality two_ne_three is the left-leg separation obtained by injecting to ordinary Nat.
proof idea
Term-mode one-liner. The goal is a conjunction; the proof supplies the pair ⟨two_six_product_eq_three_four, two_ne_three⟩. The first conjunct is the already-proved product identity (via toNat injectivity and simplification of multiplication). The second is the already-proved left-factor inequality. No further rewriting is required.
why it matters
This is the left-factor half of the finite obstruction that magnitude is not a factor oracle. It sits beside the sibling right-factor statement and the shared product identity, and it feeds the chart-transition certificate story in the same module: any bridge from Archimedean magnitude back to a unique factorization must fail on this pair. In Recognition terms it is a foundation-level non-uniqueness fact about reading factors off products, not a dynamical or continuum claim; it constrains how much structure a positional chart may pretend to recover from magnitude alone. No downstream theorems currently depend on it in the graph, so its role is local certification of the obstruction rather than a forcing-chain step (T0–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.