definiteLedger_magnitude_cannot_extract_factor
plain-language theorem explainer
On a definite ledger the only Archimedean readout of a factor pair is the product magnitude, and that readout cannot extract a left factor coordinate. Equal products need not share left factors, so the map is not magnitude-only. Cited by the substrate dichotomy certificate as the proved Branch A obstruction. Proof is a one-line restatement of the recognition lower bound.
Claim. The left-coordinate readout $(a,b)\mapsto \mathrm{toNat}(a)$ is not magnitude-only: it is not true that equal factor-pair products always yield equal values. Equivalently, a definite ledger that sees only Archimedean product magnitude cannot extract a factor chart coordinate.
background
In the Primitive Recognition Calculus factorization layer, a magnitude-only observable is any binary readout $F$ on distinction naturals that factors through the product orbit: whenever two pairs have the same factor-pair product, $F$ returns the same natural. The displayed product magnitude is the canonical example.
The candidate left-factor extractor is $(a,b)\mapsto \mathrm{toNat}(a)$, reading the iteration count of the left factor alone. The recognition lower bound already shows this map fails magnitude-only status, via the classical counterexample $2\cdot 6=3\cdot 4$ with unequal left coordinates.
This module packages the substrate dichotomy: Branch A (definite ledger, magnitude-only) versus Branch B (coherent substrate delivering a certified factor readout). The present theorem is the Branch A obstruction restated for the dichotomy certificate.
proof idea
One-line term wrapper: the claim is definitionally identical to leftFactorObservable_not_magnitudeOnly from RecognitionLowerBound, so the proof is just that theorem name. Upstream, the lower bound introduces the magnitude-only hypothesis, instantiates it on the pairs $(2,6)$ and $(3,4)$ (equal products), and obtains $2=3$ after simplification, a contradiction.
why it matters
Fills the proved half of the honest substrate dichotomy. Downstream, substrate_dichotomy_certificate installs this statement as branchA_obstruction, while Branch B is only the conditional: if a coherent substrate delivers a certified factor readout, then $N$ factors nontrivially. The Branch B antecedent itself remains the open foundational node (Door B oracle); a uniform speedup below classical factoring is a still stronger open performance claim.
In framework terms this seals that a definite, Archimedean ledger is blind to the factor chart: factorization, if it is to be native, must come from coherent structure beyond product magnitude. It does not itself invoke T5–T8 or the RCL, but it sits in the foundation layer that those forcing steps presuppose when reading physical periods off the ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.