leftFactorObservable_not_magnitudeOnly
plain-language theorem explainer
A map that returns only the left factor of a pair cannot depend solely on the product magnitude: equal products can carry unequal left coordinates. Anyone arguing that Archimedean magnitude is blind to factor charts cites this obstruction. The proof feeds the concrete pair equality 2·6 = 3·4 into the magnitude-only hypothesis and simplifies to 2 = 3.
Claim. The observable $F(a,b) = \mathrm{toNat}(a)$ (left-factor extractor) is not magnitude-only: it is not true that equal factor-pair products force equal $F$-values. Equivalently, there exist pairs with the same product but different left coordinates.
background
In the primitive recognition calculus, factor pairs live on distinction-orbit positions. A magnitude-only observable is any $F$ that factors through the product orbit: whenever two pairs share the same product position, $F$ returns the same natural number. The displayed product magnitude is the canonical example of such an $F$.
The left-factor extractor ignores the right coordinate and reads only the left orbit as a verifier natural via $\mathrm{toNat}$. Upstream, the chart-transition lemma records the finite ambiguity $2\cdot 6 = 3\cdot 4$ as distinct factor pairs with identical product; that equality is the concrete obstruction behind "magnitude is not a factor oracle."
Locally this module builds the recognition lower-bound certificate: product magnitude is magnitude-only, while genuine factor extractors are not.
proof idea
Term-mode proof by contradiction. Assume the left-factor map is magnitude-only. Instantiate that hypothesis on the four orbit positions $\mathrm{ofNat},2$, $\mathrm{ofNat},6$, $\mathrm{ofNat},3$, $\mathrm{ofNat},4$, feeding the upstream equality that their factor-pair products coincide. Simplification then yields $2=3$, which is absurd. No further lemmas are needed beyond the chart-transition product identity.
why it matters
This is one of the three core legs of the recognition lower-bound certificate: product magnitude is magnitude-only, yet neither left nor right factor extractors are. Downstream, recognition_lower_bound_certificate packages the fact directly, and the substrate dichotomy restates it as the Branch A obstruction: a definite ledger that reads only Archimedean magnitude cannot extract a factor coordinate and is therefore blind to the factor chart.
In the Recognition framework this pins a foundational non-claim about what pure magnitude can see. It supports the dichotomy between definite-ledger substrates (magnitude-blind to factors) and coherent substrates that could deliver factor information. The companion right-factor non-magnitude-only result is symmetric; together they close the lower-bound side of the factorization story.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.