recognition_lower_bound_certificate
plain-language theorem explainer
Assembles the Door A lower-bound certificate: product magnitude is a magnitude-only invariant, left and right factor coordinates are not, and no scalar post-processing of product magnitude recovers either factor on all pairs. Downstream master certificates in factorization character theory cite it as the packed witness. The proof is pure structure assembly of six already-proved sibling lemmas.
Claim. The following hold simultaneously: (1) the product-magnitude map on factor pairs is magnitude-only (equal products yield equal values); (2) the left-factor coordinate $a \mapsto a$ and the right-factor coordinate $b \mapsto b$ are not magnitude-only; (3) for every $\varphi:\mathbb{N}\to\mathbb{N}$, the post-processed product magnitude $\varphi(|ab|)$ is still magnitude-only; (4) no such $\varphi$ equals the left factor on all pairs, and none equals the right factor on all pairs.
background
In the Primitive Recognition Calculus factorization layer, observables on pairs of distinction naturals are classified by whether they are magnitude-only: an observable $f$ is magnitude-only when $ab=cd$ forces $f(a,b)=f(c,d)$. The product-magnitude observable records only the product size; left- and right-factor extractors return the integer coordinates of each factor.
The sibling lemmas establish the elementary contrast. Same product implies same magnitude, so product magnitude (and any scalar post-process of it) is magnitude-only. By contrast, the pairs $(2,6)$ and $(3,4)$ share a product but differ in left (and right) coordinates, so pure factor extraction fails the magnitude-only test. A further diagonal argument shows no fixed $\varphi:\mathbb{N}\to\mathbb{N}$ can turn product magnitude into either coordinate for every pair.
The structure RecognitionLowerBoundCertificate packages exactly these six facts as the Door A certificate: product magnitude is a real invariant, but coordinate extraction is not a magnitude-only operation.
proof idea
Term-mode structure instance. Each field of the certificate is filled by the corresponding sibling theorem: product magnitude is magnitude-only via productMagnitudeObservable_magnitudeOnly; left and right extractors fail magnitude-only via the two *_not_magnitudeOnly lemmas (witnessed by the equal-product pairs $(2,6)$ and $(3,4)$); every post-process of product magnitude remains magnitude-only via productMagnitudePostprocess_magnitudeOnly; and neither left nor right coordinate is recoverable as any such post-process, via the two no_productMagnitudePostprocess_extracts_* non-existence theorems. No new reasoning occurs here beyond wiring those results into the structure.
why it matters
Door A is the recognition lower bound in the factorization story: knowing only the product size never yields the individual factors, even after arbitrary scalar post-processing. That separation is what forces genuine recognition structure beyond bare magnitude invariants.
The packed certificate is consumed by delta_factorization_character_theory_certificate in the MasterCertificate module, which aggregates chart-transition, residue-orbit, unit-group, and period-spectrum witnesses into the delta factorization character-theory bundle. In the broader Recognition Science foundation, this sits inside Primitive Recognition Calculus factorization and supports the claim that coordinate content is not magnitude-reducible, a prerequisite for character-theoretic and octave-period analyses that treat factors as independent recognition data rather than product shadows.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.