two_ne_three
plain-language theorem explainer
The orbit positions built from ordinary 2 and 3 are distinct as DistinctionNat values. Factorization and chart-transition arguments cite it to separate left factors that share the same product magnitude. The proof is a short term argument: transport equality along toNat and simplify to the false numeral equation 2 = 3.
Claim. The finite distinction-orbit positions obtained from the ordinary naturals $2$ and $3$ are unequal: $\mathrm{ofNat}(2) \neq \mathrm{ofNat}(3)$.
background
In the primitive recognition calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction: an inductive type with zero and successor, independent of any preferred radix. The maps ofNat and toNat are mutually inverse bridges between Lean Nat and that orbit: ofNat builds an orbit position by iterating successor, and toNat reads the iteration count back as a verifier natural.
The surrounding module studies factorization of orbit positions and chart transitions. A factor pair carries a product and an archimedean magnitude; the same magnitude can arise from distinct left (or right) factors. The elementary inequality of the positions for 2 and 3 is the discrete separation needed before one can exhibit an ambiguous product such as $2\cdot 6 = 3\cdot 4$.
proof idea
Assume ofNat 2 = ofNat 3. Apply congrArg DistinctionNat.toNat to transport the equality into verifier naturals, obtaining toNat (ofNat 2) = toNat (ofNat 3). Simplification reduces both sides via the recursive definitions of toNat and ofNat, yielding the false numeral equation $2 = 3$, which closes the proof by contradiction. No external lemmas beyond the definitions of the two maps are required.
why it matters
Downstream, magnitude_underdetermines_left_factor packages this inequality with the product identity two_six_product_eq_three_four to prove that equal factor-pair products need not share the same left factor. That pair of facts is then fed into chart_transition_certificate, which assembles the explicit ambiguous product into the chart-transition certificate structure (product display, same-product-same-magnitude, and the concrete $2\cdot 6 = 3\cdot 4$ witness).
In the Recognition foundation layer this is bookkeeping rather than a forcing-chain step: it guarantees that magnitude data alone cannot rigidify factorization charts, so transitions between charts remain nontrivial. It does not itself invoke J-cost, phi, or the eight-tick octave; it only supplies the discrete inequality those later geometric layers rely on when they treat factor charts as underdetermined by size.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.