SubstrateDichotomyCertificate
plain-language theorem explainer
Honest dichotomy certificate for factorization on distinction orbits: (B) if a coherent substrate supplies a certified factor readout for nonzero N, then N factors nontrivially; (A) the pure first-component magnitude map is not a magnitude-only factor-pair observable. Factorization-lane authors cite it to separate the open Door-B antecedent from what is already reduced. It is a Prop structure packaging two proved conditionals; the inhabited instance is built separately.
Claim. A substrate dichotomy certificate is a pair of propositions: (i) for every nonzero distinction-orbit position $N$, if the substrate delivers a certified factor readout for some base modulo $N$, then $N$ admits a nontrivial factorization into nonzero non-unit factors; (ii) the map $(a,b)\mapsto |a|$ (orbit length of the first argument) is not a magnitude-only observable of factor-pair products.
background
In the Primitive Recognition Calculus, distinction-orbit positions are the base-neutral finite orbit of repeated distinction (zero and successor). Native nontrivial factorization means $N=ab$ with both factors nonzero and non-unit.
A magnitude-only observable is any two-argument readout $F$ that factors through the product orbit: whenever the factor-pair products agree, $F$ agrees. Branch A blocks extracting factors from pure magnitude by showing the first-component length map fails the invariance needed for that route.
Branch B's antecedent is existence of some base with a certified factor readout (the Door B oracle). The module docstring and the field doc treat that antecedent as open for the RS substrate; only the implication from readout to nontrivial factorization is the proved conditional.
proof idea
Definitional Prop structure, not a proved theorem: zero proof body. It declares the two fields any honest dichotomy certificate must carry. Branch B is the conditional whose implication is discharged elsewhere by coherentSubstrate_delivers_factorization; Branch A is the obstruction proved as definiteLedger_magnitude_cannot_extract_factor. The inhabited instance is the sibling theorem substrate_dichotomy_certificate, which fills both fields by those lemmas.
why it matters
Local ledger entry for the substrate dichotomy in the factorization character-theory lane. Downstream, substrate_dichotomy_certificate inhabits it, and the master stack DeltaFactorizationCharacterTheoryCertificate aggregates the broader lane (chart transition, residue orbit, unit group, period spectrum, finite multiplicative character).
The design keeps the open foundational node explicit: Door B (coherent substrate delivers a certified factor) is not asserted here. A factoring speedup would require delivering that antecedent uniformly in $N$ below classical cost, which the sibling docs flag as the open performance problem. The certificate therefore separates what the calculus has reduced from what it has not claimed about the physical substrate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.