Documentation

Complexitylib.BooleanAnalysis.Sensitivity.Internal.RecursiveCandidates

Sensitivity separation: recursive candidates #

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/Sensitivity/RecursiveCandidates.lean

Imports, namespaces, module visibility, documentation, and formatting are adapted for complexitylib. The source theorem statements and mathematical proofs are retained.

source
theorem Complexity.BooleanAnalysis.Sensitivity.Internal.targetWitness_false {k r h : ℕ} {I : Type} (T : Tournament k) (label : Fin k → Fin k → Fin r) (F : Fin (h + 1) → (I → Bool) → Bool) (q : Fin h) (x : (Fin k × Fin r) × I → Bool) (hr : 0 < r) (i : Fin k) (hi : i ∈ targetCandidates T label F q x) :
F (Fin.last h) (recursiveChild x i (targetWitness F x hr i)) = false
source
theorem Complexity.BooleanAnalysis.Sensitivity.Internal.targetWitness_unique {k r h : ℕ} {I : Type} (T : Tournament k) (label : Fin k → Fin k → Fin r) (F : Fin (h + 1) → (I → Bool) → Bool) (q : Fin h) (x : (Fin k × Fin r) × I → Bool) (hr : 0 < r) (i : Fin k) (hi : i ∈ targetCandidates T label F q x) (c : Fin r) (hc : F (Fin.last h) (recursiveChild x i c) = false) :
c = targetWitness F x hr i
source
theorem Complexity.BooleanAnalysis.Sensitivity.Internal.gateWitness_spec {k r h : ℕ} {I : Type} (T : Tournament k) (label : Fin k → Fin k → Fin r) (F : Fin (h + 1) → (I → Bool) → Bool) (q : Fin h) (x : (Fin k × Fin r) × I → Bool) (i : Fin k) (hi : i ∈ gateCandidates T label F q x) :
T.Adj i (gateWitness T label F q x i) ∧ F (gateIndex q) (recursiveChild x (gateWitness T label F q x i) (label i (gateWitness T label F q x i))) = true
source
theorem Complexity.BooleanAnalysis.Sensitivity.Internal.gateWitness_unique {k r h : ℕ} {I : Type} (T : Tournament k) (label : Fin k → Fin k → Fin r) (F : Fin (h + 1) → (I → Bool) → Bool) (q : Fin h) (x : (Fin k × Fin r) × I → Bool) (i : Fin k) (hi : i ∈ gateCandidates T label F q x) (j : Fin k) (hij : T.Adj i j) (hj : F (gateIndex q) (recursiveChild x j (label i j)) = true) :
j = gateWitness T label F q x i
source
noncomputable def Complexity.BooleanAnalysis.Sensitivity.Internal.gateSinks {k r h : ℕ} {I : Type} (T : Tournament k) (label : Fin k → Fin k → Fin r) (F : Fin (h + 1) → (I → Bool) → Bool) (q : Fin h) (x : (Fin k × Fin r) × I → Bool) :
Finset (Fin k)

Gate candidates with no outgoing edge to another gate candidate.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Complexity.BooleanAnalysis.Sensitivity.Internal.gateSinks_card {k r h : ℕ} {I : Type} (T : Tournament k) (label : Fin k → Fin k → Fin r) (F : Fin (h + 1) → (I → Bool) → Bool) (q : Fin h) (x : (Fin k × Fin r) × I → Bool) :
    (gateSinks T label F q x).card ≤ 1
    source
    theorem Complexity.BooleanAnalysis.Sensitivity.Internal.nonsink_gateWitness_mem {k r h : ℕ} {I : Type} (T : Tournament k) (label : Fin k → Fin k → Fin r) (F : Fin (h + 1) → (I → Bool) → Bool) (hF : NestedFamily F) (q : Fin h) (x : (Fin k × Fin r) × I → Bool) (i : Fin k) (hi : i ∈ gateCandidates T label F q x) (hs : i ∉ gateSinks T label F q x) :
    gateWitness T label F q x i ∈ gateCandidates T label F q x