Uniform-amplitude R46 wiring and its closed datum producer

theorem AVenhance.Infra.Section5.Contracts.r46Source_of_TGradient_uniform_amplitude (β C₀ A : ℝ) : ∃ (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 → ℝ) => ∀ (B : ℝ), Integration.TGradientContract β (I.kappaSeq κ M (m - 1)) T A B → Integration.R46SourceContract I hΦ m (I.kappaSeq κ M m) T A B

R46's coefficient is uniform in the amplitude, chosen before the instance.

theorem AVenhance.Infra.Section5.Contracts.r46Source_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.R46SourceContract I hΦ m (I.kappaSeq κ M m) T C √(l2NormSq θ₀)

Exact datum R46 source contract, with its T-gradient input discharged.