Unrestricted depth-three lower bound: reverse path encoding

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/DepthThree/ReversePathEncoding.lean

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

def Complexity.DepthThreeLowerBound.pathRemainder {V : Type uDepth1} {I : Type uDepth2} [DecidableEq V] [instDecidableEqI : DecidableEq I] (scope : I → Finset V) (T : Finset V) (P : List I) : Finset V

Live coordinates remaining after the path's revealed set is removed.

Equations

• Complexity.DepthThreeLowerBound.pathRemainder scope T P = T \ Complexity.DepthThreeLowerBound.revealed scope T P

@[simp]

theorem Complexity.DepthThreeLowerBound.pathRemainder_nil {V : Type uDepth1} {I : Type uDepth2} [DecidableEq V] [instDecidableEqI : DecidableEq I] (scope : I → Finset V) (T : Finset V) : pathRemainder scope T [] = T

theorem Complexity.DepthThreeLowerBound.coveredCount_eq_reverseEligible {V : Type uDepth1} {I : Type uDepth2} [DecidableEq V] [instFintypeI : Fintype I] (scope : I → Finset V) (T U : Finset V) (violation : I → Bool) : coveredCount scope T violation U = (reverseEligible scope violation (T \ U)).card

noncomputable def Complexity.DepthThreeLowerBound.coveredPathWeight {V : Type uDepth1} {I : Type uDepth2} [DecidableEq V] [instDecidableEqI : DecidableEq I] [instFintypeI : Fintype I] (scope : I → Finset V) (T : Finset V) (violation : I → Bool) (P : List I) : ℝ

The path weight including its covered-coordinate contribution.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Complexity.DepthThreeLowerBound.coveredPathWeight_nil {V : Type uDepth1} {I : Type uDepth2} [DecidableEq V] [instDecidableEqI : DecidableEq I] [instFintypeI : Fintype I] (scope : I → Finset V) (T : Finset V) (violation : I → Bool) : coveredPathWeight scope T violation [] = 1

theorem Complexity.DepthThreeLowerBound.coveredPathWeight_nonneg {V : Type uDepth1} {I : Type uDepth2} [DecidableEq V] [instDecidableEqI : DecidableEq I] [instFintypeI : Fintype I] (scope : I → Finset V) (T : Finset V) (violation : I → Bool) (P : List I) : 0 ≤ coveredPathWeight scope T violation P

theorem Complexity.DepthThreeLowerBound.coveredPathWeight_snoc {V : Type uDepth1} {I : Type uDepth2} [DecidableEq V] [instDecidableEqI : DecidableEq I] [instFintypeI : Fintype I] (scope : I → Finset V) (T : Finset V) (violation : I → Bool) (P : List I) (i : I) : coveredPathWeight scope T violation (P ++ [i]) = coveredPathWeight scope T violation P * (↑(coveredCount scope T violation (revealed scope T (P ++ [i]))))⁻¹

theorem Complexity.DepthThreeLowerBound.remainder_snoc_union_block {V : Type uDepth1} {I : Type uDepth2} [DecidableEq V] [instDecidableEqI : DecidableEq I] (scope : I → Finset V) (T : Finset V) (P : List I) (i : I) : pathRemainder scope T (P ++ [i]) ∪ residual scope T (revealed scope T P) i = pathRemainder scope T P

theorem Complexity.DepthThreeLowerBound.remainder_snoc_disjoint_block {V : Type uDepth1} {I : Type uDepth2} [DecidableEq V] [instDecidableEqI : DecidableEq I] (scope : I → Finset V) (T : Finset V) (P : List I) (i : I) : Disjoint (pathRemainder scope T (P ++ [i])) (residual scope T (revealed scope T P) i)

theorem Complexity.DepthThreeLowerBound.scope_disjoint_remainder_snoc {V : Type uDepth1} {I : Type uDepth2} [DecidableEq V] [instDecidableEqI : DecidableEq I] (scope : I → Finset V) (T : Finset V) (P : List I) (i : I) : Disjoint (scope i) (pathRemainder scope T (P ++ [i]))

def Complexity.DepthThreeLowerBound.reverseEncode {V : Type uDepth1} {I : Type uDepth2} [DecidableEq V] [instDecidableEqI : DecidableEq I] (scope : I → Finset V) (T : Finset V) (P : List I) : List (I × Finset V)

Encode a forward path for the reverse reconstruction argument.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Complexity.DepthThreeLowerBound.reverseEncode_nil {V : Type uDepth1} {I : Type uDepth2} [DecidableEq V] [instDecidableEqI : DecidableEq I] (scope : I → Finset V) (T : Finset V) : reverseEncode scope T [] = []

@[simp]

theorem Complexity.DepthThreeLowerBound.reverseEncode_snoc {V : Type uDepth1} {I : Type uDepth2} [DecidableEq V] [instDecidableEqI : DecidableEq I] (scope : I → Finset V) (T : Finset V) (P : List I) (i : I) : reverseEncode scope T (P ++ [i]) = (i, residual scope T (revealed scope T P) i) :: reverseEncode scope T P

