coherentSubstrate_delivers_factorization
plain-language theorem explainer
If a coherent substrate supplies a certified factor readout for a nonzero distinction orbit N, then N admits a nontrivial factorization into nonzero non-units. Factorization auditors and RS foundation readers cite this as the unconditional half of Branch B in the substrate dichotomy. The proof unpacks the existential antecedent and hands the readout certificate to the period-divisor reduction.
Claim. Let $N$ be a nonzero distinction orbit. If the substrate delivers a certified factor readout for some base modulo $N$ (the Branch B antecedent), then $N$ admits a nontrivial factorization: there exist nonzero, non-unit factors $a,b$ with $a\cdot b=N$.
background
Distinction orbits are the base-neutral finite orbits of repeated distinction (DistinctionNat): a Peano-style inductive type used as the native carrier for divisibility statements in the primitive recognition calculus. A nontrivial factorization of such an orbit is the existence of two nonzero, non-unit factors whose product recovers $N$.
The Branch B antecedent asserts that the substrate supplies a certified factor readout for some base modulo $N$. That is exactly the Door B oracle: an existential package of a base together with a nonempty certified readout. The module treats this antecedent as open for the RS substrate; only the implication from readout to factorization is claimed here.
Upstream, a certified factor readout already carries a period-divisor witness. The PhysicalPeriodReadout layer converts that witness into a native nontrivial factorization, so the present statement is the substrate-level packaging of that reduction.
proof idea
Term-mode, two steps. Destructure the Branch B hypothesis as an existential pair: a base $a$ together with a nonempty certified factor readout $r$. Apply certifiedFactorReadout_to_nontrivialFactorization to $r$, which itself is a one-line handoff to the period-divisor-to-factorization lemma on the readout's factor witness. No arithmetic is redone at this layer.
why it matters
This is the proved conditional arm of the substrate dichotomy. Downstream, substrate_dichotomy_certificate installs it as branchB_conditional, pairing it with the Branch A obstruction (definite-ledger magnitude cannot extract a factor coordinate). Together they certify the dichotomy: either the substrate is blind to factors (Archimedean magnitude only), or a certified readout forces a genuine factorization of $N$.
In the Recognition framework this sits in the primitive recognition calculus factorization stack, not in the T0–T8 forcing chain itself. The reduction is unconditional; what remains open is whether the RS substrate actually delivers the antecedent uniformly in $N$ at cost below classical factoring (the performance problem flagged in the antecedent's doc-comment). Closing that delivery question would turn Branch B from a conditional into a constructive factoring path.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.