rightFactorObservable_not_magnitudeOnly
plain-language theorem explainer
The map that returns the right factor as a natural number is not magnitude-only: equal products need not yield equal right factors. Anyone proving that pure product magnitude cannot serve as a factor oracle cites this. The proof feeds the classical ambiguity 2·6 = 3·4 into the magnitude-only hypothesis and simplifies to a numeric contradiction.
Claim. The observable $F(a,b) = b^{\mathbb{N}}$ (the right factor read as a natural number) is not magnitude-only: it is not true that equal factor-pair products force equal values of $F$. Equivalently, there exist pairs $(a,b)$ and $(c,d)$ with $a\cdot b = c\cdot d$ yet $b^{\mathbb{N}} \neq d^{\mathbb{N}}$.
background
In the Primitive Recognition Calculus factorization layer, observables on factor pairs are maps $F : \mathrm{DistinctionNat} \times \mathrm{DistinctionNat} \to \mathbb{N}$. An observable is magnitude-only when it factors through the product orbit: whenever two pairs share the same product, $F$ returns the same value. That is the content of MagnitudeOnlyObservable.
The concrete obstruction is the classical non-unique factorization of twelve: the pairs $(2,6)$ and $(3,4)$ have identical products but different right factors. Upstream, two_six_product_eq_three_four records exactly that product equality after transport through toNat and multiplication. The local module uses this finite ambiguity to separate pure magnitude data from genuine factor extraction.
proof idea
Term-style proof by contradiction. Assume the right-factor extractor is magnitude-only. Instantiate that hypothesis on the four values ofNat 2, ofNat 6, ofNat 3, ofNat 4, supplying the product equality two_six_product_eq_three_four. The hypothesis then forces the two right-factor naturals to agree. A single simp reduces that equality to $6 = 4$, which is absurd.
why it matters
This is one of the three negative legs of the recognition lower-bound certificate. Downstream, recognition_lower_bound_certificate packages: product magnitude is magnitude-only; the left-factor extractor is not; the right-factor extractor is not; and scalar post-processing of product magnitude remains magnitude-only. Together these show that reading either factor requires strictly more structure than the product orbit alone.
In the Recognition Science foundation this is the finite combinatorial reason magnitude (or any J-cost-style score built only from the product) cannot act as a factor oracle. It sits upstream of any claim that residue, character, or chart data must be coupled to magnitude before factorization becomes observable. It does not itself invoke the forcing chain T0–T8, but it underwrites the later claim that recognition cost cannot collapse to a pure product functional.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.