chart_transition_certificate
plain-language theorem explainer
Assembles a single certificate for the chart-transition obstruction: product display equals ordinary multiplication, equal products share Archimedean magnitude, the pairs (2,6) and (3,4) witness an ambiguous product with distinct factors, and every proper non-unit divisor yields a nontrivial factorization. Downstream character-theory master certificates cite it as the chart-transition leg. The proof is a structure instance that wires six already-proved lemmas.
Claim. There is a chart-transition certificate asserting: (i) for distinction naturals $a,b$, the displayed product equals $a\cdot b$ on underlying naturals; (ii) equal factor-pair products have equal Archimedean magnitudes; (iii) the pairs $(2,6)$ and $(3,4)$ realize the same product while left factors $2\neq 3$ and right factors $6\neq 4$; (iv) every proper non-unit divisor of a nonzero distinction natural supplies a nontrivial factorization.
background
In the Primitive Recognition Calculus factorization layer, distinction naturals carry a native product and an Archimedean magnitude (the cheap displayed chart). A factor pair is a pair of distinction naturals; its product is again a distinction natural whose underlying natural is the ordinary product.
The chart-transition obstruction surface records that magnitude alone cannot recover factors: distinct pairs can share a product (hence a magnitude) while differing on both sides. The certificate structure packages the display law, the magnitude-invariance of equal products, an explicit ambiguous product $2\cdot 6=3\cdot 4$, the two factor inequalities, and the reusable bridge from proper non-unit divisors to nontrivial factorizations (the endpoint used by period-readout factoring once a gcd witness appears).
Upstream lemmas already prove each field separately: product display via unfolding the factor-pair product, magnitude equality by rewriting after unfolding the magnitude, the numeric inequalities by transport to toNat, and the divisor-to-factorization map as the native nontrivial factorization constructor.
proof idea
The proof is a structure instance for the certificate Prop. Each field is filled by an existing lemma:
- product display is the theorem that the factor-pair product's underlying natural is ordinary multiplication;
- same-product/same-magnitude is introduced and discharged by the corresponding magnitude-invariance lemma;
- the explicit ambiguous product is the equality $2\cdot 6=3\cdot 4$;
- left and right factor differences are the inequalities $2\neq 3$ and $6\neq 4$;
- proper-divisor-to-nontrivial-factorization is introduced on the five hypotheses (nonzero host, nonzero divisor, non-unit, proper, divides) and closed by the reusable divisor factorization lemma.
No new arithmetic is performed; the certificate only packages prior results.
why it matters
The declaration is the chart-transition leg of the δ-factorization character-theory master certificate, which bundles chart transition, residue orbit, unit group, and period spectrum into one character-theory package. That master certificate is the consolidation point for factorization obstruction surfaces inside Primitive Recognition Calculus.
In the Recognition framework this surface separates the cheap Archimedean chart (magnitude of the product) from the fine factorization data needed for period readout and δ-divisibility. Once a period witness supplies a proper gcd divisor, the packaged divisor-to-factorization map hands a native nontrivial factorization without leaving the distinction-natural layer. The explicit $2\times 6=3\times 4$ witness is the concrete obstruction showing magnitude underdetermines both left and right factors, so any later uniqueness or reconstruction claim must carry extra structure beyond the Archimedean chart.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.