-- Maclain Hunter: MCB Decidability
-- Exact authored source SHA-256: 9333dc350ef91ebc490ba0a42fcb28d574932b02b6e6c8e370b1a47ca8861da6
-- 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