def Complexity.DepthThreeLowerBound.reverseStart {V : Type uDepth1} {I : Type uDepth2} [DecidableEq V] (R : Finset V) (L : List (I × Finset V)) : Finset V

The starting data used to reconstruct an encoded path in reverse.

Equations

• Complexity.DepthThreeLowerBound.reverseStart R L = List.foldl (fun (S : Finset V) (q : I × Finset V) => S ∪ q.2) R L

@[simp]

theorem Complexity.DepthThreeLowerBound.reverseStart_nil {V : Type uDepth1} {I : Type uDepth2} [DecidableEq V] (R : Finset V) : reverseStart R [] = R

@[simp]

theorem Complexity.DepthThreeLowerBound.reverseStart_cons {V : Type uDepth1} {I : Type uDepth2} [DecidableEq V] (R : Finset V) (i : I) (D : Finset V) (L : List (I × Finset V)) : reverseStart R ((i, D) :: L) = reverseStart (R ∪ D) L

theorem Complexity.DepthThreeLowerBound.reverseStart_encode {V : Type uDepth1} {I : Type uDepth2} [DecidableEq V] [instDecidableEqI : DecidableEq I] (scope : I → Finset V) (T : Finset V) (P : List I) : reverseStart (pathRemainder scope T P) (reverseEncode scope T P) = T

theorem Complexity.DepthThreeLowerBound.reverseEncode_indices {V : Type uDepth1} {I : Type uDepth2} [DecidableEq V] [instDecidableEqI : DecidableEq I] (scope : I → Finset V) (T : Finset V) (P : List I) : List.map Prod.fst (reverseEncode scope T P) = P.reverse

def Complexity.DepthThreeLowerBound.encodePathPair {V : Type uDepth1} {I : Type uDepth2} [DecidableEq V] [instDecidableEqI : DecidableEq I] (scope : I → Finset V) (x : (_ : Finset V) × List I) : (_ : Finset V) × List (I × Finset V)

Encode a restriction and path as reverse reconstruction data.

Equations

• Complexity.DepthThreeLowerBound.encodePathPair scope x = ⟨Complexity.DepthThreeLowerBound.pathRemainder scope x.fst x.snd, Complexity.DepthThreeLowerBound.reverseEncode scope x.fst x.snd⟩

theorem Complexity.DepthThreeLowerBound.encodePathPair_injective {V : Type uDepth1} {I : Type uDepth2} [DecidableEq V] [instDecidableEqI : DecidableEq I] (scope : I → Finset V) : Function.Injective (encodePathPair scope)

def Complexity.DepthThreeLowerBound.reverseTraces {V : Type uDepth1} {I : Type uDepth2} [DecidableEq V] [instDecidableEqI : DecidableEq I] [instFintypeI : Fintype I] (scope : I → Finset V) (violation : I → Bool) (b : ℕ) : ℕ → Finset V → Finset (List (I × Finset V))

The finite family of admissible reverse reconstruction traces.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.DepthThreeLowerBound.reverseTraces scope violation b 0 x✝ = {[]}

@[simp]

theorem Complexity.DepthThreeLowerBound.mem_reverseTraces_zero {V : Type uDepth1} {I : Type uDepth2} [DecidableEq V] [instDecidableEqI : DecidableEq I] [instFintypeI : Fintype I] (scope : I → Finset V) (violation : I → Bool) (b : ℕ) (R : Finset V) (L : List (I × Finset V)) : L ∈ reverseTraces scope violation b 0 R ↔ L = []

theorem Complexity.DepthThreeLowerBound.mem_reverseTraces_succ {V : Type uDepth1} {I : Type uDepth2} [DecidableEq V] [instDecidableEqI : DecidableEq I] [instFintypeI : Fintype I] (scope : I → Finset V) (violation : I → Bool) (b s : ℕ) (R : Finset V) (L : List (I × Finset V)) : L ∈ reverseTraces scope violation b (s + 1) R ↔ ∃ i ∈ reverseEligible scope violation R, ∃ D ∈ reverseBlocks b (scope i), ∃ M ∈ reverseTraces scope violation b s (R ∪ D), (i, D) :: M = L

theorem Complexity.DepthThreeLowerBound.reverseEncode_mem {V : Type uDepth1} {I : Type uDepth2} [DecidableEq V] [instDecidableEqI : DecidableEq I] [instFintypeI : Fintype I] (scope : I → Finset V) (violation : I → Bool) (b : ℕ) (T : Finset V) {j : ℕ} {P : List I} (hP : P ∈ paths scope T b j) (hs : ∀ i ∈ P, violation i = true) : reverseEncode scope T P ∈ reverseTraces scope violation b j (pathRemainder scope T P)

