productMagnitudePostprocess
plain-language theorem explainer
Scalar post-processing of the product magnitude of a factor pair is defined by applying any map φ : ℕ → ℕ to the archimedean product magnitude. Anyone proving that magnitude-only observables cannot recover factor coordinates cites this family. The body is a one-line composition of φ with the product-magnitude observable.
Claim. For any post-processing map $\varphi:\mathbb{N}\to\mathbb{N}$ and any pair of finite distinctions $a,b$, the post-processed product magnitude is $\varphi$ applied to the archimedean magnitude of the product of $a$ and $b$.
background
In the primitive recognition calculus, a DistinctionNat is the base-neutral finite orbit of repeated distinction (K2.12): an inductive natural built only from zero and successor. Factor pairs of such distinctions carry an archimedean product magnitude, packaged as the observable that sends $(a,b)$ to the magnitude of their product.
A magnitude-only observable is one that depends on factor pairs solely through that product magnitude: equal magnitudes force equal readings. The bare product-magnitude observable is already magnitude-only. The present definition closes that class under arbitrary scalar post-processing $\varphi:\mathbb{N}\to\mathbb{N}$, covering J-cost-style ratio or magnitude scores that do not couple to residue or character data.
The local module builds a recognition lower-bound certificate: product magnitude is a genuine invariant, yet extracting either factor coordinate is not a magnitude-only operation.
proof idea
One-line definitional wrapper: evaluate the product-magnitude observable on the pair, then apply the scalar map $\varphi$. No lemmas are invoked at the definition site; downstream proofs unfold this composition and reuse magnitude-only invariance of the underlying product magnitude.
why it matters
This family is the quantitative object against which the lower bound is stated. Downstream, productMagnitudePostprocess_magnitudeOnly shows every such post-process remains magnitude-only. The companion non-existence theorems then prove no choice of $\varphi$ can equal the left (resp. right) factor coordinate for all pairs.
Those facts feed the RecognitionLowerBoundCertificate structure (Door A): product magnitude is a real invariant, but coordinate extraction is not magnitude-only. In the Recognition framework this blocks any attempt to read factor data from pure J-cost or magnitude scores without residue or character coupling, tightening the factorization side of the primitive recognition calculus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.