physical_period_readout_certificate
plain-language theorem explainer
A physical period readout certificate asserts that any certified factor readout of a nonzero distinction natural yields a nontrivial factorization. Factorization workers assembling the master delta-factorization certificate cite it as the period-readout leg. The proof is a one-line wrapper that applies the already-proved certified-factor-to-factorization extraction lemma.
Claim. There is a physical period readout certificate: for every nonzero distinction natural $N$ and every $a$, any certified factor readout of $N$ at $a$ produces a nontrivial factorization of $N$.
background
In the Primitive Recognition Calculus factorization layer, distinction naturals are the discrete carriers on which period and factor structure is read. A certified factor readout packages a period-divisor witness that a physical device, algorithm, or substrate claims to have measured for nonzero $N$. Nontrivial factorization is the standard existence of a proper factor of $N$.
The local module separates certification of the period readout from the pure number-theoretic extraction of a factor. The structure PhysicalPeriodReadoutCertificate is exactly that interface Prop: its single field demands that every certified factor readout extract a nontrivial factorization. Upstream, the lemma that a certified factor readout already implies nontrivial factorization (via the period-divisor extraction) is already proved in this module.
The Recognition lower-bound import supplies the ambient factorization language; this certificate does not invent new arithmetic, only packages the extraction as a named interface object.
proof idea
Term-mode construction of the certificate structure. The single field is discharged by introducing $N$, $a$, the nonzero hypothesis, and the certified readout $r$, then applying the upstream lemma that converts a certified factor readout into a nontrivial factorization (itself a one-line appeal to the period-divisor extraction). No new arithmetic is proved here.
why it matters
This declaration is the period-readout leg of the factorization master certificate. Downstream, the delta-factorization character-theory certificate assembles chart transition, residue orbit, unit group, and period spectrum certificates; the present object is the packaged guarantee that a certified physical period readout already yields factorization, so the master bundle can treat period readout as a closed interface rather than an open arithmetic obligation.
In the Recognition foundation stack this sits under Primitive Recognition Calculus factorization: it keeps the physical or algorithmic supply of a period certificate cleanly separated from the pure extraction theorem, matching the module doc that the device must supply the certificate. It does not itself touch the T0–T8 forcing chain, RCL, or the phi ladder; it is infrastructure for the discrete factorization side of the calculus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.