IntervalSelfLinks.lean`

28 declarations, 0 contain sorry, 0 declared as axioms

Finite combinatorial and numerical bounds: occurrence pairings, layer-cake stage counts and selection of one small stage. None of the graph existence, matching estimates or topological assertions is an assumption here.

def OAI.TorsionFreeZeroDivisors.IntervalSelfLinks.selfSlice line 12
Source documentation
Integer positions of one actual comparison within a single block.
```
def selfSlice (L U l u : ℤ) (rev : Bool) (a : ℤ) : Finset ℤ :=
…
```
theorem OAI.TorsionFreeZeroDivisors.IntervalSelfLinks.reflection_slice line 16
theorem OAI.TorsionFreeZeroDivisors.IntervalSelfLinks.translation_slice line 24

theorem OAI.TorsionFreeZeroDivisors.IntervalSelfLinks.reflection_not_large line 33

Source documentation

No reversed self-link on a reduced word can cover more than half a block.

theorem reflection_not_large {A : Type*} (bar : A → A)
    (hbar : Function.Involutive bar) (hfree : ∀ x, bar x ≠ x)
    (w : ℤ → A) (L U l u a : ℤ)
    (hred : ∀ q, L ≤ q → q+1 < U → w (q+1) ≠ bar (w q))
    (hcompare : ∀ q ∈ selfSlice L U l u true a, w q = bar (w (a-1-q))) :
    2*(selfSlice L U l u true a).card ≤ (Finset.Ico L U).card := by
…

Mentions: OAI.TorsionFreeZeroDivisors.IntervalSelfLinks.selfSlice

theorem OAI.TorsionFreeZeroDivisors.IntervalSelfLinks.translation_from_slice line 58

Source documentation

The precise translation constraints retained by a self-link, with its literal compared-position cardinality and no additional independence premise.

theorem translation_from_slice (L U l u a : ℤ) (ha : a ≠ 0) :
    ∃ tr : BlockConstraints.Translation (U-L).toNat,
      tr.domain.card = (selfSlice L U l u false a).card ∧
      ∀ (A : Type*) (w : Fin (U-L).toNat → A),
        (∀ q (hq : q ∈ selfSlice L U l u false a),
          w (coordinate L U ⟨q+a,by simpa [selfSlice] using (Finset.mem_filter.mp hq).2⟩) =
            w (coordinate L U ⟨q,(Finset.mem_inter.mp (Finset.mem_filter.mp hq).1).1⟩)) →
          ∀ k : tr.domain, w (tr.target k) = w k.val := by
…

Mentions: OAI.TorsionFreeZeroDivisors.BlockConstraints.Translation, OAI.TorsionFreeZeroDivisors.IntervalSelfLinks.selfSlice, OAI.TorsionFreeZeroDivisors.IntervalSelfLinks.coordinate

def OAI.TorsionFreeZeroDivisors.IntervalSelfLinks.coordinateN line 72
Source documentation
The same increasing coordinate, transported along the exact cardinality.
```
def coordinateN (L U : ℤ) (n : ℕ) (hn : n = (U-L).toNat) :
    Finset.Ico L U ≃ Fin n := (coordinate L U).trans (finCongr hn.symm)
