-- Maclain Hunter: MCB Decidability
-- Exact authored source SHA-256: d62a2a92c96cc26d04abb582b6443e4c54ad6e39c15684689418646741813d8d
-- Machine formalization by Replit Agent; authority below Logic/Logos/God.
import Lean
namespace HunterAuthored

def signedIntegerPower (n : Int) : Int := if n % 2 = 0 then 1 else -1
theorem integer_parity_range (n : Int) :
    signedIntegerPower n = 1 ∨ signedIntegerPower n = -1 := by
  unfold signedIntegerPower
  by_cases h : n % 2 = 0
  · rw [if_pos h]; exact Or.inl rfl
  · rw [if_neg h]; exact Or.inr rfl
#print axioms integer_parity_range

end HunterAuthored