real_not_forced_from_distinction
plain-language theorem explainer
No countable certificate system can faithfully cover the real line: for any countable Cert and any map ℝ → Cert, the assignment fails faithfulness. Cited when contrasting what a distinction forces (countable Peano arithmetic, LogicNat) with what it does not force (ℝ). One-line restatement of the RealLineNonNativity non-certifiability theorem, placed beside the distinction-to-arithmetic bridge.
Claim. For every type $C$ of certificates with a countable enumeration, and every assignment $a : \mathbb{R} \to C$, the assignment is not faithful: it cannot certify the real line without collapsing distinctions that the continuum requires.
background
The module DistinctionToArithmetic is the named bridge on the distinction side of Universal Forcing. A distinction on a carrier $K$ is a binary predicate detecting whether two elements are distinguishable (the canonical case is inequality). From any such distinction the module builds a forced ArithmeticOf object whose carrier is LogicNat: the inductive type with constructors identity and step, the Peano naturals as forced by the Law of Logic, hence countable.
Separately, RealLineNonNativity develops the notion of a faithful certificate assignment on $\mathbb{R}$: a map from reals into a certificate type that would, if faithful, make the continuum natively certifiable from countable data. The upstream result real_not_faithfully_certifiable states that no such faithful assignment exists when the certificate type is countable.
This theorem restates that negative fact in the distinction-to-arithmetic module so the positive and negative halves sit together: distinction forces countable initial Peano arithmetic, and never forces $\mathbb{R}$.
proof idea
One-line term wrapper. The proof is exactly the application of PrimitiveRecognitionCalculus.RealLineNonNativity.real_not_faithfully_certifiable to the given assignment. No local algebra; the content lives upstream in RealLineNonNativity.
why it matters
Closes the honesty clause of the distinction-to-arithmetic bridge. The module supplies the named constructor from distinction data to an ArithmeticOf object, proves the carrier is LogicNat (hence countable), and proves canonicity of the forcing map between distinctions. This theorem is the matching negative: the continuum is not among the forced objects.
As the module doc puts it, "a distinction forces the countable initial Peano arithmetic (LogicNat), and the continuum is not forced from countable distinction certificates." The real line enters RS only through a completion or display interface, not from distinction alone. That boundary matters for the Universal Forcing program register (δ-native analysis / unification from distinction): forced arithmetic lands at LogicNat, never at $\mathbb{R}$. No downstream consumers yet; the declaration is a scope marker rather than a lemma in a longer chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.