Exact rational search for a conditioning set
Lax263307.RationalConditioning · concepts/Lax263307/RationalConditioning.lean · lax-263307
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
For a rational feasible point of , enumerate the vertex sets of size at most and return the first set satisfying and
The sum counts ordered adjacent pairs. This exact rational test is equivalent to the edge-cost condition in Lemma 12. Under that lemma's hypotheses the search succeeds and returns the required costs. The list contains at most candidates.
Concept map
Evidence
Lean source view on GitHub
| 1 | import Lax263307.ConditioningExistence |
| 2 | import Mathlib.Data.Rat.Cast.Order |
| 3 | import Mathlib.Data.List.Sublists |
| 4 | import Mathlib.Data.List.FinRange |
| 5 | import Mathlib.Data.Finset.Card |
| 6 | |
| 7 | /-! |
| 8 | --- |
| 9 | title: Exact rational search for a conditioning set |
| 10 | type: theorem |
| 11 | --- |
| 12 | For a rational feasible point of , enumerate the vertex sets |
| 13 | of size at most and return the first set satisfying and |
| 14 | |
| 15 | |
| 16 | The sum counts ordered adjacent pairs. This exact rational test is equivalent |
| 17 | to the edge-cost condition in Lemma 12. Under that lemma's hypotheses the |
| 18 | search succeeds and returns the required costs. The list contains at most |
| 19 | candidates. |
| 20 | |
| 21 | # Formalization notes |
| 22 | |
| 23 | Candidates are generated as sublists of each prescribed length, in a fixed |
| 24 | order. Enumeration does not first materialize the full power set. |
| 25 | This statement proves exact search correctness and bounds its candidate count; |
| 26 | the RAM instruction and bit-length bounds are separate obligations. |
| 27 | -/ |
| 28 | |
| 29 | namespace Lax263307.RationalConditioning |
| 30 | |
| 31 | open LinearRelaxation Entropy |
| 32 | |
| 33 | /-- Rational coordinates for the same truncated relaxation. -/ |
| 34 | abbrev RationalVector (n r : ℕ) := Coordinate n r → ℚ |
| 35 | |
| 36 | /-- Interpret a rational moment vector in the real vector space. -/ |
| 37 | def realVector {n r : ℕ} (y : RationalVector n r) : MomentVector n r := |
| 38 | fun A => (y A : ℝ) |
| 39 | |
| 40 | /-- Read a rational coordinate, extending by zero outside the coordinate domain. -/ |
| 41 | def rationalValue {n r : ℕ} (y : RationalVector n r) (A : Finset (Fin n)) : ℚ := |
| 42 | if h : A.card ≤ r + 2 then y ⟨A, h⟩ else 0 |
| 43 | |
| 44 | /-- The ordered edge-product numerator in the exact test. -/ |
| 45 | def edgeNumerator {n r : ℕ} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] |
| 46 | (y : RationalVector n r) (A : Finset (Fin n)) : ℚ := |
| 47 | ∑ u, ∑ v, if G.Adj u v then |
| 48 | rationalValue y (insert u A) * rationalValue y (insert v A) else 0 |
| 49 | |
| 50 | /-- The exact rational test after clearing the positive conditioning denominator. -/ |
| 51 | def Passes {n r : ℕ} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] |
| 52 | (k p : ℕ) (y : RationalVector n r) (A : Finset (Fin n)) : Prop := |
| 53 | 0 < rationalValue y A ∧ |
| 54 | (p : ℚ) * edgeNumerator G y A ≤ 2 * (k : ℚ) ^ 2 * rationalValue y A ^ 2 |
| 55 | |
| 56 | /-- The rational test is decidable by exact arithmetic. -/ |
| 57 | instance {n r : ℕ} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] |
| 58 | (k p : ℕ) (y : RationalVector n r) (A : Finset (Fin n)) : Decidable (Passes G k p y A) := |
| 59 | inferInstanceAs (Decidable (0 < rationalValue y A ∧ |
| 60 | (p : ℚ) * edgeNumerator G y A ≤ 2 * (k : ℚ) ^ 2 * rationalValue y A ^ 2)) |
| 61 | |
| 62 | /-- Enumerate only sublists with lengths between zero and the conditioning budget. -/ |
| 63 | def candidates (n r : ℕ) : List (Finset (Fin n)) := |
| 64 | (List.range (r + 1)).flatMap fun j => |
| 65 | ((List.finRange n).sublistsLen j).map List.toFinset |
| 66 | |
| 67 | /-- Return the first candidate satisfying the rational test. -/ |
| 68 | def findConditioning {n r : ℕ} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] |
| 69 | (k p : ℕ) (y : RationalVector n r) : Option (Finset (Fin n)) := |
| 70 | (candidates n r).find? fun A => decide (Passes G k p y A) |
| 71 | |
| 72 | /-- The candidate list contains exactly the vertex sets within the budget. -/ |
| 73 | axiom candidate_complete (n r : ℕ) (A : Finset (Fin n)) : |
| 74 | A ∈ candidates n r ↔ A.card ≤ r |
| 75 | |
| 76 | /-- The number of candidates has the required polynomial dependence on `n` at fixed `r`. -/ |
| 77 | axiom candidate_bound (n r : ℕ) : (candidates n r).length ≤ (r + 1) * (n + 1) ^ r |
| 78 | |
| 79 | /-- The exact rational search returns a conditioning set with the promised costs. -/ |
| 80 | axiom search_correct {n : ℕ} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] |
| 81 | (k r p : ℕ) (y : RationalVector n r) (feasible : IsFeasible G k r (realVector y)) |
| 82 | (target_positive : 0 < k) (level_positive : 0 < r) (threshold_positive : 0 < p) |
| 83 | (budget : 2 * (p : ℝ) * Real.logb 2 n ≤ r) : |
| 84 | ∃ A : Finset (Fin n), findConditioning G k p y = some A ∧ A.card ≤ r ∧ |
| 85 | 0 < value (realVector y) A ∧ |
| 86 | (∀ v, 0 ≤ conditioned (realVector y) A v ∧ conditioned (realVector y) A v ≤ 1) ∧ |
| 87 | (∑ v, conditioned (realVector y) A v) = k ∧ |
| 88 | edgeCost G (conditioned (realVector y) A) ≤ (k : ℝ) ^ 2 / p |
| 89 | |
| 90 | end Lax263307.RationalConditioning |
| 91 |
Formalization notes
Candidates are generated as sublists of each prescribed length, in a fixed order. Enumeration does not first materialize the full power set. This statement proves exact search correctness and bounds its candidate count; the RAM instruction and bit-length bounds are separate obligations.
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments