RecognitionLowerBoundCertificate
plain-language theorem explainer
Door A certificate: product magnitude is a genuine magnitude-only invariant of factor pairs, while extracting either coordinate is not, even after arbitrary scalar post-processing of that magnitude. Factorization and character-theory lanes cite it to separate orbit-position data from residue or character data. It is a Prop structure whose six fields are the constituent claims; the companion theorem supplies the proofs.
Claim. A recognition lower-bound certificate is the conjunction of: (i) the product-magnitude map is magnitude-only (invariant under equal product orbit positions); (ii)--(iii) the left and right coordinate maps $a \mapsto |a|$ and $b \mapsto |b|$ are not magnitude-only; (iv) every scalar post-process $\varphi$ of product magnitude remains magnitude-only; (v)--(vi) no such $\varphi$ recovers the left or right factor for all pairs on the distinction orbit.
background
In the Primitive Recognition Calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction (K2.12); toNat reads the iteration count as a verifier natural. Factor pairs live on this orbit. Their product carries an archimedean magnitude, written as the product-magnitude observable.
A magnitude-only observable is any two-argument map $F$ that factors through product orbit position: equal factorPairProduct implies equal $F$. The displayed product magnitude is such an $F$. Any scalar post-process $\varphi:\mathbb{N}\to\mathbb{N}$ applied to it remains magnitude-only. Coordinate extraction (left or right toNat) is not: equal products need not share a factor.
The module sits in the factorization lane of the foundation stack. Its job is to separate pure magnitude invariants from operations that require residue or finite multiplicative character data.
proof idea
This declaration is a structure definition bundling a Prop, not a proved theorem. It names six fields that any inhabitant must supply: magnitude-only status of the product observable and of every scalar post-process; failure of magnitude-only status for the left and right factor projections; and non-existence of any post-process that recovers either factor pointwise on all distinction-orbit pairs. The companion theorem recognition_lower_bound_certificate fills those fields from the sibling lemmas (productMagnitudeObservable_magnitudeOnly, leftFactorObservable_not_magnitudeOnly, rightFactorObservable_not_magnitudeOnly, and the corresponding post-process lemmas).
why it matters
Door A of the factorization lower-bound argument: product magnitude is a real invariant, but coordinate extraction is not a magnitude-only operation. Downstream, recognition_lower_bound_certificate constructs an inhabitant, and the master ledger DeltaFactorizationCharacterTheoryCertificate sits on the factorization character-theory lane this bound supports (chart transition, residue orbit, unit group, period spectrum, finite mul character).
In Recognition Science terms, the split keeps J-cost-style magnitude scores, which factor through product orbit position, from smuggling factor coordinates without residue or character data. That separation is what forces the character-theory certificates to carry the rest of factorization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.