GridUniform.lean`

24 declarations, 0 contain sorry, 0 declared as axioms

def OAI.TorsionFreeZeroDivisors.GridUniform.rate line 12
theorem OAI.TorsionFreeZeroDivisors.GridUniform.rate_nonneg line 15
theorem OAI.TorsionFreeZeroDivisors.GridUniform.rate_tendsto line 19

theorem OAI.TorsionFreeZeroDivisors.GridUniform.bounds line 29

Source documentation

A single offset-independent rate controls every scalar rounding loss.

theorem bounds (d : ℕ) {L : ℝ} (hL : 1≤L) (offset : Fin d → ℤ) :
    chosenScale d L offset/L ≤ rate d L ∧
    1/chosenScale d L offset ≤ rate d L ∧
    (letterError d L offset:ℝ)/chosenScale d L offset ≤ 5*rate d L ∧
    1/L ≤ rate d L := by
…

Mentions: OAI.TorsionFreeZeroDivisors.GridUniform.rate

theorem OAI.TorsionFreeZeroDivisors.GridUniform.eventually_geometry line 59
Source documentation
Unlike a chosen offset sequence, this statement is uniform over ALL integer comparison offsets at each common length scale.
```
theorem eventually_geometry (d : ℕ) : ∀ᶠ L in atTop, ∀ offset : Fin d → ℤ,
    3003 ≤ chosenScale d L offset ∧
    2*(letterError d L offset:ℝ) < chosenScale d L offset-1 := by
…
```
def OAI.TorsionFreeZeroDivisors.StageUniform.alphabetLog line 78
theorem OAI.TorsionFreeZeroDivisors.StageUniform.alphabetLog_nonneg line 80
def OAI.TorsionFreeZeroDivisors.StageUniform.coefficient line 84

theorem OAI.TorsionFreeZeroDivisors.StageUniform.scalar_bound line 89

Source documentation

Uniform scalar estimate. Its inputs are just the explicit common-grid loss bounds, not an entropy or probability estimate.

theorem scalar_bound (D K M Q : ℕ) (L s H blocks err rate den : ℝ)
    (hL : 0 < L) (hs : 0 < s) (_hH : 0 ≤ H) (hb : 0 ≤ blocks)
    (hr : 0 ≤ rate) (hscale : s/L≤ rate) (hinv : 1/s≤ rate)
    (hone : 1/L≤ rate) (he : err/s≤5*rate)
    (hsize : H≤K*L) (hblocks : s*blocks≤K*L) :
    (256*(22*s*D+H/s)+(1/1200:ℝ)*s*M*Q+
      M*((2*err*blocks+(s+1)*Q)*alphabetLog+den))/L ≤
        coefficient D K M Q*rate+M*den/L := by
…

Mentions: OAI.TorsionFreeZeroDivisors.StageUniform.alphabetLog, OAI.TorsionFreeZeroDivisors.StageUniform.coefficient

theorem OAI.TorsionFreeZeroDivisors.StageUniform.residual_bound line 125
Source documentation
Specialization to the literal stage remainder: the ONLY scale-dependent upper bound is rate, which does not mention offsets or labelled words.
```
theorem residual_bound (K M Q : ℕ) (L : ℝ) (hL : 1≤L)
    (offset : Fin (Fintype.card E) → ℤ) (len m : C → ℕ) (hQ : Fintype.card C≤Q)
    (hH : StageMass.totalLength len m ≤ K*L) (hpositive : ∀ c,1≤ m c) (den : ℝ) :
    StageMass.residual (E := E) (chosenScale (Fintype.card E) L offset) len m
…
```
Mentions: OAI.TorsionFreeZeroDivisors.StageMass.totalLength, OAI.TorsionFreeZeroDivisors.StageMass.residual

theorem OAI.TorsionFreeZeroDivisors.StageUniform.eventually_residual line 163

Source documentation

All patterns of the stated fixed bounds share one threshold. No offset, chain length, bin, or word is fixed before this eventual quantifier.

theorem eventually_residual (K M Q : ℕ) : ∀ᶠ rep in atTop,
    ∀ (offset : Fin (Fintype.card E) → ℤ) (len m : C → ℕ),
      Fintype.card C ≤ Q → StageMass.totalLength len m ≤ K*(L (size rep):ℝ) →
      (L (size rep):ℝ) ≤ StageMass.totalLength len m → (∀ c,1 ≤ m c) →
      StageMass.residual (E := E) (chosenScale (Fintype.card E) (L (size rep)) offset) len m
…

Mentions: OAI.TorsionFreeZeroDivisors.StageMass.totalLength, OAI.TorsionFreeZeroDivisors.StageMass.residual

def OAI.TorsionFreeZeroDivisors.GridUniform.binRate line 192
theorem OAI.TorsionFreeZeroDivisors.GridUniform.binRate_tendsto line 194
theorem OAI.TorsionFreeZeroDivisors.GridUniform.scale_le line 206
theorem OAI.TorsionFreeZeroDivisors.GridUniform.bin_bound line 218
Source documentation
A single common-grid bound for the logarithm of the number of all bin profiles, without fixing any comparison offsets.
```
theorem bin_bound (d : ℕ) {L : ℝ} (hL : 1 ≤ L) (offset : Fin d → ℤ) :
    Real.log (256*chosenScale d L offset+1)/chosenScale d L offset ≤ binRate L := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.GridUniform.binRate
