CertifiedPeriodReadout
plain-language theorem explainer
A certified period readout packages a nonzero exponent with a period witness that base a is a unit residue modulo N and that its orbit power returns to 1. Physical period-finders and factorization interfaces cite this as the minimal Lean-facing certificate type. It is a pure structure definition: two fields, no proof obligations beyond the witness Prop.
Claim. For a nonzero distinction number $N$ and base $a$, a certified period readout is a pair $(r, W)$ where $r$ is a distinction number and $W$ is a period witness: $r \neq 0$, $a$ is a unit residue modulo $N$, and the orbit power $a^r$ is the same residue as $1$ modulo $N$.
background
In the Primitive Recognition Calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction (an inductive copy of the naturals used for residue arithmetic without committing to a numeral base). Periods live in that orbit: raising a base by an exponent means iterating the distinction action.
A PeriodWitness (from PeriodSpectrum) is the essential certificate: a nonzero exponent $r$ such that $a$ is a unit residue modulo $N$ and orbitPow a r returns the unit residue $1$. Minimality of $r$ is optional at the interface; the witness only forces return-to-one.
This module sits in the factorization layer of PRC: physical period readout is the bridge from abstract orbit periods to the data a period-finder must expose before one can extract proper divisors.
proof idea
No proof. The declaration is a structure with two fields: an exponent of type DistinctionNat, and a witness inhabiting PeriodWitness N hN a exponent. Inhabiting the structure is exactly supplying those two components; the Prop constraints live inside the witness.
why it matters
This is the minimal Lean-facing interface a physical period-finder must satisfy in the PRC factorization stack. The sibling certified factor readout is strictly stronger: it exposes a proper divisor certified by the same period data. Downstream certificates such as PhysicalPeriodReadoutCertificate are meant to wrap this shape.
In the broader Recognition framework, period structure on distinction orbits feeds the eight-tick octave (T7) and the discrete spectrum that factorization and mass-ladder bookkeeping rely on. The type itself does not force phi or D=3; it only standardizes what counts as a certified period before those layers attach.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.