SiteTailCalibration

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

Elementary bounds used by site-tail calibration

This module retains the two dimension and gate-factor bounds shared with the active calibration modules.

Elementary bounds

theorem Algsuperdiff.Section5.Support.one_le_shiftFactor (d : ℕ) : 1 ≤ 3 ^ (sitePathExponent * ↑(Section3.Provider.Percolation.sepShift d))

The shift factor 3^{a · sepShift d} is at least one.

theorem Algsuperdiff.Section5.Support.one_le_gateBracket (Cpath : ℝ) : 1 ≤ 1 + Real.log 3 + (16 * Cpath) ^ 2

The bracket of the constant is at least one.