-- Maclain Hunter: Exponent Multiplication Parity
-- Exact authored source SHA-256: 84fe5492d3f527cd1c959228d59ea71762363696064d4226925d2756b3dc8b67
-- Machine formalization by Replit Agent; authority below Logic/Logos/God.
import Lean
namespace HunterAuthored

def parityPower (n : Int) : Int := if n % 2 = 0 then 1 else -1
theorem parity_power_multiplication (a b : Int) :
    parityPower a * parityPower b = parityPower (a + b) := by
  unfold parityPower
  have ra : a % 2 = 0 ∨ a % 2 = 1 := by omega
  have rb : b % 2 = 0 ∨ b % 2 = 1 := by omega
  rcases ra with ha | ha <;> rcases rb with hb | hb
  · have hc : (a + b) % 2 = 0 := by omega
    rw [if_pos ha, if_pos hb, if_pos hc]; rfl
  · have hc : (a + b) % 2 ≠ 0 := by omega
    have hn : b % 2 ≠ 0 := by omega
    rw [if_pos ha, if_neg hn, if_neg hc]; rfl
  · have hc : (a + b) % 2 ≠ 0 := by omega
    have hn : a % 2 ≠ 0 := by omega
    rw [if_neg hn, if_pos hb, if_neg hc]; rfl
  · have hc : (a + b) % 2 = 0 := by omega
    have hn : a % 2 ≠ 0 := by omega
    have hm : b % 2 ≠ 0 := by omega
    rw [if_neg hn, if_neg hm, if_pos hc]; rfl
#print axioms parity_power_multiplication

end HunterAuthored