ChartTransitionCertificate
plain-language theorem explainer
Packages the chart-transition obstruction: the positional chart sees only products, so distinct factor pairs can share the same Archimedean magnitude. The certificate records product-to-Nat fidelity, magnitude invariance under equal products, the explicit 2·6 = 3·4 ambiguity with unequal factors, and the link from proper divisors to nontrivial factorizations. Downstream master certificates cite it as the chart-transition lane. As a Prop structure it is discharged by assembling named lemmas, not by a single proof term.
Claim. A proposition bundling six facts on finite distinction orbits: (i) the product chart satisfies $(a\cdot b)_{\mathbb{N}}=a_{\mathbb{N}}\cdot b_{\mathbb{N}}$; (ii) equal products yield equal Archimedean magnitudes; (iii) the pairs $(2,6)$ and $(3,4)$ display the same product; (iv)--(v) those pairs differ in both left and right factors; (vi) every proper non-unit divisor of a nonzero orbit yields a nontrivial factorization.
background
In the primitive recognition calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction (zero and successor). Positions convert to ordinary naturals by iteration count (toNat / ofNat). Multiplication of orbits is the factor-pair product; the positional chart records only that product, not the ordered factors.
Archimedean magnitude is just the displayed toNat of an orbit position. Consequently any two factor pairs with the same product are indistinguishable on the cheap chart: same product implies same magnitude. The classical numerical identity $2\cdot 6=3\cdot 4$ lifts to an explicit orbit-level collision with unequal left and right factors.
The module sits in the factorization lane of the foundation stack (imports orbit Euclidean structure). The certificate is the obstruction surface for chart transition: magnitude alone underdetermines factorization.
proof idea
This is a Prop-valued structure, not a proved theorem. Each field is a named hypothesis shape to be filled by an instance. The companion theorem chart_transition_certificate supplies the instance: product display from factorPairProduct_toNat; magnitude invariance by applying the one-line same_product_same_magnitude; the ambiguous product from two_six_product_eq_three_four; factor inequalities from two_ne_three and six_ne_four; and the divisor-to-factorization arrow from nontrivialFactorization_of_proper_divisor. No new algebra is done at the structure itself.
why it matters
The structure is the chart-transition entry in the factorization character-theory ledger. DeltaFactorizationCharacterTheoryCertificate requires a field chart_transition : ChartTransitionCertificate, so every master certificate for that lane must discharge this bundle. The companion chart_transition_certificate is the concrete witness.
In Recognition terms this is the obstruction that forces a richer chart than pure Archimedean magnitude when reading factorization off distinction orbits. It does not itself invoke the forcing chain (T5--T8), RCL, or the mass ladder; it is pure foundation arithmetic that later character-theory and period-spectrum certificates sit on. Closing the master ledger depends on this surface being inhabited.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.