productMagnitudeObservable_magnitudeOnly
plain-language theorem explainer
Equal factor-pair products yield equal displayed archimedean magnitudes, so the product-magnitude map is magnitude-only. Anyone building the recognition lower-bound certificate or closing postprocess invariance cites this. The proof is a one-line unfold plus the chart-transition lemma that same product implies same magnitude.
Claim. The observable $F(a,b)=\mathrm{archimedeanMagnitude}(\mathrm{product}(a,b))$ is magnitude-only: for all distinction pairs $(a,b)$ and $(c,d)$, if $\mathrm{product}(a,b)=\mathrm{product}(c,d)$ then $F(a,b)=F(c,d)$.
background
In the primitive recognition calculus, factor pairs of distinction naturals sit on product orbits. A magnitude-only observable is any map $F$ on pairs that is constant on those orbits: equal products force equal $F$-values. The displayed product magnitude is the archimedean magnitude of the factor-pair product; it is the cheap chart reading of orbit position.
The upstream chart-transition fact states that equal products give equal displayed magnitudes ("Same product means same displayed magnitude. This is the cheap chart."). The present claim simply packages that fact as the magnitude-only property for this particular observable, which is the baseline positive case before one shows that left- and right-factor extractors fail the same test.
proof idea
Term-mode proof. Introduce four distinction naturals and the hypothesis that their factor-pair products agree. Unfold the product-magnitude observable to archimedean magnitude of the product, then apply same_product_same_magnitude to that equality. No further rewriting is needed.
why it matters
This is the positive half of the recognition lower-bound story in the factorization module: product magnitude is magnitude-only, while left- and right-factor extractors are not. Downstream, recognition_lower_bound_certificate installs the claim as the field product_magnitude_is_magnitude_only, and productMagnitudePostprocess_magnitudeOnly reuses it to show that any postprocess of the product magnitude remains magnitude-only.
In the broader Recognition Science foundation, the result supports the claim that only orbit-level (product) data is freely readable without extra structure, which is the lower-bound side of the factorization/recognition calculus. It does not itself invoke the forcing chain T0–T8, but it sits under the primitive recognition layer those landmarks rest on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.