MagnitudeOnlyObservable
plain-language theorem explainer
An observable on factor pairs is magnitude-only when equal products force equal readings. Lower-bound and substrate-dichotomy arguments cite this predicate to separate product-magnitude invariants from left/right coordinate extractors. The body is a pure universal quantification: same product orbit position implies same F-value.
Claim. Let $F$ map pairs of distinction-orbit positions to natural numbers. $F$ is magnitude-only if, for all pairs $(a,b)$ and $(c,d)$, equality of products $a\cdot b = c\cdot d$ implies $F(a,b)=F(c,d)$. Equivalently, $F$ factors through the product orbit position.
background
The local setting is the factorization layer of the primitive recognition calculus. Distinction positions are the base-neutral finite orbit DistinctionNat (K2.12): zero and successor, with no preferred radix. A factor pair is two such positions; the positional chart records only their product.
Upstream, factorPairProduct is defined as ordinary multiplication on that orbit: "The positional chart sees only the product of a pair." Archimedean magnitude of an orbit position is the displayed size of that product. Observables here are maps $F$ from pairs into Nat.
A magnitude-only observable is one that cannot distinguish two pairs once their products agree. It is blind to how the product splits into left and right factors, and sees only the product orbit position.
proof idea
Definition, not a proved theorem. The predicate is the Prop that for all distinction positions $a,b,c,d$, if the factor-pair products agree then $F(a,b)=F(c,d)$. No tactics or lemmas; downstream theorems discharge or refute instances by unfolding this quantifier and applying product-equality lemmas (e.g. $2\cdot 6=3\cdot 4$).
why it matters
This predicate is the hinge of Door A in the recognition lower bound. RecognitionLowerBoundCertificate packages three facts built on it: product magnitude is magnitude-only; left-factor extraction is not; right-factor extraction is not. Downstream, productMagnitudeObservable_magnitudeOnly and the postprocess variant prove the positive side; leftFactorObservable_not_magnitudeOnly and rightFactorObservable_not_magnitudeOnly prove the negative side by exhibiting distinct factorizations of one product.
In SubstrateDichotomy, the same obstruction is restated as Branch A: "the product-magnitude observable available to a definite-ledger substrate cannot extract a factor coordinate. A definite ledger that reads only Archimedean magnitude is blind to the factor chart." That feeds SubstrateDichotomyCertificate and isolates the open Branch B node (CoherentSubstrateDeliversFactor). Within the forcing chain this is foundation-level bookkeeping before T5–T8 physics constants: it fixes what a magnitude-only ledger can and cannot see.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.