Exact rational search above the conditioning moment floor
Lax263307.HeavyRationalConditioning · concepts/Lax263307/HeavyRationalConditioning.lean · lax-263307
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
Search the existing bounded-size candidate list using exact rational edge cost tests and the additional moment threshold tau^r. The strengthened entropy argument guarantees a successful candidate. The search returns bounded costs of total mass k, sparse edge cost, and the quantitative conditioning moment floor, without computing entropy values.
Concept map
Evidence
Each proof establishes this claim relative to its assumptions.
Lean source view on GitHub
| 1 | import Lax263307.HeavyConditioning |
| 2 | import Lax263307.RationalConditioning |
| 3 | |
| 4 | /-! |
| 5 | --- |
| 6 | title: Exact rational search above the conditioning moment floor |
| 7 | type: theorem |
| 8 | --- |
| 9 | Search the existing bounded-size candidate list using exact rational edge |
| 10 | cost tests and the additional moment threshold tau^r. The strengthened |
| 11 | entropy argument guarantees a successful candidate. The search returns |
| 12 | bounded costs of total mass k, sparse edge cost, and the quantitative |
| 13 | conditioning moment floor, without computing entropy values. |
| 14 | |
| 15 | # Formalization notes |
| 16 | |
| 17 | The rational floor uses integer n,p,log2 n and has an explicit denominator. |
| 18 | The candidate count remains at most (r+1)(n+1)^r. This proves the executable |
| 19 | search function's correctness; its RAM implementation is still separate. |
| 20 | -/ |
| 21 | |
| 22 | namespace Lax263307.HeavyRationalConditioning |
| 23 | |
| 24 | open LinearRelaxation Entropy RationalConditioning HeavyConditioning |
| 25 | |
| 26 | def rationalFloor (n p : ℕ) : ℚ := 1 / (2 * (n : ℚ) * p * ((Nat.log2 n : ℚ) + 1)) |
| 27 | |
| 28 | def HeavyPasses {n r : ℕ} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] |
| 29 | (k p : ℕ) (y : RationalVector n r) (A : Finset (Fin n)) : Prop := |
| 30 | Passes G k p y A ∧ rationalFloor n p ^ r ≤ rationalValue y A |
| 31 | |
| 32 | instance {n r : ℕ} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] |
| 33 | (k p : ℕ) (y : RationalVector n r) (A : Finset (Fin n)) : Decidable (HeavyPasses G k p y A) := |
| 34 | inferInstanceAs (Decidable (Passes G k p y A ∧ rationalFloor n p ^ r ≤ rationalValue y A)) |
| 35 | |
| 36 | def findHeavyConditioning {n r : ℕ} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] |
| 37 | (k p : ℕ) (y : RationalVector n r) : Option (Finset (Fin n)) := |
| 38 | (candidates n r).find? fun A => decide (HeavyPasses G k p y A) |
| 39 | |
| 40 | |
| 41 | axiom search_correct {n : ℕ} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] |
| 42 | (k r p : ℕ) (y : RationalVector n r) (feasible : IsFeasible G k r (realVector y)) |
| 43 | (order_positive : 0 < n) (target_positive : 0 < k) |
| 44 | (level_positive : 0 < r) (threshold_positive : 0 < p) |
| 45 | (budget : (p : ℝ) * ((Nat.log2 n : ℝ) + 1) ≤ r) : |
| 46 | ∃ A : Finset (Fin n), findHeavyConditioning G k p y = some A ∧ A.card ≤ r ∧ |
| 47 | probabilityFloor n p ^ r ≤ value (realVector y) A ∧ 0 < value (realVector y) A ∧ |
| 48 | (∀ v, 0 ≤ conditioned (realVector y) A v ∧ conditioned (realVector y) A v ≤ 1) ∧ |
| 49 | (∑ v, conditioned (realVector y) A v) = k ∧ |
| 50 | edgeCost G (conditioned (realVector y) A) ≤ (k : ℝ) ^ 2 / p |
| 51 | |
| 52 | end Lax263307.HeavyRationalConditioning |
| 53 |
Formalization notes
The rational floor uses integer n,p,log2 n and has an explicit denominator. The candidate count remains at most (r+1)(n+1)^r. This proves the executable search function's correctness; its RAM implementation is still separate.
Used by
From Mathlib
none
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments