OAI/Probability/FKMaps/BlockLaw.lean

GitHub source file

78 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.FKCRT.Inventory.rawWord_signSum line 11
  2. lemma OAI.FKCRT.Inventory.rawWord_take line 15
  3. lemma OAI.FKCRT.Inventory.emptyProb_le_killed line 19
  4. theorem OAI.FKCRT.Inventory.emptyProb_summable line 33

    Source documentation

    Finiteness of the endpoint inventory generating function follows from the actual killed walk Green sum; no coefficient asymptotic is assumed.

    theorem emptyProb_summable (P : Parameters) : Summable (emptyProb P) :=
…

    Mentions: OAI.FKCRT.Inventory.Parameters, OAI.FKCRT.Inventory.emptyProb

  5. theorem OAI.FKCRT.Inventory.emptyProb_even_summable line 35
  6. lemma OAI.FKCRT.Inventory.emptyProb_zero line 37
  7. def OAI.FKCRT.Inventory.emptyTotal line 41
  8. lemma OAI.FKCRT.Inventory.emptyTotal_ge_one line 42
  9. lemma OAI.FKCRT.Inventory.emptyTotal_pos line 46
  10. def OAI.FKCRT.Inventory.emptyWeights line 48
  11. theorem OAI.FKCRT.Inventory.emptyWeights_abel_lower line 58

    Source documentation

    The normalized exact word coefficient law has the required near-endpoint Abel lower bound. The remaining bridge to map coefficients is combinatorial.

    theorem emptyWeights_abel_lower (P : Parameters) : ∃ c : ℝ,0<c ∧ ∀ x : ℝ,(3:ℝ)/4≤x → x<1 →
    c≤Real.sqrt (1-x)*(emptyWeights P).abelMean x := by