```
Mentions: OAI.TorsionFreeZeroDivisors.IntervalSelfLinks.coordinate
theorem OAI.TorsionFreeZeroDivisors.IntervalSelfLinks.coordinateN_val line 75
theorem OAI.TorsionFreeZeroDivisors.IntervalSelfLinks.translation_from_slice_at line 79
abbrev OAI.TorsionFreeZeroDivisors.EntropyStages.Pairing.Unmatched line 107
theorem OAI.TorsionFreeZeroDivisors.EntropyStages.Pairing.color_balance line 111
Source documentation
The exact link balance, including isolated blocks and multiple links. A self-link is excluded only in the component where the bound is used.
```
theorem color_balance (color : O → C) (c : C)
    (hcross : ∀ o, P.partner o ≠ o → color (P.partner o) ≠ color o) :
    2 * Fintype.card {o : O // color o = c} ≤
      Fintype.card O + Fintype.card P.Unmatched := by
…
```
theorem OAI.TorsionFreeZeroDivisors.EntropyStages.stage_sum line 146
Source documentation
Exact finite layer-cake identity. Stage j+1 is present precisely when j is smaller than the occurrence multiplicity.
```
theorem stage_sum (M k : ℕ) (hk : k ≤ M) (a : ℝ) :
    (∑ j ∈ Finset.range M, if j < k then a else 0) = k * a := by
…
```
theorem OAI.TorsionFreeZeroDivisors.EntropyStages.sum_stage_costs line 158
Source documentation
Multiplying the numerical stage bounds is equivalent to summing their logarithms; their shared edge/word costs are counted with multiplicity.
```
theorem sum_stage_costs {I : Type*} [Fintype I]
    (M : ℕ) (m : I → ℕ) (hm : ∀ i, m i ≤ M) (d : I → ℝ) :
    (∑ j ∈ Finset.range M, ∑ i, if j < m i then d i else 0) =
      ∑ i, (m i : ℝ) * d i := by
…
```
theorem OAI.TorsionFreeZeroDivisors.EntropyStages.select_stage line 167
Source documentation
A bound for the product of numerical stage estimates selects one stage; no independence between the random variables at different stages is used.
```
theorem select_stage (M : ℕ) (hM : 0 < M) (logB : Fin M → ℝ) (decay : ℝ)
    (hprod : (∑ j, logB j) ≤ -decay) :
    ∃ j, logB j ≤ -decay / M := by
…
```

theorem OAI.TorsionFreeZeroDivisors.EntropyStages.select_exponential_stage line 181

Source documentation

Markov/union-bound conclusions can use this exponential version directly.

theorem select_exponential_stage (M : ℕ) (hM : 0 < M) (logB : Fin M → ℝ)
    (decay : ℝ) (hprod : (∑ j, logB j) ≤ -decay) :
    ∃ j, Real.exp (logB j) ≤ Real.exp (-decay / M) := by
…

theorem OAI.TorsionFreeZeroDivisors.component_cost_bound line 193

Source documentation

The cost estimate for a component without a self-link, with the lower bin bound and unmatched-occurrence correction.

theorem component_cost_bound {J : Type*} [Fintype J]
    (m d : J → ℝ) (dmin δ s a₀ z b : ℝ)
    (hm : ∀ i, 0 ≤ m i) (hmin : ∀ i, dmin ≤ d i)
    (hlow : δ * s / 2 ≤ dmin) (hhigh : dmin ≤ a₀ * s)
    (hδ : 0 ≤ δ) (hs : 0 ≤ s) (ha : 0 ≤ a₀) (hb : 0 ≤ b)
    (hbalance : 2 * z ≤ (∑ i, m i) + b) :
    -(∑ i, m i * d i) + 2 * z * dmin - δ * s * z ≤
      a₀ * s * b - δ / 2 * s * (∑ i, m i) := by
…

theorem OAI.TorsionFreeZeroDivisors.selflinked_component_cost_bound line 220

Source documentation

A self-link removes the root-word entropy. The remaining cost has the same decay term, with no unmatched-occurrence correction.

theorem selflinked_component_cost_bound {J : Type*} [Fintype J]
    (m d : J → ℝ) (δ s : ℝ) (hm : ∀ i, 0 ≤ m i)
    (hlow : ∀ i, δ * s / 2 ≤ d i) :
    -(∑ i, m i * d i) ≤ -δ / 2 * s * (∑ i, m i) := by
…

theorem OAI.TorsionFreeZeroDivisors.StageFusion.layers line 238
Source documentation
Layer-cake identity in the Fin M indexing of the selected stages.
```
theorem layers (M k : ℕ) (hk : k ≤ M) (a : ℝ) :
    (∑ j : Fin M, if j.val < k then a else 0) = k*a := by
…
```
def OAI.TorsionFreeZeroDivisors.StageFusion.componentCost line 246

theorem OAI.TorsionFreeZeroDivisors.StageFusion.total_component_cost line 253

Source documentation

The component costs added together. Every condition here is the local bin/link balance, not an assumed probability or conclusion.

theorem total_component_cost (self : C → Prop) [DecidablePred self]
    (m : ∀ c, I c → ℕ) (d : ∀ c, I c → ℝ) (z : C → ℕ)
    (dmin b : C → ℝ) (δ s a : ℝ)
    (hδ : 0 ≤ δ) (hs : 0 ≤ s) (ha : 0 ≤ a) (hb : ∀ c, 0 ≤ b c)
    (hlow : ∀ c i, δ*s/2 ≤ d c i)
    (hmin : ∀ c, ¬self c → ∀ i, dmin c ≤ d c i)
    (hminlow : ∀ c, ¬self c → δ*s/2 ≤ dmin c)
    (hminhigh : ∀ c, ¬self c → dmin c ≤ a*s)
    (hbalance : ∀ c, ¬self c → 2*(z c : ℝ) ≤ (∑ i, (m c i : ℝ)) + b c) :
    (∑ c, componentCost self m d z dmin δ s c) ≤
      a*s*(∑ c, b c) - δ/2*s*(∑ c, ∑ i, (m c i : ℝ)) := by
…

Mentions: OAI.TorsionFreeZeroDivisors.StageFusion.componentCost

def OAI.TorsionFreeZeroDivisors.StageFusion.stageLog line 282

Source documentation

Exact logarithm of a numerical stage bound. power is V_j-E_j-k_j; err contains the independently controlled endpoint/block errors.

def stageLog (M : ℕ) (self : C → Prop) [DecidablePred self]
    (m : ∀ c, I c → ℕ) (d : ∀ c, I c → ℝ) (z : C → ℕ)
    (dmin : C → ℝ) (δ s logn : ℝ) (power err : Fin M → ℝ) (j : Fin M) : ℝ :=
…

theorem OAI.TorsionFreeZeroDivisors.StageFusion.sum_stageLog line 290

Source documentation

No multiplication of random variables: this is solely an identity between finite sums of logs of bounds and finite sums of local component costs.

theorem sum_stageLog (M : ℕ) (self : C → Prop) [DecidablePred self]
    (m : ∀ c, I c → ℕ) (d : ∀ c, I c → ℝ) (z : C → ℕ)
    (hm : ∀ c i, m c i ≤ M) (hz : ∀ c, z c ≤ M)
    (dmin : C → ℝ) (δ s logn : ℝ) (power err : Fin M → ℝ) :
    (∑ j, stageLog M self m d z dmin δ s logn power err j) =
      (∑ j, power j)*logn + (∑ c, componentCost self m d z dmin δ s c) + ∑ j, err j := by
…

Mentions: OAI.TorsionFreeZeroDivisors.StageFusion.stageLog, OAI.TorsionFreeZeroDivisors.StageFusion.componentCost

def OAI.TorsionFreeZeroDivisors.StageFusion.epsilon line 319
Source documentation
The error threshold is fixed using only the universal weight constants.
```
def epsilon (δ a : ℝ) : ℝ := min (1/4) (δ/(16*(1+a)))
```
theorem OAI.TorsionFreeZeroDivisors.StageFusion.epsilon_pos line 321
theorem OAI.TorsionFreeZeroDivisors.StageFusion.absorb_errors line 326
Source documentation
Deterministic final absorption of the unmatched mass and sublinear errors.
```
theorem absorb_errors {δ a H b e : ℝ} (hδ : 0 < δ) (ha : 0 ≤ a) (hH : 0 ≤ H)
    (hb : b ≤ epsilon δ a * H) (he : e ≤ δ*H/8) :
    -δ/2*H + a*b + e ≤ -δ*H/4 := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.StageFusion.epsilon

theorem OAI.TorsionFreeZeroDivisors.StageFusion.markov_count line 349

Source documentation

Elementary finite Markov bound, including sample restriction.

theorem markov_count (Bad : Ω → Prop) [DecidablePred Bad] (X : Ω → ℕ)
    (hX : ∀ ω ∈ sample, Bad ω → 1 ≤ X ω) :
    ((sample.filter Bad).card : ℝ) / sample.card ≤
      ((∑ ω ∈ sample, X ω : ℕ) : ℝ) / sample.card := by
…

theorem OAI.TorsionFreeZeroDivisors.StageFusion.one_pattern line 364

Source documentation

Select a single numerical stage for each pattern. No independence is a premise, and the chosen stage can depend on the pattern.

theorem one_pattern (M : ℕ) (hM : 0 < M) (Bad : Ω → Prop) [DecidablePred Bad]
    (X : Fin M → Ω → ℕ) (logB : Fin M → ℝ) (decay : ℝ)
    (hX : ∀ j ω, ω ∈ sample → Bad ω → 1 ≤ X j ω)
    (hexpect : ∀ j, ((∑ ω ∈ sample, X j ω : ℕ) : ℝ) / sample.card ≤ Real.exp (logB j))
    (hproduct : (∑ j, logB j) ≤ -decay) :
    ((sample.filter Bad).card : ℝ) / sample.card ≤ Real.exp (-decay/M) := by
…

theorem OAI.TorsionFreeZeroDivisors.StageFusion.pattern_union line 375

Source documentation

Union bound over the enlarged unlabelled patterns.

theorem pattern_union (Bad : P → Ω → Prop) [∀ p, DecidablePred (Bad p)] (B : ℝ)
    (hB : ∀ p, ((sample.filter (Bad p)).card : ℝ) / sample.card ≤ B) :
    ((sample.filter (fun ω => ∃ p, Bad p ω)).card : ℝ) / sample.card ≤
      (Fintype.card P : ℝ)*B := by
…

theorem OAI.TorsionFreeZeroDivisors.StageFusion.subexponential_union line 399

Source documentation

Explicit finite version of exp(o(L)) times exponential decay.

theorem subexponential_union {N : ℕ} {δ M L error : ℝ}
    (_hM : 0 < M) (_hδ : 0 ≤ δ)
    (hN : (N : ℝ) ≤ Real.exp error) (he : error ≤ δ*L/(8*M)) :
    (N : ℝ)*Real.exp (-δ*L/(4*M)) ≤ Real.exp (-δ*L/(8*M)) := by
…