IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Orbit

   1/-
   2  PrimitiveRecognitionCalculus/Orbit.lean
   3
   4  Round-trip source:
   5    PRC_Kernel_Spec_20260526.html
   6
   7  Spec anchors:
   8    K2.12, R8, K4.5
   9
  10  Base-neutral arithmetic begins as the finite orbit of repeated δ. Lean's
  11  Nat is used here only as a verifier representation, and the equivalence is
  12  proved explicitly.
  13-/
  14
  15import Mathlib
  16import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Basic
  17
  18namespace IndisputableMonolith
  19namespace Foundation
  20namespace PrimitiveRecognitionCalculus
  21
  22/-- K2.12. The base-neutral finite orbit of repeated distinction. -/
  23inductive DistinctionNat where
  24  | zero
  25  | succ : DistinctionNat → DistinctionNat
  26  deriving DecidableEq, Repr
  27
  28namespace DistinctionNat
  29
  30/-- R8. Zero is not a successor. -/
  31theorem zero_ne_succ (n : DistinctionNat) :
  32    zero ≠ succ n := by
  33  intro h
  34  cases h
  35
  36/-- R8. Successor is injective. -/
  37theorem succ_injective :
  38    Function.Injective succ := by
  39  intro a b h
  40  cases h
  41  rfl
  42
  43/-- R8. Induction over the δ-orbit. -/
  44theorem induction {P : DistinctionNat → Prop}
  45    (hzero : P zero)
  46    (hsucc : ∀ n : DistinctionNat, P n → P (succ n)) :
  47    ∀ n : DistinctionNat, P n := by
  48  intro n
  49  induction n with
  50  | zero => exact hzero
  51  | succ n ih => exact hsucc n ih
  52
  53/-- Verifier representation of the orbit as Lean Nat. -/
  54def toNat : DistinctionNat → Nat
  55  | zero => 0
  56  | succ n => Nat.succ (toNat n)
  57
  58/-- Build an orbit position from a verifier Nat. -/
  59def ofNat : Nat → DistinctionNat
  60  | 0 => zero
  61  | Nat.succ n => succ (ofNat n)
  62
  63@[simp] theorem toNat_zero :
  64    toNat zero = 0 := by
  65  rfl
  66
  67@[simp] theorem toNat_succ (n : DistinctionNat) :
  68    toNat (succ n) = Nat.succ (toNat n) := by
  69  rfl
  70
  71@[simp] theorem ofNat_zero :
  72    ofNat 0 = zero := by
  73  rfl
  74
  75@[simp] theorem ofNat_succ (n : Nat) :
  76    ofNat (Nat.succ n) = succ (ofNat n) := by
  77  rfl
  78
  79/-- K4.5. Transport from Lean Nat to the δ-orbit and back is identity. -/
  80theorem toNat_ofNat (n : Nat) :
  81    toNat (ofNat n) = n := by
  82  induction n with
  83  | zero => rfl
  84  | succ n ih =>
  85      simp [ofNat, ih]
  86
  87/-- K4.5. Transport from the δ-orbit to Lean Nat and back is identity. -/
  88theorem ofNat_toNat (n : DistinctionNat) :
  89    ofNat (toNat n) = n := by
  90  induction n with
  91  | zero => rfl
  92  | succ n ih =>
  93      simp [toNat, ih]
  94
  95/-- K4.5. The δ-orbit is equivalent to Lean Nat as a verifier display. -/
  96def equivNat : DistinctionNat ≃ Nat where
  97  toFun := toNat
  98  invFun := ofNat
  99  left_inv := ofNat_toNat
 100  right_inv := toNat_ofNat
 101
 102end DistinctionNat
 103
 104end PrimitiveRecognitionCalculus
 105end Foundation
 106end IndisputableMonolith
 107