…

    Mentions: OAI.FKCRT.Inventory.Parameters, OAI.FKCRT.Inventory.emptyWeights

  12. def OAI.FKCRT.Inventory.flexParameter line 85
  13. def OAI.FKCRT.Inventory.radiusParameter line 86
  14. lemma OAI.FKCRT.Inventory.flexParameter_pos line 88
  15. lemma OAI.FKCRT.Inventory.radiusParameter_pos line 95
  16. lemma OAI.FKCRT.Inventory.typedCoefficient_inventory line 98
  17. def OAI.FKCRT.Inventory.inventorySeries line 115
  18. lemma OAI.FKCRT.Inventory.inventorySeries_summable line 117
  19. lemma OAI.FKCRT.Inventory.inventorySeries_nonneg line 123
  20. lemma OAI.FKCRT.Inventory.inventorySeries_ge_one line 126
  21. lemma OAI.FKCRT.Inventory.wordSeries_inventory line 132
  22. def OAI.FKCRT.Inventory.coreCoefficientReal line 147
  23. lemma OAI.FKCRT.Inventory.coreCoefficientReal_nonneg line 150
  24. lemma OAI.FKCRT.Inventory.coreCoefficient_ofReal line 153
  25. lemma OAI.FKCRT.Inventory.coreCoefficientReal_zero line 161
  26. theorem OAI.FKCRT.Inventory.actual_core_series line 171

    Source documentation

    A real HasSum form of the exact root-corner substitution, derived from finite endpoint summability rather than assumed analytic convergence.

    theorem actual_core_series (P : Parameters) {x : ℝ} (hx : 0 ≤ x) (hx' : x ≤ 1) :
    HasSum (fun m => coreCoefficientReal (flexParameter P) m*
      (radiusParameter P*x*(inventorySeries P x)^2)^m) (inventorySeries P x-1) := by
…

    Mentions: OAI.FKCRT.Inventory.Parameters, OAI.FKCRT.Inventory.coreCoefficientReal, OAI.FKCRT.Inventory.flexParameter, OAI.FKCRT.Inventory.radiusParameter, OAI.FKCRT.Inventory.inventorySeries

  27. def OAI.FKCRT.Inventory.blockCoefficientReal line 213
  28. def OAI.FKCRT.Inventory.actualBlockMass line 216
  29. lemma OAI.FKCRT.Inventory.blockCoefficientReal_nonneg line 220
  30. lemma OAI.FKCRT.Inventory.actualBlockMass_nonneg line 225
  31. lemma OAI.FKCRT.Inventory.actualBlockMass_zero line 230
  32. lemma OAI.FKCRT.Inventory.actualBlockMass_zero_pos line 233
  33. lemma OAI.FKCRT.Inventory.inventorySeries_pgf line 237
  34. lemma OAI.FKCRT.Inventory.actual_block_series line 245
  35. lemma OAI.FKCRT.Inventory.actual_inverse_equation line 259

    Source documentation

    The actual connected-core coefficients satisfy precisely the normalized inverse equation required by the analytic criticality proof.

    lemma actual_inverse_equation (P : Parameters) {x : ℝ} (hx : 0 ≤ x) (hx' : x ≤ 1) :
    HasSum (fun m => actualBlockMass P m*(x*((emptyWeights P).pgf x)^2)^m)
      ((emptyWeights P).pgf x) := by
…

    Mentions: OAI.FKCRT.Inventory.Parameters, OAI.FKCRT.Inventory.actualBlockMass, OAI.FKCRT.Inventory.emptyWeights

  36. def OAI.FKCRT.Inventory.criticalApproach line 275
  37. lemma OAI.FKCRT.Inventory.criticalApproach_bounds line 277
  38. lemma OAI.FKCRT.Inventory.criticalApproach_tendsto line 285
  39. theorem OAI.FKCRT.Inventory.actual_block_moments line 294

    Source documentation

    Criticality and the finite second moment for the genuine block series. The only assumptions are the original p∈(1/2,1); no block-law or moment conclusion is postulated.

    theorem actual_block_moments (P : Parameters) :
    HasSum (actualBlockMass P) 1 ∧
      HasSum (fun m : ℕ => (m:ℝ)*actualBlockMass P m) (1/2) ∧
      Summable (fun m : ℕ => (m:ℝ)^2*actualBlockMass P m) := by
…

    Mentions: OAI.FKCRT.Inventory.Parameters, OAI.FKCRT.Inventory.actualBlockMass

  40. def OAI.FKCRT.BlockCritical.doubleMass line 315
  41. lemma OAI.FKCRT.BlockCritical.doubleMass_even line 317
  42. lemma OAI.FKCRT.BlockCritical.doubleMass_outside line 320
  43. lemma OAI.FKCRT.BlockCritical.doubleMass_nonneg line 326
  44. lemma OAI.FKCRT.BlockCritical.hasSum_doubleMass line 332
  45. lemma OAI.FKCRT.BlockCritical.hasSum_doubleMean line 337
  46. lemma OAI.FKCRT.BlockCritical.summable_doubleSecond line 344
  47. def OAI.FKCRT.BlockCritical.evenOffspring line 355

    Source documentation

    Doubling block edge counts gives exactly the corner offspring law. The support span is two, and sizes in the tree theorem are all 2n+1.

    def evenOffspring (b : Weights) (h₀ : 0<b.mass 0) (h₁ : 0<b.mass 1)
    (hm : HasSum (fun k : ℕ => (k:ℝ)*b.mass k) (1/2))
    (hs : Summable (fun k : ℕ => (k:ℝ)^2*b.mass k)) : TreeCoding.CriticalEvenOffspring where
…

    Mentions: OAI.FKCRT.BlockCritical.Weights, OAI.FKCRT.TreeCoding.CriticalEvenOffspring

  48. theorem OAI.FKCRT.BlockCritical.block_joint_coding line 372

    Source documentation

    The exact normalized analytic criterion feeds the proved source joint excursion invariance theorem, with neither criticality nor finite variance postulated separately. This is a dependency lemma, not the FK main.

    theorem block_joint_coding (p : Weights) {b : ℕ → ℝ}
    (hb : ∀ k,0≤b k) (hb₀ : 0<b 0) (hb₁ : 0<b 1)
    {x : ℕ → ℝ} (hx : ∀ n,0≤x n ∧ x n<1) (ht : Tendsto x atTop (𝓝 1))
    (heq : ∀ n,HasSum (fun k => b k*(x n*(p.pgf (x n))^2)^k) (p.pgf (x n)))
    {c : ℝ} (hc : 0<c) (hlower : ∀ n,c≤Real.sqrt (1-x n)*p.abelMean (x n)) :
    ∃ offspring : TreeCoding.CriticalEvenOffspring,
      offspring.mass=doubleMass b ∧ TreeCoding.JointCodingStatement offspring := by
…

    Mentions: OAI.FKCRT.BlockCritical.Weights, OAI.FKCRT.TreeCoding.CriticalEvenOffspring, OAI.FKCRT.BlockCritical.doubleMass, OAI.FKCRT.TreeCoding.JointCodingStatement

  49. lemma OAI.FKCRT.Inventory.oneLink_core line 395

    Source documentation

    The true one-link word is a connected core, including its root seam.

    lemma oneLink_core : CoreWord [TypedLetter.burger true,TypedLetter.order true] := by
…

    Mentions: OAI.FKCRT.Inventory.CoreWord

  50. lemma OAI.FKCRT.Inventory.coreCoefficientReal_one_pos line 420
  51. lemma OAI.FKCRT.Inventory.actualBlockMass_one_pos line 429
  52. def OAI.FKCRT.Inventory.actualOffspring line 437

    Source documentation

    The actual corner offspring distribution, not an abstract replacement.

    def actualOffspring (P : Parameters) : FKCRT.TreeCoding.CriticalEvenOffspring :=
…

    Mentions: OAI.FKCRT.Inventory.Parameters, OAI.FKCRT.TreeCoding.CriticalEvenOffspring

  53. theorem OAI.FKCRT.Inventory.actual_offspring_joint_coding line 446

    Source documentation

    The proved invariance theorem is instantiated by the genuine core coefficients, under precisely the original phase parameter range. Finite FK map metric transport is a separate remaining obligation.

    theorem actual_offspring_joint_coding (P : Parameters) :
    FKCRT.TreeCoding.JointCodingStatement (actualOffspring P) :=
…

    Mentions: OAI.FKCRT.Inventory.Parameters, OAI.FKCRT.TreeCoding.JointCodingStatement, OAI.FKCRT.Inventory.actualOffspring

  54. def OAI.FKCRT.Inventory.CoreTree.productMass line 462

    Source documentation

    Product of genuine root-core probabilities at every vertex.

    def productMass (t r τ : ℝ) : CoreTree→ℝ
  | leaf => 1/τ
  | branch c ts => (wordMonomial t (r*τ) c.val/τ)*∏ i,productMass t r τ (ts i)

    Mentions: OAI.FKCRT.Inventory.CoreTree, OAI.FKCRT.Inventory.wordMonomial

  55. lemma OAI.FKCRT.Inventory.CoreTree.productMass_nonneg line 466
  56. theorem OAI.FKCRT.Inventory.CoreTree.productMass_eq line 476

    Source documentation

    Exact cancellation of the τ powers, including every leaf. This is the pointwise branching density, not merely a generating-function identity.

    theorem productMass_eq (t r τ : ℝ) (hτ : τ≠0) (T : CoreTree) :
    T.productMass t r τ=wordMonomial t r T.word/τ := by
…

    Mentions: OAI.FKCRT.Inventory.T, OAI.FKCRT.Inventory.CoreTree, OAI.FKCRT.Inventory.wordMonomial

  57. lemma OAI.FKCRT.Inventory.wordMonomial_ofReal line 494
  58. lemma OAI.FKCRT.Inventory.inventorySeries_one line 499
  59. lemma OAI.FKCRT.Inventory.wordMonomial_hasSum line 502
  60. theorem OAI.FKCRT.Inventory.coreTree_productMass_hasSum line 523

    Source documentation

    The genuine finite core trees carry total branching mass one. This also establishes extinction of this actual branching construction without adding an extinction or GW identification as a premise.

    theorem coreTree_productMass_hasSum (P : Parameters) :
    HasSum (CoreTree.productMass (flexParameter P) (Real.sqrt (radiusParameter P)) (emptyTotal P)) 1 := by
…

    Mentions: OAI.FKCRT.Inventory.Parameters, OAI.FKCRT.Inventory.CoreTree.productMass, OAI.FKCRT.Inventory.flexParameter, OAI.FKCRT.Inventory.radiusParameter, OAI.FKCRT.Inventory.emptyTotal

  61. def OAI.FKCRT.Inventory.CoreTree.shape line 544
  62. lemma OAI.FKCRT.Inventory.CoreTree.shape_degrees line 548
  63. lemma OAI.FKCRT.Inventory.CoreTree.degrees_excursion line 558
  64. abbrev OAI.FKCRT.Inventory.CoreTree.LabelExcursion line 563
  65. def OAI.FKCRT.Inventory.CoreTree.labelEquiv line 566
  66. def OAI.FKCRT.Inventory.CoreLabel.mass line 577
  67. lemma OAI.FKCRT.Inventory.CoreLabel.mass_nonneg line 581
  68. lemma OAI.FKCRT.Inventory.CoreTree.productMass_labels line 591
  69. theorem OAI.FKCRT.Inventory.CoreTree.labels_product_eq_word line 602

    Source documentation

    Exact pointwise GW branching weight in the faithful preorder coding.

    theorem labels_product_eq_word (t r τ : ℝ) (hτ : τ≠0) (l : LabelExcursion) :
    (l.val.map (CoreLabel.mass t r τ)).prod=
      wordMonomial t r (labelEquiv.symm l).word/τ := by
…

    Mentions: OAI.FKCRT.Inventory.CoreTree.LabelExcursion, OAI.FKCRT.Inventory.CoreLabel.mass, OAI.FKCRT.Inventory.wordMonomial, OAI.FKCRT.Inventory.CoreTree.word

  70. lemma OAI.FKCRT.Inventory.coreMass_finite_sum line 621

    Source documentation

    The actual connected-core contribution in each fixed edge-size fiber.

    lemma coreMass_finite_sum (P : Parameters) (m : ℕ) :
    (∑ w∈(typedEmptyWords (2*m)).filter CoreWord,
      ENNReal.ofReal (wordMonomial (flexParameter P)
        (Real.sqrt (radiusParameter P)*emptyTotal P) w/emptyTotal P))=
    ENNReal.ofReal (coreCoefficientReal (flexParameter P) m*
      (radiusParameter P*(emptyTotal P)^2)^m/emptyTotal P) := by
…

    Mentions: OAI.FKCRT.Inventory.Parameters, OAI.FKCRT.Inventory.typedEmptyWords, OAI.FKCRT.Inventory.CoreWord, OAI.FKCRT.Inventory.wordMonomial, OAI.FKCRT.Inventory.flexParameter, OAI.FKCRT.Inventory.radiusParameter, OAI.FKCRT.Inventory.emptyTotal, OAI.FKCRT.Inventory.coreCoefficientReal

  71. lemma OAI.FKCRT.Inventory.coreMass_by_size line 649

    Source documentation

    Grouping is over genuine normalized connected cores, with no abstract counting coefficients left in the summands.

    lemma coreMass_by_size (P : Parameters) (F : ℕ→ℝ≥0∞) :
    (∑' c : Core,ENNReal.ofReal (wordMonomial (flexParameter P)
      (Real.sqrt (radiusParameter P)*emptyTotal P) c.val/emptyTotal P)*F c.val.length)=
    ∑' m : ℕ,ENNReal.ofReal (coreCoefficientReal (flexParameter P) m*
      (radiusParameter P*(emptyTotal P)^2)^m/emptyTotal P)*F (2*m) := by
