BadEventFrozenApplication

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

The per-cube bad-event tail at the dimension floor, from the frozen estimate

This module consumes Algsuperdiff.Frozen.Section3.bad_event_estimate and delivers the per-cube tail at a constant that clears the dimension floor (d : ℝ) ^ 6, which is what the Section 3.4 good-event display needs. It is the consuming half of the scale-shift bridge whose geometric core is Provider.Diffusivity.ApproximateRecurrence.BadEventScaleShiftBridge.

The mechanism

The frozen export publishes only 1 ≤ Ccg, and goodLocalEvent is not monotone in that constant. The bridge trades the constant against the cube scale: with k := badEventScaleShiftExp d = 6 d,

good (2 Ccg, cu_m, n) ∩ good (2 Ccg, cu_{m + 2k}, n) ⊆ good (2 · 3^k · Ccg, cu_m, n)

(goodLocalEvent_inter_subset_scaleShift_le), and 3 ^ k ≥ (d : ℝ) ^ 6 (dim_pow_six_le_three_pow_scaleShiftExp). The frozen export is applied twice at the same translate triadicCubeShift R, once at the cube scale R.scale and once at the enlarged scale R.scale + 2 k, and the union bound produces the factor 2 that the consumer absorbs through its Hoelder 3/8 power.

The two guarded rate gates

The first application sits in the ¬ (n < m) regime, so both of its guarded gates are vacuous. The second one need not: the Section 3.4 grid is indexed by a free recurrence multiplier a ≤ 32, and at a = 0 the cube scale equals the field scale, leaving no headroom at all. The two gates are therefore discharged on their own terms, using only R.scale ≤ n, which caps the enlarged gap at m - n ≤ 2 k:

• the rate gate 3 ^ (5 (m - n)) ≤ c · cstar · gamma⁻¹ follows from the admissibility premise c⁻¹ cstar⁻¹ ≤ E ≤ gamma⁻¹ once the exported c is the dimension-only shrink c₀ · 3 ^ (-12 k);
• the ellipticity gate d (m - n) log 3 + exp (X / 8) ≤ exp (X / 4), X := Ccg⁻¹ E⁻² gamma⁻¹, follows from u ^ 2 + exp u ≤ exp (2 u) at u = X / 8 once X is above the dimension-only threshold Kgate := 40 (d + k + 1) Ccg, which is exported as a binder and discharged by the consumer from its own window premise.

Both gates are derived, never assumed of the source: Kgate is an exported existential witness, and the consumer discharges Kgate ≤ E⁻² gamma⁻¹ from the window premise gamma / 2 + exp (-(C⁻¹ E⁻² gamma⁻¹)) ≤ gamma at its own enlarged constant C.

References

• ABK26, l.bad.event.lemma; e.good.local.events.
• The gate R.scale + 2 k ≤ n that §5.3 proposes is not available at the consumer, whose public statement quantifies the recurrence multiplier freely; the two gates are discharged non-vacuously instead, and no public statement changes.

One elementary exponential inequality

The frozen application

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.exists_badEventEstimate_perCube_dimFloor_ofFrozen (d : ℕ) : ∃ (Cbase : ℝ) (c : ℝ) (Kgate : ℝ), 1 ≤ Cbase ∧ ↑d ^ 6 ≤ Cbase ∧ 0 < c ∧ 0 < Kgate ∧ ∀ (M : ABKModel d) (m0 : ℤ) (E : { E : ℝ // 1 ≤ E }), Frozen.Section3.inductionState M (m0 - 1) E → c⁻¹ * (Disorder.cstar M)⁻¹ ≤ ↑E → ↑E ≤ M.gamma ^ (-(1 / 5)) → Kgate ≤ (↑E)⁻¹ ^ 2 * M.gamma⁻¹ → ∀ (R : HCPolySupport.TriadicCube d), ∀ n ≤ m0 - 1, R.scale ≤ n → (↑(Cutoff.cutoffSampleLaw M)).real (BadEvents.goodLocalEvent M (2 * Cbase) R n)ᶜ ≤ 2 * (Real.exp (-(c * Disorder.cstar M * M.gamma⁻¹ * 3 ^ (-5 * BadEvents.scaleGapPos n R.scale) * 3 ^ BadEvents.scaleGapPos R.scale n)) + Real.exp (-Real.exp (c * (↑E)⁻¹ ^ 2 * M.gamma⁻¹)))

The per-cube bad-event tail at a floor-normalized constant, derived from the frozen Algsuperdiff.Frozen.Section3.bad_event_estimate.

The frozen export is applied twice at the same translate triadicCubeShift R, once at the cube scale R.scale and once at the enlarged scale R.scale + 2 * badEventScaleShiftExp d; the scale-shift inclusion turns the two events into the single event at the enlarged constant 2 * 3 ^ k * Ccg, whose floor (d : ℝ) ^ 6 is cleared by dim_pow_six_le_three_pow_scaleShiftExp, and the union bound produces the factor 2.

The exported Kgate is a dimension-only lower threshold on E⁻² gamma⁻¹: it is what discharges the frozen ellipticity gate at the enlarged scale, and the consumer derives it from its own window premise.

: this statement holds only under the propositions supplied by its binders. It is a provider A, not a source-facing frozen declaration.