RebaseEpsilon

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

The clause-threshold calculus

Conditional-free provider helpers, not a node realization. Everything in this module is arithmetic on the frozen good-event threshold ε = C⁻¹ s⁴ together with the proved ε-monotonicity of the good event (GoodEvents.goodEventAt_mono_ep). No analysis, no measure theory beyond a Set.indicator rewrite.

Exactly two literals of the frozen statement read C⁻¹ s⁴ rather than (1/2), at the statement's own existential constant:

• the hoisted γ-smallness funding line;
• the general clause's good-event threshold.

The interior clause's event stays at (1/2). Both read the same way, so passing from the (1/2) form to the C⁻¹ s⁴ form is a pure weakening; the four lemmas of §1--§3 are exactly the two directions that weakening needs, and §5 is the consumer-side re-pricing that lets the development's own good-scale supply ε = (s/8)√δ (and the minimal-scale anchor's ε = s√δ) reach the threshold.

References

• ABK26, l.harmonic.approximation.good.scales; the frozen block of Algsuperdiff/Section4/Provider/ExcessDecay/ProviderEpsFree.lean (read for the byte-verification, never imported).

1. The clause threshold is an admissible, sub-half ε

theorem Algsuperdiff.Section4.Provider.ExcessDecay.clauseEpsilon_nonneg {C s : ℝ} (hC : 0 < C) (hs : 0 ≤ s) : 0 ≤ C⁻¹ * s ^ 4

The frozen threshold is nonnegative — the left half of the proved goodEventAt_mono_ep side condition.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.clauseEpsilon_le_half {C s : ℝ} (hC : 2 ≤ C) (hs : 0 ≤ s) (hs1 : s ≤ 1) : C⁻¹ * s ^ 4 ≤ 1 / 2

The frozen threshold is at most 1/2, as soon as the statement's own existential constant is at least 2 and s ≤ 1.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.clauseEpsilon_anti {C C' s : ℝ} (hC : 0 < C) (hCC : C ≤ C') (hs : 0 ≤ s) : C'⁻¹ * s ^ 4 ≤ C⁻¹ * s ^ 4

The threshold is antitone in the constant: raising C shrinks the clause event. This is the whole reason a joint constant max _ _ can be handed to a producer stated at its own smaller constant.

2. The funding back-port

theorem Algsuperdiff.Section4.Provider.ExcessDecay.funding_le_of_epsilon_le {d : ℕ} {M : Section3.ABKModel d} {s ep ep' : ℝ} (hs : 0 < s) (hep : ep ≤ ep') (h : M.gamma * |Real.log M.gamma| ^ 2 ≤ (s / 8).rpow (3 / 2) * Section3.Disorder.cstar M ^ 2 * ep) : M.gamma * |Real.log M.gamma| ^ 2 ≤ (s / 8).rpow (3 / 2) * Section3.Disorder.cstar M ^ 2 * ep'

The back-port. The anchor's hoisted γ-smallness line is monotone in its trailing ε factor, so funding at the smaller C⁻¹ s⁴ threshold funds every larger one — in particular the literal (1/2) and the producer's own C₀⁻¹ s⁴.

This is DirectionProbe's hfund' step, isolated.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.regime_le_of_const_le {d : ℕ} {M : Section3.ABKModel d} {C C' : ℝ} (hC : 0 < C) (hCC : C ≤ C') (h : M.gamma ≤ C'⁻¹ * Section3.Disorder.cstar M ^ 10) : M.gamma ≤ C⁻¹ * Section3.Disorder.cstar M ^ 10

The standing regime hypothesis is back-ported the same way: it reads C⁻¹ directly, and C ≤ C' makes the C' form the stronger one.

3. The event and its indicator

theorem Algsuperdiff.Section4.Provider.ExcessDecay.indicator_goodEventAt_transfer {d : ℕ} {M : Section3.ABKModel d} {Ccg : ℝ} {j : ℤ} {y : HCPolySupport.Vec d} {t : { t : ℝ // 0 < t }} {ep ep₁ ep₂ : ℝ} {F : Section3.Cutoff.CutoffSample d → ENNReal} {B : ENNReal} {omega : Section3.Cutoff.CutoffSample d} (hep0 : 0 ≤ ep) (h1 : ep ≤ ep₁) (h2 : ep ≤ ep₂) (hmem : omega ∈ Frozen.Section4.goodEventAt M Ccg j y t ep) (h : (Frozen.Section4.goodEventAt M Ccg j y t ep₁).indicator F omega ≤ B) : (Frozen.Section4.goodEventAt M Ccg j y t ep₂).indicator F omega ≤ B

The slot transfer at a witnessed ω.

An indicator bound at one threshold ε₁ transfers to any other threshold ε₂, provided the sample ω is known to sit in the good event at a threshold ε below both. Off the event an indicator is 0; at a witnessed ω both indicators collapse to the same value F ω, so the transfer is free in both directions.

This is the mechanism that turns every proved (1/2)-gated hharm binder into its C⁻¹ s⁴-gated sibling, and back: the consumer always carries hmem.

4. The general clause's bracket

theorem Algsuperdiff.Section4.Provider.ExcessDecay.fourSummandBracket_nonneg {a b e f X c Y Z W : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (he : 0 ≤ e) (hf : 0 ≤ f) (hX : 0 ≤ X) (hc : 0 ≤ c) (hY : 0 ≤ Y) (hZ : 0 ≤ Z) (hW : 0 ≤ W) : 0 ≤ a * (X + c) + b * Y + e * Z + f * W

Nonnegativity of the frozen general clause's four-summand bracket, stated abstractly in the legs (so it is blind to every s-exponent the freeze moved). In-repo public sibling of the join lane's private bracket helper.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.fourSummandBracket_absorb {C₀ C t₁ t₂ t₃ t₄ : ℝ} (h : C₀ ≤ C) (h₁ : 0 ≤ t₁) (h₂ : 0 ≤ t₂) (h₃ : 0 ≤ t₃) (h₄ : 0 ≤ t₄) : C₀ * (t₁ + t₂ + t₃ + t₄) ≤ C * t₁ + C * t₂ + C * t₃ + C * t₄

Raising a four-summand real right-hand side from a producer's constant to the assembly's joint constant.

5. The δ re-pricing

theorem Algsuperdiff.Section4.Provider.ExcessDecay.sqrt_le_of_le_sq {a t : ℝ} (ha : 0 ≤ a) (h : t ≤ a ^ 2) : √t ≤ a

√t ≤ a from t ≤ a² at nonnegative a — the only square-root step the re-pricing needs.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.excessDecayEpsilon_le_clauseEpsilon {C s delta : ℝ} (hC : 0 < C) (hs : 0 ≤ s) (hdelta : delta ≤ (8 * C⁻¹ * s ^ 3) ^ 2) : s / 8 * √delta ≤ C⁻¹ * s ^ 4

The excess-decay consumer's supply reaches the clause event.

The development's good-scale supply is ε = (s/8)√δ (the printed good-event-cap slot). It sits below the frozen threshold exactly when δ ≤ (8 C⁻¹ s³)².

theorem Algsuperdiff.Section4.Provider.ExcessDecay.excessDecayDelta_repriced {C s delta : ℝ} (hC : 0 < C) (hs : 0 ≤ s) (hdelta : delta ≤ 64 * (C ^ 2)⁻¹ * s ^ 6) : s / 8 * √delta ≤ C⁻¹ * s ^ 4

The consumer's δ price, written out.

δ ≤ 64 C⁻² s⁶ is (8 C⁻¹ s³)² written out; at that price the good-scale supply feeds the general clause with no further analysis.