def Complexity.DepthThreeLowerBound.reverseTraceWeight {V : Type uDepth1} {I : Type uDepth2} [DecidableEq V] [instFintypeI : Fintype I] (α : ℝ) (scope : I → Finset V) (violation : I → Bool) : Finset V → List (I × Finset V) → ℝ

The product weight of a reverse reconstruction trace.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.DepthThreeLowerBound.reverseTraceWeight α scope violation x✝ [] = 1

theorem Complexity.DepthThreeLowerBound.reverseTraceWeight_nonneg {V : Type uDepth1} {I : Type uDepth2} [DecidableEq V] [instFintypeI : Fintype I] {α : ℝ} (hα : 0 ≤ α) (scope : I → Finset V) (violation : I → Bool) (R : Finset V) (L : List (I × Finset V)) : 0 ≤ reverseTraceWeight α scope violation R L

theorem Complexity.DepthThreeLowerBound.sum_reverseTraces_succ {V : Type uDepth1} {I : Type uDepth2} [DecidableEq V] [instDecidableEqI : DecidableEq I] [instFintypeI : Fintype I] (scope : I → Finset V) (violation : I → Bool) (b s : ℕ) (R : Finset V) (f : List (I × Finset V) → ℝ) : ∑ L ∈ reverseTraces scope violation b (s + 1) R, f L = ∑ i ∈ reverseEligible scope violation R, ∑ D ∈ reverseBlocks b (scope i), ∑ L ∈ reverseTraces scope violation b s (R ∪ D), f ((i, D) :: L)

theorem Complexity.DepthThreeLowerBound.sum_reverseTraceWeight {V : Type uDepth1} {I : Type uDepth2} [DecidableEq V] [instDecidableEqI : DecidableEq I] [instFintypeI : Fintype I] (α : ℝ) (scope : I → Finset V) (violation : I → Bool) (b j : ℕ) (R : Finset V) : ∑ L ∈ reverseTraces scope violation b j R, reverseTraceWeight α scope violation R L = reverseTotal α b scope violation j R

theorem Complexity.DepthThreeLowerBound.reverseEncode_weight {V : Type uDepth1} {I : Type uDepth2} [DecidableEq V] [instDecidableEqI : DecidableEq I] [instFintypeI : Fintype I] [Fintype V] (p : ℝ) (hp0 : 0 < p) (hp1 : p < 1) (scope : I → Finset V) (violation : I → Bool) (T : Finset V) (P : List I) : bernoulliWeight p T * 2 ^ (revealed scope T P).card * coveredPathWeight scope T violation P = bernoulliWeight p (pathRemainder scope T P) * reverseTraceWeight (2 * p / (1 - p)) scope violation (pathRemainder scope T P) (reverseEncode scope T P)

def Complexity.DepthThreeLowerBound.supportedForwardPairs {V : Type uDepth1} {I : Type uDepth2} [DecidableEq V] [instDecidableEqI : DecidableEq I] [instFintypeI : Fintype I] [Fintype V] (scope : I → Finset V) (violation : I → Bool) (b j : ℕ) : Finset ((_ : Finset V) × List I)

Forward restriction-path pairs having nonzero supported contribution.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.DepthThreeLowerBound.indexedReverseTraces {V : Type uDepth1} {I : Type uDepth2} [DecidableEq V] [instDecidableEqI : DecidableEq I] [instFintypeI : Fintype I] [Fintype V] (scope : I → Finset V) (violation : I → Bool) (b j : ℕ) : Finset ((_ : Finset V) × List (I × Finset V))

Reverse traces indexed by their starting data.

Equations

• Complexity.DepthThreeLowerBound.indexedReverseTraces scope violation b j = Finset.univ.sigma fun (R : Finset V) => Complexity.DepthThreeLowerBound.reverseTraces scope violation b j R

theorem Complexity.DepthThreeLowerBound.encode_supported_mem {V : Type uDepth1} {I : Type uDepth2} [DecidableEq V] [instDecidableEqI : DecidableEq I] [instFintypeI : Fintype I] [Fintype V] (scope : I → Finset V) (violation : I → Bool) (b j : ℕ) {x : (_ : Finset V) × List I} (hx : x ∈ supportedForwardPairs scope violation b j) : encodePathPair scope x ∈ indexedReverseTraces scope violation b j

theorem Complexity.DepthThreeLowerBound.weighted_supported_paths_le {V : Type uDepth1} {I : Type uDepth2} [DecidableEq V] [instDecidableEqI : DecidableEq I] [instFintypeI : Fintype I] [Fintype V] (p : ℝ) (hp0 : 0 < p) (hp1 : p < 1) (b k : ℕ) (scope : I → Finset V) (hscope : ∀ (i : I), (scope i).card ≤ k) (violation : I → Bool) (j : ℕ) : (∑ T : Finset V, bernoulliWeight p T * ∑ P ∈ paths scope T b j, if ∀ i ∈ P, violation i = true then 2 ^ (revealed scope T P).card * coveredPathWeight scope T violation P else 0) ≤ reverseTheta (2 * p / (1 - p)) b k ^ j