OAI/Combinatorics/KServer/OutputDynamics.lean

GitHub source file

76 declarations, 0 contain sorry, 0 declared as axioms

Rule II: the finite type I here indexes sides only, with the dominant coordinate stored separately. Thus the formulation includes an empty side set.

  1. def OAI.KServer.OutputDynamics.variation line 15
  2. def OAI.KServer.OutputDynamics.excess line 16
  3. def OAI.KServer.OutputDynamics.holesI line 18
  4. def OAI.KServer.OutputDynamics.outputI line 19
  5. lemma OAI.KServer.OutputDynamics.variation_nonneg line 22
  6. lemma OAI.KServer.OutputDynamics.variation_triangle line 25
  7. lemma OAI.KServer.OutputDynamics.variation_sum line 29
  8. lemma OAI.KServer.OutputDynamics.positive_part_lipschitz line 33
  9. lemma OAI.KServer.OutputDynamics.excess_lipschitz line 36
  10. lemma OAI.KServer.OutputDynamics.excess_nonneg line 44
  11. lemma OAI.KServer.OutputDynamics.holesI_nonneg line 47
  12. lemma OAI.KServer.OutputDynamics.holesI_sum line 50
  13. lemma OAI.KServer.OutputDynamics.holesI_movement line 53
  14. lemma OAI.KServer.OutputDynamics.outputI_budget line 66
  15. lemma OAI.KServer.OutputDynamics.hole_bound line 75
  16. lemma OAI.KServer.OutputDynamics.regular_hole line 92

    Source documentation

    Rule I at a regular coordinate. This includes S=0 without division.

    lemma regular_hole {S R β βi e η B a : ℝ}
    (hS : 0 ≤ S) (hR : 0 ≤ R) (he : 0 ≤ e) (hB : 0 ≤ B)
    (ha : 0 ≤ a) (_hη : 0 ≤ 1 + η) (hβ : 0 ≤ β) (hβi : 0 ≤ βi)
    (hr : R ≤ β * S + e) (hp : S * a ≤ (1 + η) * B)
    (hroom : (β * S + e) * (1 + η) ≤ βi * S)
    (hzero : S = 0 → e = 0) : R * a ≤ βi * B := by
…
  17. lemma OAI.KServer.OutputDynamics.dominant_hole line 109
  18. lemma OAI.KServer.OutputDynamics.regular_parameter_room line 120

    Source documentation

    The error margin used on regular children, including zero core mass.

    lemma regular_parameter_room {S β βi e η g : ℝ}
    (hS : 0 ≤ S) (he : 0 ≤ e) (hη : η ≤ 1)
    (hgap : β + g ≤ βi) (hηgap : β * η ≤ g / 2)
    (herr : 4 * e ≤ g * S) : (β * S + e) * (1 + η) ≤ βi * S := by
…
  19. lemma OAI.KServer.OutputDynamics.outputI_regular line 130

    Source documentation

    Literal regular-coordinate lower bound for Rule I, and its upper cap.

    lemma outputI_regular {n B f b a η βi : I → ℝ} {β e q : ℝ}
    (hp : (∑ i, (n i - β * B i + f i)) ≤ q)
    (hc : (∑ i, (b i - f i)) ≤ e) (hβ : 0 ≤ β) (he : 0 ≤ e)
    (hB : ∀ i, 0 ≤ B i) (ha : ∀ i, 0 ≤ a i)
    (hprop : ∀ i, (∑ j, B j) * a i ≤ (1 + η i) * B i)
    (hzero : (∑ i, B i) = 0 → e = 0)
    (i : I) (hβi : 0 ≤ βi i) (hη : 0 ≤ 1 + η i)
    (hroom : (β * (∑ j, B j) + e) * (1 + η i) ≤ βi i * (∑ j, B j))
    (fc : ℝ) (hfc : fc ≤ b i) :
    n i - βi i * B i + fc ≤ outputI (fun j => n j + b j) q a i ∧
      outputI (fun j => n j + b j) q a i ≤ n i + b i := by
