The moment relaxation as an explicit rational linear program
Lax263307.MomentLP · concepts/Lax263307/MomentLP.lean · lax-263307
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
Use the computable moment catalog as the LP variable order. Paired normalization rows, upper-bound rows, nonindependence rows, insertion monotonicity rows, and paired conditioned-mass rows encode the relaxation exactly. Primal nonnegativity supplies the coordinate lower bounds. The resulting rational LP has N variables and 2+4N+Nn rows, where N≤(r+3)(n+1)^(r+2).
Concept map
Evidence
This concept declares 6 statements. Each proof establishes one of them relative to its assumptions.
1 decode_encode proven
2 encode_decode proven
3 evaluate_encoding proven
4 feasible_iff proven
5 primal_characterization proven
6 single_row_value proven
Lean source view on GitHub
| 1 | import Lax263307.CoordinateCatalog |
| 2 | import Lax263307.ComponentCutEncoding |
| 3 | import Lax109476.RationalCertificates |
| 4 | |
| 5 | /-! |
| 6 | --- |
| 7 | title: The moment relaxation as an explicit rational linear program |
| 8 | type: theorem |
| 9 | --- |
| 10 | Use the computable moment catalog as the LP variable order. Paired |
| 11 | normalization rows, upper-bound rows, nonindependence rows, insertion |
| 12 | monotonicity rows, and paired conditioned-mass rows encode the relaxation |
| 13 | exactly. Primal nonnegativity supplies the coordinate lower bounds. |
| 14 | The resulting rational LP has N variables and 2+4N+Nn rows, where |
| 15 | N≤(r+3)(n+1)^(r+2). |
| 16 | |
| 17 | # Formalization notes |
| 18 | |
| 19 | All finite index concatenations and graph independence tests are computable. |
| 20 | Rows indexed by sets of size r+2 are inactive in the two families restricted |
| 21 | to size at most r+1. Collected component-cut coefficients can use the same |
| 22 | catalog order, with evaluation exactly equal to a native finite dot product. |
| 23 | Dense input construction and solver execution on RAM remain separate bounds. |
| 24 | -/ |
| 25 | |
| 26 | namespace Lax263307.MomentLP |
| 27 | |
| 28 | open LinearRelaxation CoordinateCatalog |
| 29 | open Lax109476.LinearProgram Lax109476.RationalCertificates |
| 30 | |
| 31 | abbrev dimension (n r : ℕ) : ℕ := (catalog n r).length |
| 32 | abbrev Index (n r : ℕ) := Fin (dimension n r) |
| 33 | |
| 34 | def decode {K : Type} {n r : ℕ} (x : Index n r → K) : Coordinate n r → K := |
| 35 | fun A => x ((indexing n r).symm A) |
| 36 | |
| 37 | def encode {K : Type} {n r : ℕ} (y : Coordinate n r → K) : Index n r → K := |
| 38 | fun j => y (indexing n r j) |
| 39 | |
| 40 | def singleRow {n r : ℕ} (A : Finset (Fin n)) (j : Index n r) : ℚ := |
| 41 | if A = (indexing n r j).val then 1 else 0 |
| 42 | |
| 43 | def monotoneRow {n r : ℕ} (A : Finset (Fin n)) (v : Fin n) (j : Index n r) : ℚ := |
| 44 | singleRow (insert v A) j - singleRow A j |
| 45 | |
| 46 | def massRow {n r : ℕ} (A : Finset (Fin n)) (k : ℕ) (j : Index n r) : ℚ := |
| 47 | (∑ v, singleRow (insert v A) j) - (k : ℚ) * singleRow A j |
| 48 | |
| 49 | def program {n : ℕ} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] (k r : ℕ) : |
| 50 | Program ℚ (2 + (dimension n r + (dimension n r + (dimension n r * n + (dimension n r + dimension n r))))) (dimension n r) where |
| 51 | A := Fin.addCases |
| 52 | (fun i : Fin 2 => fun j => if i = 0 then singleRow ∅ j else -singleRow ∅ j) |
| 53 | (Fin.addCases |
| 54 | (fun i : Index n r => singleRow (indexing n r i).val) |
| 55 | (Fin.addCases |
| 56 | (fun i : Index n r => fun j => |
| 57 | if G.IsIndepSet ((indexing n r i).val : Set (Fin n)) then 0 else singleRow (indexing n r i).val j) |
| 58 | (Fin.addCases |
| 59 | (fun i : Fin (dimension n r * n) => |
| 60 | let uv := finProdFinEquiv.symm i |
| 61 | if (indexing n r uv.1).val.card ≤ r + 1 then monotoneRow (indexing n r uv.1).val uv.2 else fun _ => 0) |
| 62 | (Fin.addCases |
| 63 | (fun i : Index n r => |
| 64 | if (indexing n r i).val.card ≤ r + 1 then massRow (indexing n r i).val k else fun _ => 0) |
| 65 | (fun i : Index n r => fun j => |
| 66 | if (indexing n r i).val.card ≤ r + 1 then -massRow (indexing n r i).val k j else 0))))) |
| 67 | b := Fin.addCases (fun i : Fin 2 => if i = 0 then 1 else -1) |
| 68 | (Fin.addCases (fun _ : Index n r => 1) (fun _ => 0)) |
| 69 | c := fun _ => 0 |
| 70 | |
| 71 | axiom decode_encode {K : Type} {n r : ℕ} (y : Coordinate n r → K) : decode (encode y) = y |
| 72 | |
| 73 | axiom encode_decode {K : Type} {n r : ℕ} (x : Index n r → K) : encode (decode x) = x |
| 74 | |
| 75 | axiom single_row_value {n r : ℕ} (x : Index n r → ℝ) (A : Finset (Fin n)) : |
| 76 | (∑ j, (singleRow A j : ℝ) * x j) = value (decode x) A |
| 77 | |
| 78 | axiom primal_characterization {n : ℕ} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] (k r : ℕ) |
| 79 | (x : Index n r → ℝ) : |
| 80 | PrimalFeasible (toReal (program G k r)) x ↔ Lax263307.LinearRelaxation.IsFeasible G k r (decode x) |
| 81 | |
| 82 | axiom feasible_iff {n : ℕ} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] (k r : ℕ) : |
| 83 | Lax109476.LinearProgram.IsFeasible (toReal (program G k r)) ↔ |
| 84 | ∃ y : MomentVector n r, Lax263307.LinearRelaxation.IsFeasible G k r y |
| 85 | |
| 86 | axiom evaluate_encoding {n r : ℕ} (a : Coordinate n r → ℤ) (x : Index n r → ℝ) : |
| 87 | Lax263307.ComponentCutEncoding.evaluate a (decode x) = |
| 88 | (fun j => ((encode a j : ℤ) : ℝ)) ⬝ᵥ x |
| 89 | |
| 90 | end Lax263307.MomentLP |
| 91 |
Formalization notes
All finite index concatenations and graph independence tests are computable. Rows indexed by sets of size r+2 are inactive in the two families restricted to size at most r+1. Collected component-cut coefficients can use the same catalog order, with evaluation exactly equal to a native finite dot product. Dense input construction and solver execution on RAM remain separate bounds.
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments