UpperSaturatedOrdinaryComparison

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

Comparing the saturated and polynomial ordinary profiles

The strict-descendant saturated amplitude used for 1 ≤ q ≤ 2 is pointwise no larger than the polynomial ordinary amplitude used by the common envelope route for q ≥ 2. Thus one proved per-cube estimate at the saturated scale can feed both deterministic aggregation mechanisms.

This file supplies only that algebraic comparison. It proves no per-cube analytic estimate, does not treat the depth-zero/root row, and does not combine any random lanes.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.upperSaturatedPerCubeAmplitude_le_upperOrdinary {C cstar gamma : ℝ} (hC : 0 ≤ C) (hcstar : 0 ≤ cstar⁻¹) (k : ℕ) : upperSaturatedPerCubeAmplitude C cstar gamma k ≤ upperOrdinaryPerCubeAmplitude C cstar gamma k

The saturated strict-descendant scale is bounded by the polynomial ordinary scale with the same head constant.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.triadicJointDepthEntropyConst_mul_upperSaturatedPerCubeAmplitude_le_bound (d : ℕ) {C cstar gamma : ℝ} (hC : 0 ≤ C) (hcstar : 0 ≤ cstar⁻¹) (hgamma : 0 ≤ gamma) (hgamma1 : gamma ≤ 1) (k : ℕ) : triadicJointDepthEntropyConst d * (↑k + 1) * upperSaturatedPerCubeAmplitude C cstar gamma k ≤ upperPolyProfile (upperOrdinaryJointProfileBound d C cstar gamma) gamma k

Consequently the joint spatial-and-depth price of the saturated row fits the existing common-envelope polynomial profile. This remains an algebraic profile comparison, not a statement that an actual row has this amplitude.