theorem OAI.TorsionFreeZeroDivisors.BinProfiles.height_bounds line 241
theorem OAI.TorsionFreeZeroDivisors.BinProfiles.feasible_bounds line 251
Source documentation
Feasible literal blocks obey BOTH entropy cutoffs and belong to the finite profile family. This includes the empty block carrier.
```
theorem feasible_bounds (s : ℝ) (hs : 3003 ≤ s) (len m : C → ℕ)
    (cmp : Comparisons (E := E) (traversalLength len m))
…
```
structure OAI.TorsionFreeZeroDivisors.RealizationTransport.Embedding line 275
Source documentation
An injective realization in a fixed sampled matching. These are actual maps on vertices and ports; no random-event bound is part of the data.
```
structure Embedding (Γ : PortGraph PV PD) (plabel : PD → T) (outgoing : TV → Finset T)
    (pin : PV → Option TV) (bar : T → T) (r : Matching (label outgoing) bar) where
…
```
theorem OAI.TorsionFreeZeroDivisors.RealizationTransport.immersed line 290
def OAI.TorsionFreeZeroDivisors.RealizationTransport.vertexMap line 302
theorem OAI.TorsionFreeZeroDivisors.RealizationTransport.dartMap_eq line 313
theorem OAI.TorsionFreeZeroDivisors.RealizationTransport.realizations_pos line 325
Source documentation
A literal embedding contributes at least one to the exact realization count. The event direction is explicit rather than postulated.
```
theorem realizations_pos : 0 < StageRealization.realizations Γ plabel outgoing pin bar r := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.StageRealization.realizations
def OAI.TorsionFreeZeroDivisors.RealizationTransport.pullback line 336
Source documentation
Graph isomorphisms, such as actual marked-chain subdivision, preserve all event data, including the root pin and exact directed labels.
```
def pullback (Γ' : PortGraph PV' PD') (eV : PV' ≃ PV) (eD : PD' ≃ PD)
    (ho : ∀ d,eV (Γ'.origin d)=Γ.origin (eD d))
    (hr : ∀ d,eD (Γ'.reverse d)=Γ.reverse (eD d)) :
    Embedding Γ' (plabel ∘ eD) outgoing (pin ∘ eV) bar r where
…
```
Mentions: OAI.TorsionFreeZeroDivisors.RealizationTransport.Embedding

theorem OAI.TorsionFreeZeroDivisors.TwoSideStage.count_pos line 355

Source documentation

Every actual globally compatible embedding is contained in the event counted by the two-side first moment.

theorem count_pos (A B : Side) (X : Finset W) (WA : W → A.Word) (WB : W → B.Word)
    (r : A.Match × B.Match) (w : W) (hw : w∈X)
    (eA : RealizationTransport.Embedding (ChainSubdivision.graph A.len A.first A.last)
      (ChainRealization.label A.len (StageExpectation.readWord A.len (WA w))) A.outgoing
      (ChainRealization.pin A.len A.pin) Types.inverse r.1)
    (eB : RealizationTransport.Embedding (ChainSubdivision.graph B.len B.first B.last)
      (ChainRealization.label B.len (StageExpectation.readWord B.len (WB w))) B.outgoing
      (ChainRealization.pin B.len B.pin) Types.inverse r.2) :
    0<count A B X WA WB r := by
…

Mentions: OAI.TorsionFreeZeroDivisors.TwoSideStage.Side, OAI.TorsionFreeZeroDivisors.RealizationTransport.Embedding, OAI.TorsionFreeZeroDivisors.ChainSubdivision.graph, OAI.TorsionFreeZeroDivisors.ChainRealization.label, OAI.TorsionFreeZeroDivisors.StageExpectation.readWord, OAI.TorsionFreeZeroDivisors.ChainRealization.pin, OAI.TorsionFreeZeroDivisors.Types.inverse, OAI.TorsionFreeZeroDivisors.TwoSideStage.count