-- Maclain Hunter: XOR Self-Inverse
-- Exact authored source SHA-256: 58ed7e9b6ca841f3d468ab5fa6085ba089acb15df13ea37f7fec47e3c9f87b2e
-- Machine formalization by Replit Agent; authority below Logic/Logos/God.
import Lean
namespace HunterAuthored

def evenNat : Nat → Bool
  | 0 => true
  | n + 1 => !(evenNat n)
theorem even_add (a b : Nat) : evenNat (a + b) = (evenNat a == evenNat b) := by
  induction b with
  | zero =>
    change evenNat a = (evenNat a == true)
    cases evenNat a <;> rfl
  | succ b ih =>
    calc
      evenNat (a + (b + 1)) = !(evenNat (a + b)) := rfl
      _ = !(evenNat a == evenNat b) := congrArg Bool.not ih
      _ = (evenNat a == !(evenNat b)) := by cases evenNat a <;> cases evenNat b <;> rfl
def exponentXorState (a b : Int) : Int :=
  if evenNat (a.natAbs + b.natAbs) then 1 else -1
theorem exponent_xor_self_positive (a : Int) : exponentXorState a a = 1 := by
  unfold exponentXorState
  rw [even_add]
  cases evenNat a.natAbs <;> rfl
#print axioms exponent_xor_self_positive

end HunterAuthored