CoherentSubstrateDeliversFactor
plain-language theorem explainer
Branch B antecedent: for nonzero distinction orbit N, the substrate supplies some base a with a certified factor readout (a proper divisor certified by period data). Foundation workers cite it as the open Door B oracle in the substrate dichotomy. Pure Prop definition: existential over CertifiedFactorReadout; no proof content.
Claim. For a nonzero finite distinction orbit $N$, there exists a base $a$ such that a certified factor readout of $N$ at $a$ is inhabited: the substrate exposes a proper divisor of $N$ certified by period data.
background
In the Primitive Recognition Calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction (inductive zero/succ). Factorization is phrased relative to this orbit type rather than classical ℕ.
A certified factor readout is stronger than a bare period readout: it packages an exponent together with a proper-divisor witness extracted from period data. That structure is the minimal Lean-facing interface a physical period-finder must satisfy.
This module sets up an honest substrate dichotomy for factorization. Branch A is the obstruction that a definite ledger reading only Archimedean magnitude cannot extract a factor coordinate. Branch B is the conditional that a coherent substrate delivering a certified readout forces nontrivial factorization. The present definition is exactly the Branch B antecedent (Door B oracle); the module docstring stresses it is not proved for the RS substrate.
proof idea
Definitional abbreviation, not a theorem. The Prop is the existential statement that some base a : DistinctionNat makes CertifiedFactorReadout N hN a nonempty. No tactics or lemmas; the body is the interface type itself.
why it matters
This is the open foundational node of the substrate dichotomy. Downstream, coherentSubstrate_delivers_factorization is the proved Branch B conditional: if this antecedent holds, then N admits a nontrivial factorization (via certifiedFactorReadout_to_nontrivialFactorization). The same Prop appears in SubstrateDichotomyCertificate, which packages both proved conditionals without asserting the antecedent.
A factoring speedup would require delivering this antecedent uniformly in N below classical cost; that performance claim remains open. The definition therefore separates the unconditional reduction (proved) from the physical delivery question (unproved), keeping the certificate honest.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.