Documentation

LeanPool.Superdiffusion.Algsuperdiff.Section4.Provider.Regularity.RootClauseBFinalFunding

RootClauseBFinalFunding #

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

1. The C₁-floor form of the Step-6 gate #

source
noncomputable def Algsuperdiff.Section4.Provider.Regularity.rootClauseBFundFloor (d : ℕ) [NeZero d] (C Cann : ℝ) (k : ℕ) :
ℝ

The Step-6 funding floor (2·P·C_ann·(s/8)·3^{k/4})².

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Algsuperdiff.Section4.Provider.Regularity.edFunding_of_c1_floor (d : ℕ) [NeZero d] {C Cann C1 alpha : ℝ} {k : ℕ} (hC : 0 ≤ C) (hCann : 0 ≤ Cann) (halpha0 : 0 ≤ alpha) (hC1 : 0 < C1) (hfloor : rootClauseBFundFloor d C Cann k ≤ C1) :
    edFinalEpsCoeff d C k stepOneS * (Cann * stepOneEp (stepOneDelta C1 alpha)) ≤ 1 / 2 * 3 ^ (-(1 / 4) * ↑k)

    The Step-6 funding line from a pure C₁-floor.

    No division, and no positivity of edFinalEpsCoeff is needed: the whole argument is √δ ≤ (√C₁)⁻¹ followed by one cross-multiplication.

    2. The Step-1 δ-slot, evaluated #

    source
    theorem Algsuperdiff.Section4.Provider.Regularity.stepOneC1Delta0_eq {Cedos Cann : ℝ} (hCedos : 0 < Cedos) (hCann : 0 < Cann) (k : ℕ) :
    stepOneC1Delta0 Cedos Cann k = (2 * Cedos * Cann * stepOneThreePow k) ^ 2 / stepOneS

    The Step-1 C₁ slot, in closed form: stepOne C_edos C_ann k = (2 C_edos C_ann 3^{k/4})²/s.

    3. The floor, discharged at explicit constants #

    source
    noncomputable def Algsuperdiff.Section4.Provider.Regularity.rootClauseBFundCedos (d : ℕ) [NeZero d] (C Cann : ℝ) (k : ℕ) :
    ℝ

    The Step-1 excess-decay letter that funds the Step-6 gate: C_edos = max 1 (P·C_ann·(s/8)). It meets the printed floor 1 ≤ C_edos by construction.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Algsuperdiff.Section4.Provider.Regularity.one_le_rootClauseBFundCedos (d : ℕ) [NeZero d] (C Cann : ℝ) (k : ℕ) :
      1 ≤ rootClauseBFundCedos d C Cann k
      source
      theorem Algsuperdiff.Section4.Provider.Regularity.rootClauseBFundCedos_pos (d : ℕ) [NeZero d] (C Cann : ℝ) (k : ℕ) :
      0 < rootClauseBFundCedos d C Cann k
      source
      theorem Algsuperdiff.Section4.Provider.Regularity.rootClauseBFundFloor_le_stepOneC1 (d : ℕ) [NeZero d] {C Cann : ℝ} (hC : 0 ≤ C) (hCann : 0 ≤ Cann) (Citer : ℝ) (k : ℕ) :
      rootClauseBFundFloor d C Cann k ≤ stepOneC1 d (rootClauseBFundCedos d C Cann k) 1 Citer k

      The floor is met by the root's own C₁.

      stepOneC1 dominates its δ-slot, which at C_ann' = 1 and the explicit C_edos above equals 4·(2 C_edos 3^{k/4})² (because s = 1/4), and that dominates (2·P·C_ann·(s/8)·3^{k/4})².