CertifiedFactorReadout
plain-language theorem explainer
A certified factor readout packages an exponent together with a proper-divisor witness extracted from period data for a nonzero distinction integer N and base a. Anyone building a physical period-finder or substrate oracle cites this as the minimal Lean interface that already exposes a factor, not merely a period. It is a plain structure definition, not a proved theorem.
Claim. For a nonzero distinction integer $N$ and base $a$, a certified factor readout consists of an exponent $r$ together with a proper-divisor-from-period witness for $(N,a,r)$: a period certificate plus a nonzero non-unit divisor of $N$.
background
Distinction integers are the base-neutral finite orbits of repeated distinction (K2.12): an inductive type with zero and successor, used throughout the primitive recognition calculus in place of ordinary naturals.
A proper-divisor-from-period witness stores both a period certificate for base $a$ modulo $N$ at exponent $r$ and an explicit nonzero non-unit divisor of $N$. The divisor may arise from a classical route such as $\gcd(a^{r/2}-1,N)$, but the structure keeps the certificate rather than treating the readout as already derived.
This module sits in the factorization layer of the primitive recognition calculus. It separates what a physical period-finder must hand back from the pure arithmetic reduction that turns that handoff into a nontrivial factorization of $N$.
proof idea
No proof body: this is a structure definition. It records two fields, an exponent of type distinction integer and a factor witness of type proper-divisor-from-period for that same exponent. Downstream theorems project the witness and apply the existing period-to-factorization reduction.
why it matters
This is the minimal Lean-facing interface a physical period-finder must satisfy: stronger than a bare period readout because it already exposes a proper divisor certified by the period data.
It feeds the one-line reduction that turns any such readout into a nontrivial factorization of $N$, and it is the payload type inside the physical period-readout certificate (the device or substrate must supply the certificate; the interface separates certification from the factorization theorem).
In the substrate dichotomy it is exactly the Door B oracle antecedent: a coherent substrate delivers a factor when there exists some base $a$ with a nonempty certified factor readout for $N$. That reduction is unconditional; only the antecedent is open. A factoring speedup would require delivering the antecedent uniformly in $N$ below classical cost, which remains an open performance question, not a proved RS claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.