zero_ne_one
plain-language theorem explainer
In the primitive recognition calculus, the rational zero and unit classes are unequal. Field-structure certificates, hierarchy obstruction arguments, and sphere-pole nontriviality all cite this fact. The proof is a two-line rewrite: transport the choice-free zero discriminator along the assumed equality and contradict the unit case.
Claim. In the PRC rational quotient (ratio-orbit classes with nonzero denominators, identified by cross-multiplication), the additive identity is distinct from the multiplicative unit: $0 \neq 1$.
background
PRC rationals are the quotient of ratio orbits by the cross-multiplication setoid: two displays represent the same class when their orbit-level numerators and denominators cross-agree. Zero and one are the classes of the zero and unit ratio orbits built from signed orbits and distinction naturals.
The local setting is K4.8 of the primitive recognition calculus: arithmetic on these classes must be choice-free and must not lean on a classical $\mathbb{Q}$ display. The predicate isZero is the structural discriminator: it holds exactly when the underlying signed orbit is balanced against the zero orbit.
Upstream, isZero holds of the zero class by reflexivity of balance, and fails of the unit class because the integer images of the unit and zero signed orbits are $1$ and $0$, which are unequal.
proof idea
Assume for contradiction that the zero class equals the unit class. Rewrite the fact that zero is zero along that equality to conclude that the unit class is zero. That directly contradicts the upstream lemma that the unit is not zero. The argument never opens the quotient or displays into classical rationals; it only uses the discriminator and substitution.
why it matters
Structural nontriviality $0 \neq 1$ is the missing field axiom that classical constructions take for granted. Downstream, the rational field certificate packages it with the additive and multiplicative laws so PRC rationals form a field. The same fact is invoked when proving no injective map $\mathbb{R} \to \mathrm{Bool}$ (hierarchy realization obstruction), when separating north and south poles on singular spheres, in the unknot-complement core embedding, and in linear independence of discrete Lichnerowicz polarizations. It closes K4.8 without classical $\mathbb{Q}$, keeping the forcing chain's arithmetic layer choice-free.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.