productMagnitudePostprocess_magnitudeOnly
plain-language theorem explainer
Any scalar function of the product magnitude remains a magnitude-only observable: equal products yield equal scores. Factorization and recognition-bound arguments cite this to rule out J-style or other post-processed magnitude scores as factor extractors. The proof unfolds the postprocess definition and rewrites by the raw product-magnitude case.
Claim. For every function $\varphi:\mathbb{N}\to\mathbb{N}$, the map $(a,b)\mapsto \varphi(|a\cdot b|)$ (scalar post-processing of product magnitude) is magnitude-only: whenever two distinction pairs have the same product orbit position, the post-processed scores agree.
background
In the primitive recognition calculus, a factor pair is a pair of distinction naturals, and the product orbit position records only the product magnitude. An observable $F$ on pairs is magnitude-only when equal products force equal values: $F$ cannot see which factorization produced the product.
The raw product-magnitude observable is already magnitude-only (via same-product-same-magnitude). The postprocess construction applies an arbitrary scalar $\varphi:\mathbb{N}\to\mathbb{N}$ to that magnitude, covering J-cost-style ratio or magnitude scores that ignore residue or character data.
The local module builds a recognition lower-bound certificate: magnitude-only data cannot recover left or right factor coordinates. This lemma is the closure step that keeps the whole postprocess family inside the magnitude-only class.
proof idea
Term-mode intro on four distinctions and the equal-product hypothesis. Unfold the postprocess definition so both sides become $\varphi$ of the raw product magnitude. Rewrite by productMagnitudeObservable_magnitudeOnly on the same hypothesis, which already equates the underlying magnitudes; applying $\varphi$ preserves equality.
why it matters
Feeds the two non-extraction theorems: no scalar postprocess of product magnitude equals the left factor coordinate on all pairs, and likewise for the right factor. Those, with the raw magnitude-only and factor-not-magnitude-only facts, assemble recognition_lower_bound_certificate.
In Recognition Science terms this blocks a common shortcut: treating J-cost or other magnitude scores as if they could split a product into factors without residue or character data. The lower bound forces genuine factorization structure (finite multiplicative character / residue) rather than pure magnitude postprocessing, consistent with the primitive recognition calculus before the forcing chain (T5 J-uniqueness, T6 $\phi$) is applied at the physics layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.