PhysicalPeriodReadoutCertificate
plain-language theorem explainer
Certificate interface asserting that any certified factor readout of a nonzero distinction orbit yields a nontrivial factorization. Factorization-lane authors cite it to keep physical period-finding separate from pure arithmetic extraction. It is a one-field Prop structure; the companion theorem discharges the field by applying the extraction lemma from a certified readout to a native factorization.
Claim. Certificate property: for every nonzero distinction-orbit number $N$ and every orbit element $a$, if a certified factor readout of $N$ at $a$ exists (exposing a proper divisor witnessed by period data), then $N$ admits a nontrivial factorization, i.e. $N = ab$ with $a,b$ both nonzero and non-units.
background
In the Primitive Recognition Calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction (K2.12): an inductive copy of the naturals used as the native carrier for orbit arithmetic. A nontrivial factorization of such an $N$ means $N = ab$ with both factors nonzero and non-units.
A certified factor readout is stronger than a bare period readout. It packages an exponent together with a proper-divisor witness derived from period data, and is documented as the minimal Lean-facing interface a physical period-finder must satisfy. The module isolates that physical/device layer from the pure factorization theorem.
This certificate is the Prop-level contract for that separation: period certification may come from a device, algorithm, or substrate; the arithmetic consequence (nontrivial factorization) is what the ledger records.
proof idea
Definitional structure, not a proved theorem. It declares a single field: every certified factor readout of a nonzero $N$ implies a nontrivial factorization of $N$. No tactics run here. The companion theorem physical_period_readout_certificate inhabits the structure by introducing the readout and applying the sibling extraction lemma that turns a certified factor readout into a native nontrivial factorization.
why it matters
Keeps the factorization character-theory lane honest about where physics ends and arithmetic begins. Downstream, the master ledger DeltaFactorizationCharacterTheoryCertificate aggregates chart transition, residue orbit, unit group, period spectrum, and finite multiplicative character certificates; this interface is the physical-period leg that feeds that stack via the inhabited certificate theorem.
In Recognition Science terms it supports the orbit-divisibility side of the primitive recognition calculus: period data on distinction orbits must force genuine composite structure when a proper divisor is certified. It does not itself touch T5–T8 or the J-cost equation; it is infrastructure for reading factors off physical periods inside the foundation layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.