certifiedFactorReadout_to_nontrivialFactorization
plain-language theorem explainer
A certified factor readout for nonzero distinction-natural N yields a nontrivial factorization of N. Anyone wiring a physical period-finder (device, algorithm, or substrate) into the δ-native factorization layer cites this bridge. The proof is a one-line projection: extract the proper-divisor witness and hand it to the period-spectrum factorization lemma.
Claim. Let $N$ be a nonzero distinction-natural and $a$ any distinction-natural. Given a certified factor readout of $N$ relative to base $a$ (an exponent together with a proper-divisor-from-period witness), $N$ admits a nontrivial factorization.
background
In the Primitive Recognition Calculus, distinction-naturals carry a δ-native divisibility layer. A proper divisor from a period readout is a divisor of $N$ that is neither zero nor a unit and is not equal to the modulus $N$ itself; such a witness is enough to produce a nontrivial factorization.
A certified factor readout is the minimal Lean-facing interface a physical period-finder must satisfy. It is stronger than a bare period readout: it packages an exponent together with a ProperDivisorFromPeriod certificate derived from that period data. The module separates period certification (supplied by device, algorithm, or substrate) from the pure factorization theorem that follows once the certificate exists.
Upstream, the period-spectrum lemma states that once a period readout has supplied a proper-divisor certificate, the δ-native divisibility layer gives a nontrivial factorization of $N$.
proof idea
One-line term proof. Project the certified factor readout to its factor_witness field (a ProperDivisorFromPeriod), then apply period_divisor_to_nontrivialFactorization. That upstream lemma in turn calls nontrivialFactorization_of_proper_divisor on the three side conditions (divisor nonzero, nonunit, not equal to the modulus).
why it matters
This is the extraction arrow from the physical readout interface into pure factorization. Downstream, physical_period_readout_certificate installs it as the field certified_factor_readout_extracts_factorization, packaging the whole interface as a certificate object. The substrate dichotomy theorem coherentSubstrate_delivers_factorization uses it for Branch B: if a coherent substrate delivers a certified factor readout, then $N$ factors nontrivially; the reduction is unconditional and only the antecedent remains open.
In the Recognition framework this sits in the foundation factorization stack that turns period structure (linked to the eight-tick octave and discrete orbit data) into arithmetic consequences. It does not itself force the existence of a readout; it only converts a supplied certificate into a factorization theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.