Big-bound estimate at the datum amplitude: the last closures and bigbound_of_remaining

The big-bound estimate needs every BigBoundInputs contract only at the datum amplitude B = ‖θ₀‖_{L²}.

• normie2Source_datum_closed_contract: normie2Source_contract with hmGradient_contract.
• vIncrement_datum_contract: the V upgrade (iterate_V_upgrade_of_theta) with the big-bound premise block θ profile at amplitude 2‖θ₀‖ (thetaProfileA7_contract), at a constant Cs large for both.
• tinyHMinusSource_datum_closed_contract: tinyHMinusSource_contract at B = 2‖θ₀‖ with sourceErrorD_contract, vIncrement_datum_contract, tinyMeanZero_contract, rescaled to ‖θ₀‖.
• bigbound_of_remaining: the literal big-bound estimate statement from a datum-amplitude Normie3CenteredSourceContract producer. bigbound_contract supplies the proved normie3CenteredSource_datum_closed_contract.

theorem AVenhance.Infra.Section5.Contracts.normie2Source_datum_closed_contract (β Ccut : ℝ) : ∃ (C : ℝ) (C₁ : ℝ), Integration.OnA7Instances β Ccut C₁ fun (I : Ingredients β) (_Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hΦ : IsStreamSeq I _Φ) (κ : ℝ) (M : ℕ) (_R : ℝ) (θ₀ : Homogenization.Vec 2 → ℝ) (m : ℕ) (_θprev : ℝ → Homogenization.Vec 2 → ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) => Integration.Normie2SourceContract I hΦ m (I.kappaSeq κ M m) T C √(l2NormSq θ₀)

Exact datum producer of Normie2SourceContract, every input discharged.

theorem AVenhance.Infra.Section5.Contracts.vIncrement_datum_contract (β Ccut : ℝ) : ∃ (Cs : ℝ) (C₁ : ℝ), 1 ≤ Cs ∧ Integration.OnA7Instances β Ccut C₁ fun (I : Ingredients β) (_Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (_hΦ : IsStreamSeq I _Φ) (κ : ℝ) (M : ℕ) (R : ℝ) (θ₀ : Homogenization.Vec 2 → ℝ) (m : ℕ) (_θprev : ℝ → Homogenization.Vec 2 → ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) => Integration.VIncrementContract I m (I.kappaSeq κ M (m - 1)) T Cs R (2 * √(l2NormSq θ₀))

The V increments of the actual iterates at amplitude 2‖θ₀‖, with radius the block's R.

theorem AVenhance.Infra.Section5.Contracts.tinyHMinusSource_datum_closed_contract (β Ccut : ℝ) : ∃ (C : ℝ) (C₁ : ℝ), Integration.OnA7Instances β Ccut C₁ fun (I : Ingredients β) (_Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hΦ : IsStreamSeq I _Φ) (κ : ℝ) (M : ℕ) (_R : ℝ) (θ₀ : Homogenization.Vec 2 → ℝ) (m : ℕ) (_θprev : ℝ → Homogenization.Vec 2 → ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) => Integration.TinyHMinusSourceContract I hΦ m (I.kappaSeq κ M m) (I.kappaSeq κ M (m - 1)) T C √(l2NormSq θ₀)

Exact datum producer of TinyHMinusSourceContract, every input discharged.

theorem AVenhance.Infra.Section5.Contracts.bigbound_of_remaining (β C₀ : ℝ) (hNormie3 : ∃ (C : ℝ) (C₁ : ℝ), Integration.OnA7Instances β C₀ C₁ fun (I : Ingredients β) (_Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hΦ : IsStreamSeq I _Φ) (κ : ℝ) (M : ℕ) (_R : ℝ) (θ₀ : Homogenization.Vec 2 → ℝ) (m : ℕ) (_θprev : ℝ → Homogenization.Vec 2 → ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) => Integration.Normie3CenteredSourceContract I hΦ m (I.kappaSeq κ M m) T C √(l2NormSq θ₀)) : Integration.BigBoundStatement β C₀

Big-bound estimate from a normie3 producer. The literal BigBoundStatement β C₀ (= the body of AVenhance.bigbound), with every other big-bound estimate contract discharged by its datum producer. bigbound_contract supplies the proved normie3CenteredSource_datum_closed_contract for the displayed hypothesis.

theorem AVenhance.Infra.Section5.Contracts.bigbound_closed (β C₀ : ℝ) : Integration.BigBoundStatement β C₀

Big-bound estimate, closed: the literal BigBoundStatement β C₀ with every big-bound estimate contract discharged, Normie3CenteredSourceContract by normie3CenteredSource_datum_closed_contract. This is the producer body for AVenhance.bigbound.