Errorless average-case heuristics

This module exposes the exact errorless-heuristic semantics used in average-case complexity: globally sound yes/no/failure answers, polynomial runtime through a canonical FP output codec, and slice-wise failure probability over arbitrary finite uniform-seed ensembles. It also defines AvgPAt δ and the inverse-polynomial intersection AvgP for distributional problems.

@[simp]

theorem Complexity.HeuristicAnswer.decode?_encode (answer : HeuristicAnswer) : decode? answer.encode = some answer

Canonical heuristic answers round-trip through their binary codec.

theorem Complexity.HeuristicAnswer.encode_injective : Function.Injective encode

The canonical three-answer encoding is injective.

theorem Complexity.HeuristicAnswer.encode_length_le_one (answer : HeuristicAnswer) : answer.encode.length ≤ 1

Every canonical heuristic-answer code has length at most one.

@[simp]

theorem Complexity.HeuristicAnswer.complement_complement (answer : HeuristicAnswer) : answer.complement.complement = answer

Complementing an answer twice returns the original answer.

@[simp]

theorem Complexity.HeuristicAnswer.complement_eq_failure_iff (answer : HeuristicAnswer) : answer.complement = failure ↔ answer = failure

Complement preserves and reflects explicit failure.

theorem Complexity.HeuristicAnswer.CorrectFor.complement {answer : HeuristicAnswer} {truth : Prop} (hcorrect : answer.CorrectFor truth) : answer.complement.CorrectFor ¬truth

Complementing a sound answer gives a sound answer for the negated truth value.

theorem Complexity.HeuristicAlgorithm.IsErrorlessFor.complement {A : HeuristicAlgorithm} {L : Language} (herrorless : A.IsErrorlessFor L) : A.complement.IsErrorlessFor Lᶜ

Complementing a globally errorless heuristic yields an errorless heuristic for the complement language.

@[simp]

theorem Complexity.HeuristicAlgorithm.complement_apply_eq_failure_iff (A : HeuristicAlgorithm) (x : List Bool) : A.complement x = HeuristicAnswer.failure ↔ A x = HeuristicAnswer.failure

Complementing a heuristic preserves its failure event pointwise.

theorem Complexity.HeuristicAlgorithm.failureProbability_nonneg (D : FiniteEnsemble (List Bool)) (A : HeuristicAlgorithm) (n : ℕ) : 0 ≤ failureProbability D A n

Failure probability is nonnegative.

theorem Complexity.HeuristicAlgorithm.failureProbability_le_one (D : FiniteEnsemble (List Bool)) (A : HeuristicAlgorithm) (n : ℕ) : failureProbability D A n ≤ 1

Failure probability is at most one.

theorem Complexity.HeuristicAlgorithm.answerProbability_nonneg (D : FiniteEnsemble (List Bool)) (A : HeuristicAlgorithm) (answer : HeuristicAnswer) (n : ℕ) : 0 ≤ answerProbability D A answer n

Every answer probability is nonnegative.

theorem Complexity.HeuristicAlgorithm.answerProbability_le_one (D : FiniteEnsemble (List Bool)) (A : HeuristicAlgorithm) (answer : HeuristicAnswer) (n : ℕ) : answerProbability D A answer n ≤ 1

Every answer probability is at most one.

theorem Complexity.HeuristicAlgorithm.failureProbability_eq_answerProbability (D : FiniteEnsemble (List Bool)) (A : HeuristicAlgorithm) (n : ℕ) : failureProbability D A n = answerProbability D A HeuristicAnswer.failure n

Failure probability is the probability of the failure answer.

theorem Complexity.HeuristicAlgorithm.IsErrorlessFor.one_sub_languageProbability_sub_failure_le_reject {A : HeuristicAlgorithm} {L : Language} (herrorless : A.IsErrorlessFor L) (D : FiniteEnsemble (List Bool)) (n : ℕ) : 1 - D.languageProbability L n - failureProbability D A n ≤ answerProbability D A HeuristicAnswer.reject n

An errorless heuristic correctly rejects mass at least one minus the language mass and its failure mass.

@[simp]

theorem Complexity.HeuristicAlgorithm.failureProbability_complement (D : FiniteEnsemble (List Bool)) (A : HeuristicAlgorithm) (n : ℕ) : failureProbability D A.complement n = failureProbability D A n

Complementing a heuristic preserves its failure probability exactly.