…

    Mentions: OAI.FKCRT.Inventory.Parameters, OAI.FKCRT.Inventory.Core, OAI.FKCRT.Inventory.wordMonomial, OAI.FKCRT.Inventory.flexParameter, OAI.FKCRT.Inventory.radiusParameter, OAI.FKCRT.Inventory.emptyTotal, OAI.FKCRT.Inventory.coreCoefficientReal

  72. def OAI.FKCRT.Inventory.CoreLabel.rootMass line 676
  73. lemma OAI.FKCRT.Inventory.CoreLabel.rootMass_nonneg line 679
  74. lemma OAI.FKCRT.Inventory.CoreLabel.rootMass_by_size line 682
  75. lemma OAI.FKCRT.Inventory.CoreLabel.rootMass_total line 703
  76. def OAI.FKCRT.Inventory.CoreLabel.rootLaw line 711
  77. lemma OAI.FKCRT.Inventory.CoreLabel.rootLaw_by_size line 714
  78. theorem OAI.FKCRT.Inventory.CoreLabel.rootLaw_arity line 737

    Source documentation

    The true root core has the already proved critical offspring marginal.

    theorem rootLaw_arity (P : Parameters) : (rootLaw P).map arity=(actualOffspring P).law := by
…

    Mentions: OAI.FKCRT.Inventory.Parameters, OAI.FKCRT.Inventory.CoreLabel.rootLaw, OAI.FKCRT.Inventory.CoreLabel.arity, OAI.FKCRT.Inventory.actualOffspring, OAI.FKCRT.Inventory.law