six_ne_four
plain-language theorem explainer
Orbit positions built from the naturals 6 and 4 are unequal in DistinctionNat. Factorization and chart-transition arguments cite it to separate right factors when products agree. The proof is a short congruence: push equality through toNat and reduce to ordinary 6 ≠ 4.
Claim. The base-neutral distinction-orbit positions corresponding to the verifier naturals $6$ and $4$ are distinct.
background
DistinctionNat is the inductive, base-neutral finite orbit of repeated distinction (zero and successor), the K2.12 carrier used throughout PrimitiveRecognitionCalculus. The maps ofNat and toNat are mutually inverse bridges between Lean Nat and that orbit: ofNat builds an orbit position from a verifier natural; toNat reads the iteration count back out.
This module studies factorization of orbit data under an Archimedean magnitude chart. Sibling facts record that the factor pairs (2,6) and (3,4) share the same product (hence the same magnitude), so magnitude alone cannot name either factor. The present inequality is the right-factor half of that ambiguity witness.
Upstream, ArithmeticFromLogic.toNat plays the same iteration-count role on LogicNat; here only DistinctionNat.toNat is needed.
proof idea
Term-mode by contradiction. Assume ofNat 6 = ofNat 4. Apply congrArg of DistinctionNat.toNat to obtain equality of the underlying Nats. simp then reduces both sides (toNat ∘ ofNat is the identity on these numerals) to the false statement 6 = 4, closing the goal.
why it matters
Feeds magnitude_underdetermines_right_factor, which packages the product identity two_six_product_eq_three_four with this inequality to show that equal magnitude does not determine the right factor. That pair is then installed as explicit_ambiguous_product inside chart_transition_certificate, the module's certificate that chart transitions must carry more than magnitude data.
In the Recognition foundation this is a small but load-bearing discreteness fact: orbit positions are rigid under toNat, so distinct rungs stay distinct when factorization is read in the Archimedean chart. It does not itself invoke J-cost, phi, or the forcing chain; it only secures the combinatorial side of chart ambiguity used later in PrimitiveRecognitionCalculus factorization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.