def GraphNonIsoIP.ISO_bar {Γ : Type} (enc : Probabilistic.GraphPairEncoding Γ) : Set (List Γ)

The graph non-isomorphism language \overline{ISO}: the complement of ISO = { ⟨G, H⟩ | G and H are isomorphic graphs } under a fixed encoding of graph pairs. Membership ⟨G, H⟩ ∈ ISO_bar says that the two graphs are not isomorphic.

structure GraphNonIsoIP.GraphPermuter (Γ : Type) (enc : Probabilistic.GraphPairEncoding Γ) : Type

A GraphPermuter packages the random-permutation oracle used by the honest prover in the IP protocol for graph non-isomorphism.

• challenge w b seed returns the verifier's challenge graph obtained by randomly permuting either graph (b = false) or the other (b = true).
• iso_challenge_eq says that if the input pair w is isomorphic then the two challenge distributions coincide: the prover cannot distinguish.
• identify msg reads a challenge back and reports which of the two graphs it came from.
• identify_correct says that if the input pair w is not isomorphic then identify recovers the bit b that the verifier used.

• challenge : List Γ → Bool → List Γ → List Γ
• iso_challenge_eq (w : List Γ) : w ∈ Probabilistic.ISO enc → ∀ (seed : List Γ), self.challenge w true seed = self.challenge w false seed
• identify : List Γ → List Γ → Bool
• identify_correct (w : List Γ) : w ∉ Probabilistic.ISO enc → ∀ (b : Bool) (seed : List Γ), self.identify w (self.challenge w b seed) = b

noncomputable def GraphNonIsoIP.defaultGraphPermuter {Γ : Type} [Inhabited Γ] (enc : Probabilistic.GraphPairEncoding Γ) : GraphPermuter Γ enc

A toy default implementation of GraphPermuter used to show that the structure is inhabited.

It does not implement an actual graph permutation; instead it produces length-distinguishable outputs whenever the input pair is not isomorphic (satisfying identify_correct) and a single constant output whenever the input is isomorphic (satisfying iso_challenge_eq). It suffices for proving ISO_bar ∈ IP.

theorem GraphNonIsoIP.coin_match_le_one (g1 g2 : Bool) : {coins : Fin 2 → Bool | (g1 == coins ⟨0, ⋯⟩ && g2 == coins ⟨1, ⋯⟩) = true}.card ≤ 1

For fixed guesses g1, g2 : Bool, at most one of the four coin assignments coins : Fin 2 → Bool matches both guesses simultaneously.

This bounds the cheating probability of a dishonest prover in the graph non-isomorphism IP protocol by 1 / 4 ≤ 1 / 3.

def GraphNonIsoIP.isoBarVerifier {Γ : Type} [DecidableEq Γ] {enc : Probabilistic.GraphPairEncoding Γ} (perm : GraphPermuter Γ enc) : InteractiveProofs.Verifier Bool Γ

The verifier in the graph non-isomorphism IP protocol.

Using two random coins, in two rounds it sends perm.challenge w bᵢ w for b₀, b₁ ∈ {true, false} and finally accepts iff the prover's responses correctly identify the bits, i.e. both coins ⟨0⟩ == guess1 and coins ⟨1⟩ == guess2 hold.

def GraphNonIsoIP.isoBarHonestProver {Γ : Type} [Inhabited Γ] {enc : Probabilistic.GraphPairEncoding Γ} (perm : GraphPermuter Γ enc) : InteractiveProofs.Prover Γ

The honest prover in the graph non-isomorphism IP protocol.

After each verifier challenge c it calls perm.identify input c and replies with a nonempty marker ([default]) if the bit is identified as true, and the empty list otherwise. By identify_correct, when w ∉ ISO enc (i.e. w ∈ ISO_bar enc) the honest prover always recovers the verifier's bits and the protocol accepts with probability 1.

theorem GraphNonIsoIP.iso_bar_in_IP {Γ : Type} [DecidableEq Γ] [Inhabited Γ] (enc : Probabilistic.GraphPairEncoding Γ) (perm : GraphPermuter Γ enc) : InteractiveProofs.InIP (ISO_bar enc)

Graph non-isomorphism is in IP (relative to a GraphPermuter oracle).

\overline{ISO} ∈ IP: there is an interactive proof system in which

• if w ∈ ISO_bar enc (graphs not isomorphic) the honest prover convinces the verifier with probability ≥ 2/3 (in fact 1 here);
• if w ∉ ISO_bar enc (graphs are isomorphic) any prover P' is accepted with probability ≤ 1/3 (in fact ≤ 1/4 here), because the prover's two guesses can match the verifier's two random coin flips for at most one of the four coin assignments.

theorem ISO_bar_in_IP {Γ : Type} [DecidableEq Γ] [Inhabited Γ] (enc : Probabilistic.GraphPairEncoding Γ) : InteractiveProofs.InIP (GraphNonIsoIP.ISO_bar enc)

Graph non-isomorphism is in IP: \overline{ISO} ∈ IP.

Top-level corollary specializing iso_bar_in_IP to the defaultGraphPermuter, giving an unconditional instance of the interactive-proof membership.