substrate_dichotomy_certificate
plain-language theorem explainer
Packages the honest substrate dichotomy: a definite-ledger magnitude readout cannot extract a factor coordinate, while any coherent substrate that delivers a certified factor readout forces nontrivial factorization of nonzero N. The open antecedent (coherent delivery) is not asserted. Factorization character-theory work cites this certificate. Term proof that fills the two certificate fields from prior lemmas.
Claim. There is a substrate dichotomy certificate: (B) for every nonzero distinction-natural $N$, if a coherent substrate delivers a certified factor readout for $N$, then $N$ admits a nontrivial factorization; and (A) the definite-ledger product-magnitude observable $a \mapsto a.{\rm toNat}$ is not a magnitude-only left-factor observable.
background
In the Primitive Recognition Calculus factorization layer, integers are read as distinction-naturals. Two substrate regimes are compared. A definite ledger that only sees Archimedean product magnitude is blind to factor coordinates: the observable sending a pair to the first factor's natural value is not magnitude-only. That is the Branch A obstruction, already proved from the recognition lower bound.
Branch B is conditional. The antecedent CoherentSubstrateDeliversFactor means the substrate supplies a certified factor readout for nonzero $N$. The reduction from that antecedent to nontrivial factorization is unconditional and already proved by unpacking the readout and applying the certified-readout-to-factorization map. The antecedent itself remains the open foundational node and is not claimed here.
The local module packages both proved legs into a single Prop-valued certificate structure so downstream master certificates can cite the dichotomy without smuggling the open hypothesis.
proof idea
Term-mode inhabitant of the certificate structure. The Branch B field is discharged by introducing $N$, nonzero-ness, and the coherent-delivery hypothesis, then applying coherentSubstrate_delivers_factorization (which itself unpacks the certified readout and calls the readout-to-nontrivial-factorization lemma). The Branch A field is filled by direct reference to definiteLedger_magnitude_cannot_extract_factor, the restated magnitude-only obstruction. No new arithmetic is done; the proof only assembles the two prior theorems into the certificate record.
why it matters
Gives the factorization stack an honest dichotomy object: both legs are theorems, yet the coherent-substrate delivery hypothesis stays explicitly open. Downstream, delta_factorization_character_theory_certificate in the MasterCertificate module consumes this packaging as part of the character-theory certificate bundle (alongside chart transition, residue orbit, unit group, and period spectrum). That keeps the master claim from overstating what is closed versus what still hangs on the open foundational node. In Recognition terms this sits under the primitive recognition calculus that feeds later forcing and readout structure; it does not itself invoke T5–T8 or the RCL, but it polices what a ledger can and cannot see when reading factors.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.