EarlyExit

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

The canonical chain length and the Chernoff budget

The hit--exit bridge asks for a chain length below the usable trace count of a good cube. This file fixes the canonical choice — the usable count, after one reserved site, divided by the overlap multiplicity — and verifies its counting condition. It also carries the deterministic Chernoff calculation that turns a contraction bounded by exp (-kappa) together with a budget lam * t + b ≤ kappa * N into the decay exp (-b).

def Algsuperdiff.Section5.Provider.earlyExitTraceCount (d k : ℕ) : ℕ

The number of trace sites left after the two endpoint losses.

Equations

• Algsuperdiff.Section5.Provider.earlyExitTraceCount d k = 3 * 3 ^ k / 4 - 2 * d

def Algsuperdiff.Section5.Provider.earlyExitChainLength (d k : ℕ) : ℕ

The largest chain length obtained by dividing the usable trace count, after reserving one site, by the overlap multiplicity 3^d.

Equations

• Algsuperdiff.Section5.Provider.earlyExitChainLength d k = (Algsuperdiff.Section5.Provider.earlyExitTraceCount d k - 1) / 3 ^ d

theorem Algsuperdiff.Section5.Provider.earlyExitChainLength_mul_lt (d k : ℕ) (hcount : 0 < earlyExitTraceCount d k) : earlyExitChainLength d k * 3 ^ d < earlyExitTraceCount d k

The canonical chain length satisfies the strict counting condition of the hit--exit bridge whenever at least one trace site remains.

theorem Algsuperdiff.Section5.Provider.ofReal_exp_mul_pow_le_of_budget {lam t kappa b : ℝ} {rho : ENNReal} {N : ℕ} (hrho : rho ≤ ENNReal.ofReal (Real.exp (-kappa))) (hbudget : lam * t + b ≤ kappa * ↑N) : ENNReal.ofReal (Real.exp (lam * t)) * rho ^ N ≤ ENNReal.ofReal (Real.exp (-b))

The deterministic Chernoff calculation after chaining. A contraction bounded by exp (-kappa) and a budget lam * t + b ≤ kappa * N leave the decay exp (-b).