productMagnitudeObservable
plain-language theorem explainer
The product magnitude observable returns the Archimedean size of the product of two distinction-orbit values. Factorization lower-bound arguments cite it as the canonical magnitude-only readout of a factor pair. The definition is a one-line composition of the positional product chart with the magnitude map to natural numbers.
Claim. For distinction-orbit values $a$ and $b$, the product magnitude observable is the natural number obtained by taking the Archimedean magnitude of their product: $\mathrm{mag}(a\cdot b)$.
background
DistinctionNat is the base-neutral finite orbit of repeated distinction (K2.12): an inductive copy of the naturals used as the carrier for primitive recognition calculus. On that carrier, the positional chart of a factor pair is the ordinary product $a\cdot b$; the chart is deliberately product-only and does not expose ordered factors.
Archimedean magnitude is the displayed size of an orbit position, implemented as the underlying natural number. The RecognitionLowerBound module studies which readouts of a factor pair can be recovered from magnitude data alone versus which require residue or character side-channels.
This definition packages the two maps into a single binary observable: product first, then magnitude. Downstream material treats that composite as the prototype magnitude-only score.
proof idea
Pure definitional composition, not a proof. Apply the factor-pair product chart to $(a,b)$, then apply Archimedean magnitude (conversion of the resulting DistinctionNat to Nat). No lemmas or tactics.
why it matters
This is the seed observable for Door A of the recognition lower bound. The sibling theorem productMagnitudeObservable_magnitudeOnly shows it is MagnitudeOnlyObservable: equal products yield equal scores. productMagnitudePostprocess lifts that to any scalar post-processing of the product magnitude, covering J-cost-style ratio or magnitude scores unless they couple to residue or character data.
RecognitionLowerBoundCertificate packages the contrast: product magnitude is a real magnitude-only invariant, while left- and right-factor extraction are not. That certificate is the local statement that coordinate factorization is not free once only product magnitude is displayed. In the broader RS forcing picture it supports the claim that recognition must carry more structure than a pure Archimedean size if factors are to be recovered.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.