Pointwise and partial-sum consequences of the one global scale choice, ready for a finite-prefix packet induction.

theorem EulerPacketInductionScales.Scales.x_one {c B : ℝ} (S : Scales c B) : 1 ≤ S.X

theorem EulerPacketInductionScales.Scales.x_pos {c B : ℝ} (S : Scales c B) : 0 < S.X

theorem EulerPacketInductionScales.Scales.j_one {c B : ℝ} (S : Scales c B) : 1 ≤ S.J

theorem EulerPacketInductionScales.Scales.sequence_one {c B : ℝ} (S : Scales c B) (n : ℕ) : 1 ≤ EulerPacketSourceScaleChoice.scaleSequence S.J S.X n

theorem EulerPacketInductionScales.Scales.previousShear_one {c B : ℝ} (S : Scales c B) (n : ℕ) : 1 ≤ EulerPacketSourceScaleSequence.previousShear S.J S.X n

theorem EulerPacketInductionScales.Scales.shear_one {c B : ℝ} (S : Scales c B) (n : ℕ) : 1 ≤ EulerPacketSourceScaleSequence.shear S.J S.X n

theorem EulerPacketInductionScales.Scales.spike_pos {c B : ℝ} (S : Scales c B) (n : ℕ) : 0 < EulerPacketSourceScaleSequence.spike S.J S.X n

theorem EulerPacketInductionScales.Scales.spike_one {c B : ℝ} (S : Scales c B) (n : ℕ) : EulerPacketSourceScaleSequence.spike S.J S.X n ≤ 1

theorem EulerPacketInductionScales.Scales.support_pos {c B : ℝ} (S : Scales c B) (n : ℕ) : 0 < EulerPacketSourceScaleSequence.supportScale S.J S.X n

theorem EulerPacketInductionScales.Scales.support_one {c B : ℝ} (S : Scales c B) (n : ℕ) : EulerPacketSourceScaleSequence.supportScale S.J S.X n ≤ 1

theorem EulerPacketInductionScales.Scales.previousFrequency_one {c B : ℝ} (S : Scales c B) (n : ℕ) : 1 ≤ EulerPacketSourceScaleSequence.previousFrequency S.J S.D S.X n

theorem EulerPacketInductionScales.Scales.priorError_nonneg {c B : ℝ} (S : Scales c B) (n : ℕ) : 0 ≤ EulerPacketSourceScaleActual.priorError S.J S.D S.X n

theorem EulerPacketInductionScales.Scales.priorError_one {c B : ℝ} (S : Scales c B) (n : ℕ) : EulerPacketSourceScaleActual.priorError S.J S.D S.X n ≤ 1

theorem EulerPacketInductionScales.Scales.shear_separation {c B : ℝ} (S : Scales c B) (n : ℕ) : EulerPacketSourceScaleSequence.previousShear S.J S.X n ^ 2 ≤ EulerPacketSourceScaleSequence.shear S.J S.X n / 4

theorem EulerPacketInductionScales.Scales.olderShear_le {c B : ℝ} (S : Scales c B) (n : ℕ) : EulerPacketSourceScaleSequence.olderShear S.J S.X n ≤ EulerPacketSourceScaleSequence.previousShear S.J S.X n

theorem EulerPacketInductionScales.Scales.frequency_cost {c B : ℝ} (S : Scales c B) (n : ℕ) : (EulerNormalPacketParameters.frequencySpec 4).cost S.J (EulerPacketSourceScaleChoice.scaleSequence S.J S.X) n ≤ 1

theorem EulerPacketInductionScales.Scales.source_frequency {c B : ℝ} (S : Scales c B) (n : ℕ) (P : ℝ) (hP : 1 ≤ P) (hPE : P ≤ EulerNormalPacketParameters.envelope S.J 4 S.X n) : EulerPacketUniformSource.frequencyConstant * P ^ EulerPacketUniformSource.frequencyPower ≤ EulerPacketSourceFrequency.smallPower (EulerPacketSourceScaleSequence.frequency S.J S.X n)

theorem EulerPacketInductionScales.Scales.secondary_frequency {c B : ℝ} (S : Scales c B) (n : ℕ) (K : ℝ) (hK : K ≤ EulerPacketSourceScaleSequence.previousFrequency S.J S.D S.X n ^ 80) : K ≤ EulerPacketSourceScaleSequence.frequency S.J S.X n ∧ (EulerPacketSourceScaleSequence.supportScale S.J S.X n)⁻¹ ≤ EulerPacketSourceScaleSequence.frequency S.J S.X n ^ (3 / 4)

theorem EulerPacketInductionScales.Scales.initial_partial_sum {c B : ℝ} (S : Scales c B) (n : ℕ) : ∑ i ∈ Finset.range n, initialIncrement S.J S.X i ≤ 2 * S.δ

theorem EulerPacketInductionScales.Scales.pressure_partial_sum {c B : ℝ} (S : Scales c B) (n : ℕ) : ∑ i ∈ Finset.range n, pressureIncrement S.J S.X i ≤ 3 * S.δ

theorem EulerPacketInductionScales.Scales.activation_small {c B : ℝ} (S : Scales c B) {n : ℕ} (hn : n ≠ 0) : EulerPacketLowConstants.frameConstant * (1 + EulerPacketSourceScaleSequence.olderShear S.J S.X n) + EulerPacketSourceScaleActual.priorError S.J S.D S.X n ≤ activationMargin * EulerPacketSourceScaleSequence.previousShear S.J S.X n

theorem EulerPacketInductionScales.Scales.localized_guard {c B : ℝ} (S : Scales c B) (T K Be Bc : ℝ) (hT : 0 ≤ T) (hK : 0 ≤ K) (hBe : 0 ≤ Be) (hBc : 0 ≤ Bc) (hKcap : K ≤ EulerBaseDatum.initialCoefficientCost + 1) (hBecap : Be ≤ EulerBaseDatum.initialCoefficientCost + 1) (hBccap : Bc ≤ EulerPacketLowConstants.gradientConstant * S.X ^ 1000 + 2) (hTcap : T ≤ EulerPacketBaseGuardScales.baseHorizon S.J S.X) : K * (T ^ 2 / 2) + Be * T + EulerMeanHarmonic.boundaryLocalizationC2 * Bc * EulerPacketBaseGuardScales.baseRadius S.X ^ 3 * T ≤ 1 / 2