theorem Complexity.HeuristicAlgorithm.FailsWithProbabilityAtMost.mono {D : FiniteEnsemble (List Bool)} {A : HeuristicAlgorithm} {δ ε : ℕ → ℚ} (hfailure : FailsWithProbabilityAtMost D A δ) (hδε : ∀ (n : ℕ), δ n ≤ ε n) : FailsWithProbabilityAtMost D A ε

A failure guarantee remains true under a pointwise weaker bound.

theorem Complexity.HeuristicAlgorithm.FailsWithProbabilityAtMost.complement {D : FiniteEnsemble (List Bool)} {A : HeuristicAlgorithm} {δ : ℕ → ℚ} (hfailure : FailsWithProbabilityAtMost D A δ) : FailsWithProbabilityAtMost D A.complement δ

Complementing a heuristic preserves every failure guarantee.

theorem Complexity.HeuristicAlgorithm.ofDecision_apply (decide : List Bool → Bool) (x : List Bool) : ofDecision decide x = if decide x = true then HeuristicAnswer.accept else HeuristicAnswer.reject

The decision-function adapter has its advertised pointwise semantics.

theorem Complexity.HeuristicAlgorithm.ofDecision_encoded (decide : List Bool → Bool) : (ofDecision decide).encoded = fun (x : List Bool) => [decide x]

The canonical encoding of a decision adapter is its singleton Boolean output.

theorem Complexity.HeuristicAlgorithm.ofDecision_isPolynomialTime {decide : List Bool → Bool} (htime : (fun (x : List Bool) => [decide x]) ∈ FP) : (ofDecision decide).IsPolynomialTime

A decision adapter runs in polynomial time whenever its singleton Boolean output function belongs to FP.

theorem Complexity.HeuristicAlgorithm.ofDecision_isErrorlessFor {decide : List Bool → Bool} {L : Language} (hdecide : ∀ (x : List Bool), decide x = true ↔ x ∈ L) : (ofDecision decide).IsErrorlessFor L

An exact Boolean decision function induces a globally errorless heuristic.

@[simp]

theorem Complexity.HeuristicAlgorithm.ofDecision_failureProbability (D : FiniteEnsemble (List Bool)) (decide : List Bool → Bool) (n : ℕ) : failureProbability D (ofDecision decide) n = 0

A total decision adapter has zero failure probability on every ensemble slice.

theorem Complexity.HeuristicAlgorithm.ofDecision_failsWithProbabilityAtMost_zero (D : FiniteEnsemble (List Bool)) (decide : List Bool → Bool) : FailsWithProbabilityAtMost D (ofDecision decide) fun (x : ℕ) => 0

A total decision adapter meets the zero failure bound.

theorem Complexity.inversePolynomialFailure_nonneg (c n : ℕ) : 0 ≤ inversePolynomialFailure c n

The total inverse-polynomial failure target is nonnegative.

theorem Complexity.inversePolynomialFailure_le_one (c n : ℕ) : inversePolynomialFailure c n ≤ 1

The total inverse-polynomial failure target is at most one.

theorem Complexity.AvgPAt_mono {δ ε : ℕ → ℚ} (hδε : ∀ (n : ℕ), δ n ≤ ε n) : AvgPAt δ ⊆ AvgPAt ε

AvgPAt is monotone in its allowed failure probability.

theorem Complexity.mem_AvgP_iff (problem : DistributionalProblem) : problem ∈ AvgP ↔ ∀ (c : ℕ), problem ∈ AvgPAt (inversePolynomialFailure c)

Membership in AvgP means meeting every total inverse-polynomial failure target.

theorem Complexity.DistributionalProblem.mem_AvgPAt_of_decision (problem : DistributionalProblem) (δ : ℕ → ℚ) (decide : List Bool → Bool) (htime : (fun (x : List Bool) => [decide x]) ∈ FP) (hdecide : ∀ (x : List Bool), decide x = true ↔ x ∈ problem.language) (hδ : ∀ (n : ℕ), 0 ≤ δ n) : problem ∈ AvgPAt δ

Any exact polynomial-time Boolean decision function gives a zero-failure member of AvgPAt δ for every nonnegative failure allowance.

theorem Complexity.DistributionalProblem.mem_AvgP_of_decision (problem : DistributionalProblem) (decide : List Bool → Bool) (htime : (fun (x : List Bool) => [decide x]) ∈ FP) (hdecide : ∀ (x : List Bool), decide x = true ↔ x ∈ problem.language) : problem ∈ AvgP

Any exact polynomial-time Boolean decision function solves the same language errorlessly on every distribution ensemble, hence places the distributional problem in AvgP.