Errorless average-case heuristics -- proof internals

This layer proves codec exactness, semantic soundness of complement and decision adapters, and the elementary probability/class monotonicity laws.

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

theorem Complexity.HeuristicAnswer.encode_injective_internal : Function.Injective encode

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

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

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

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

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

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

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

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

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

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

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

theorem Complexity.HeuristicAlgorithm.IsErrorlessFor.one_sub_languageProbability_sub_failure_le_reject_internal {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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Complexity.DistributionalProblem.mem_AvgPAt_of_decision_internal (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 δ

theorem Complexity.DistributionalProblem.mem_AvgP_of_decision_internal (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