…

    Mentions: OAI.KServer.OutputDynamics.outputI

  20. lemma OAI.KServer.OutputDynamics.outputI_dominant line 148
  21. def OAI.KServer.OutputDynamics.sideOutput line 168
  22. def OAI.KServer.OutputDynamics.dominantOutput line 169
  23. def OAI.KServer.OutputDynamics.dominantHole line 171
  24. def OAI.KServer.OutputDynamics.totalExcess line 173
  25. lemma OAI.KServer.OutputDynamics.dominant_hole_identity line 176
  26. lemma OAI.KServer.OutputDynamics.holesII_sum line 198
  27. lemma OAI.KServer.OutputDynamics.outputII_feasibility line 206

    Source documentation

    Feasibility, with exactly the parent lower bound, regular flex caps, side-proportion inequalities and dominant parameter slack used in §05.

    lemma outputII_feasibility {n B f fc b w βi θ z : I → ℝ}
    {no Bo fo fco bo β βo D q : ℝ}
    (hD : 0 ≤ D) (hw : ∀ i, 0 ≤ w i) (_hB : ∀ i, 0 ≤ B i)
    (hβo : 0 ≤ βo) (hBo : 0 ≤ Bo)
    (hlcap : ∀ i, fc i ≤ b i) (hucap : ∀ i, b i ≤ f i)
    (hdomcap : fco ≤ bo)
    (hparent : no - β * Bo + fo + (∑ i, (n i - β * B i + f i)) ≤ q)
    (hupper : ∀ i, D * w i ≤ βi i * B i)
    (hlower : ∀ i, β * B i - D * θ i * z i ≤ D * w i)
    (hslack : D * (∑ i, θ i * z i) ≤
      (no - β * Bo + fo) - (no - βo * Bo + fco)) :
    (∀ i, n i - βi i * B i + fc i ≤ sideOutput (fun j => n j + b j) w D i ∧
…

    Mentions: OAI.KServer.OutputDynamics.sideOutput

  28. lemma OAI.KServer.OutputDynamics.dominantHole_lipschitz line 249
  29. lemma OAI.KServer.OutputDynamics.holesII_movement line 257
  30. lemma OAI.KServer.OutputDynamics.scaled_movement line 263
  31. lemma OAI.KServer.OutputDynamics.output_from_holes_movement line 278
  32. lemma OAI.KServer.OutputDynamics.outputI_movement line 288

    Source documentation

    The parent coefficient is genuinely one, independent of degree.

    lemma outputI_movement {d d' a a' : I → ℝ} {q q' : ℝ}
    (ha : ∀ i, 0 ≤ a i) (hsa : ∑ i, a i = 1) :
    variation (outputI d' q' a') (outputI d q a) ≤
      |q' - q| + 2 * variation d' d + excess d' q' * variation a' a := by
…

    Mentions: OAI.KServer.OutputDynamics.variation, OAI.KServer.OutputDynamics.outputI, OAI.KServer.OutputDynamics.excess

  33. def OAI.KServer.OutputDynamics.withDominant line 300

    Source documentation

    A star as one dominant coordinate and a (possibly empty) finite side set.

    def withDominant (x : ℝ) (xs : I → ℝ) : Option I → ℝ
  | none => x
  | some i => xs i
  34. def OAI.KServer.OutputDynamics.holesII line 304
  35. def OAI.KServer.OutputDynamics.outputII line 307
  36. lemma OAI.KServer.OutputDynamics.variation_dominant line 310
  37. lemma OAI.KServer.OutputDynamics.holesII_vector_sum line 314
  38. lemma OAI.KServer.OutputDynamics.holesII_nonneg line 319
  39. lemma OAI.KServer.OutputDynamics.outputII_is_holes line 326
  40. lemma OAI.KServer.OutputDynamics.outputII_movement line 342

    Source documentation

    Literal Rule II, not merely an assumed hole formula; coefficient of parent movement is exactly one, also for inserted/deleted zero side coordinates.

    lemma outputII_movement {do_ do' q q' D D' Cw : ℝ} {d d' w w' : I → ℝ}
    (hD : 0 ≤ D) (hD' : 0 ≤ D') (hw : ∀ i, 0 ≤ w i) (hw' : ∀ i, 0 ≤ w' i)
    (hws : (∑ i, w i) ≤ Cw) :
    variation (outputII do' q' d' w' D') (outputII do_ q d w D) ≤
      |q'-q|+2*variation (withDominant do' d') (withDominant do_ d)+
      2*D'*variation w' w+2*Cw*|D'-D| := by
…

    Mentions: OAI.KServer.OutputDynamics.variation, OAI.KServer.OutputDynamics.outputII, OAI.KServer.OutputDynamics.withDominant

  41. lemma OAI.KServer.OutputDynamics.variation_le_mass line 367
  42. lemma OAI.KServer.OutputDynamics.downcross_movement line 377

    Source documentation

    A switch uses the actual old rule, without evaluating the unused rule at the old inputs. These are the full downcrossing/upcrossing estimates of §05.

    lemma downcross_movement {R R' D' Cr Cw : ℝ} {a : Option I → ℝ} {w' : I → ℝ}
    (hR : 0 ≤ R) (hR' : 0 ≤ R') (hD' : 0 ≤ D') (ha : ∀ i, 0 ≤ a i)
    (hsa : ∑ i, a i=1) (hw' : ∀ i, 0 ≤ w' i) (hws : (∑ i, w' i) ≤ Cw)
    (hr : R' ≤ Cr*D') :
    variation (holesII R' (fun i => D'*w' i)) (holesI R a) ≤
      |R'-R|+(2*Cr+Cw)*D' := by
…

    Mentions: OAI.KServer.OutputDynamics.variation, OAI.KServer.OutputDynamics.holesII, OAI.KServer.OutputDynamics.holesI

  43. lemma OAI.KServer.OutputDynamics.upcross_movement line 396
  44. def OAI.KServer.HeldWeights.regular line 428

    Source documentation

    Literal regular gap weight; zero coordinates are harmless placeholders.

    def regular (A a : ℝ) : ℝ := 1+max 0 (Real.log (A/a))
  45. lemma OAI.KServer.HeldWeights.regular_one line 430
  46. lemma OAI.KServer.HeldWeights.regular_log line 433
  47. lemma OAI.KServer.HeldWeights.regular_eq line 436
  48. lemma OAI.KServer.HeldWeights.regular_exp line 440
  49. lemma OAI.KServer.HeldWeights.regular_upper line 447
  50. lemma OAI.KServer.HeldWeights.log_reciprocal_lower line 469
  51. lemma OAI.KServer.HeldWeights.side_lower line 480
  52. lemma OAI.KServer.HeldWeights.exp_sum line 509
  53. lemma OAI.KServer.HeldWeights.side_exp_sum line 518
  54. structure OAI.KServer.CausalSimplex.Input line 540

    Source documentation

    Current held parameters and raw ranks. The latter are used only for the initial minimizing selection, never substituted for the affine rank input.

    structure Input (J R : Type) [Fintype J] where
…
  55. def OAI.KServer.CausalSimplex.prepared line 545
  56. def OAI.KServer.CausalSimplex.prepare line 548
  57. def OAI.KServer.CausalSimplex.candidate line 553
  58. def OAI.KServer.CausalSimplex.move line 560

    Source documentation

    The membership branch totalizes the mathematical rule off its admitted rank/parameter domain. The ordinary regular/marked lemmas below prove it is never used on genuine source data. Wholesale steps use the canonical base.

    def move (C ell : ℝ) (old new : Input J R) (p : J × R → ℝ) (a : J → ℝ) : J → ℝ := by
…

    Mentions: OAI.KServer.CausalSimplex.Input

  59. lemma OAI.KServer.CausalSimplex.move_mem line 567
  60. def OAI.KServer.CausalSimplex.model line 578

    Source documentation

    Only initialization changes the seed; the potential and coefficient are the exact source primitives already proved affine in the raw ranks.

    def model (C ell : ℝ) : Family (Input J R) (J × R) J where
…

    Mentions: OAI.KServer.CausalSimplex.Input

  61. lemma OAI.KServer.CausalSimplex.model_value line 589
  62. lemma OAI.KServer.CausalSimplex.model_update line 592
  63. def OAI.KServer.CausalSimplex.transport line 595
  64. def OAI.KServer.CausalSimplex.mass line 601
  65. def OAI.KServer.CausalSimplex.run line 603
  66. lemma OAI.KServer.CausalSimplex.run_mem line 608
  67. lemma OAI.KServer.CausalSimplex.run_initial line 614
  68. lemma OAI.KServer.CausalSimplex.run_successor line 619
  69. lemma OAI.KServer.CausalSimplex.run_adapted line 624
  70. lemma OAI.KServer.CausalSimplex.candidate_regular line 638
  71. lemma OAI.KServer.CausalSimplex.move_regular line 645
  72. lemma OAI.KServer.CausalSimplex.regular_successor line 667

    Source documentation

    The fully specified causal successor is the source's prepared/deleted/ minimized successor on an ordinary unmarked epoch. No policy-existence or expected drift statement is an assumption.

    lemma regular_successor {Ω : Type} [Fintype Ω] (d : ℕ → Ω → Input J R)
    (t : ℕ) (ω : Ω) {A B : Finset J} (hA : A.Nonempty) (hB : B.Nonempty)
    (f g : J → R → Bool) (h h' : J → ℝ)
    (hh : ∀ i, 1≤h i) (hh' : ∀ i, 1≤h' i)
    {C ell ct ηmax Cexp : ℝ} (hC : 0<C) (hl : 0<ell) (hc : 0<ct)
    (hmax : ∀ i∈A, ct*h i/ell≤ηmax) (hCexp : 0≤Cexp)
    (htail : ∑ i∈A, Real.exp (-h i)≤Cexp)
    (hgap : 2*(25+32*Cexp)*(1+ηmax)<C*ct)
    (hp : ∀ ir, 0≤(d (t+1) ω).ranks ir)
    (hold : (d t ω).data=regular A f h (fun i => ct*h i/ell) hh)
    (hnew : (d (t+1) ω).data=regular B g h' (fun i => ct*h' i/ell) hh')
    (he : (d t ω).epoch=(d (t+1) ω).epoch) :
…

    Mentions: OAI.KServer.CausalSimplex.Input

  73. lemma OAI.KServer.CausalSimplex.candidate_marked line 703
  74. lemma OAI.KServer.CausalSimplex.move_marked line 711
  75. lemma OAI.KServer.CausalSimplex.move_wholesale line 734
  76. lemma OAI.KServer.CausalSimplex.marked_successor line 739