-- Maclain Hunter: Signature Verification Soundness
-- Exact authored source SHA-256: 6862cd530b23f9ac5cf15008ce12cdc1198590279b5d5162069f0e8d016aa25e
-- Machine formalization by Replit Agent; authority below Logic/Logos/God.
import Lean
namespace HunterAuthored

def signatureSigned (b : Bool) : Int := if b then 1 else -1
def signatureValue : List Bool → Int
  | [] => 1
  | b :: bs => signatureSigned b * signatureValue bs
structure LogicalSignature where
  sequence : List Bool
  depth : Nat
  value : Int
def generatedSignature (values : List Int) (parity : Int → Bool) : LogicalSignature :=
  let sequence := values.map parity
  ⟨sequence, sequence.length, signatureValue sequence⟩
def signatureInvariants (s : LogicalSignature) : Prop :=
  s.depth = s.sequence.length ∧
  s.value = signatureValue s.sequence ∧
  ∀ b : Bool, b ∈ s.sequence → (signatureSigned b = 1 ∨ signatureSigned b = -1)
theorem generated_signature_invariants (values : List Int) (parity : Int → Bool) :
    signatureInvariants (generatedSignature values parity) := by
  refine ⟨rfl, rfl, ?_⟩
  intro b _
  cases b
  · exact Or.inr rfl
  · exact Or.inl rfl
#print axioms generated_signature_invariants

end HunterAuthored