Bridges from the global source-form flow package to the per-scale hypotheses consumed by the Section 2 induction.
theorem
AVenhance.Infra.Construction.section2_flow_bounds_at_scale_from_induction
{β : ℝ}
{I : Ingredients β}
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
{hseq : IsStreamSeq I Φ}
{R M : ℕ → ℝ}
{K : ℝ}
(hscales : Section2Scales I R M)
(happB2 : AppB2InverseFlowData I Φ hseq R M)
(hind : ∀ (m : ℕ), Section2StreamInductionHypothesis R M m)
(hK : 1 ≤ K)
(hlevels : MaterialAuxJetLevels I Φ (2 * Nstar β + 1) K (Nstar β))
(m : ℕ)
(hm : 1 ≤ m)
:
Section2FlowBoundsAtScale I Φ hseq (section2MaterialJacobianConstant β K) m
The material-Jacobian display at one scale follows from the actual all-order velocity material jets and the spatial displays at that scale.
theorem
AVenhance.Infra.Construction.section2_flow_bounds_of_stream_induction
{β : ℝ}
{I : Ingredients β}
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
{hseq : IsStreamSeq I Φ}
{R M : ℕ → ℝ}
(hscales : Section2Scales I R M)
(happB2 : AppB2InverseFlowData I Φ hseq R M)
(hind : ∀ (m : ℕ), Section2StreamInductionHypothesis R M m)
(hincrement : StreamIncrementBounds I Φ)
:
∃ (Cmat : ℝ), 1 ≤ Cmat ∧ FlowBoundsData I Φ hseq Cmat
Assemble FlowBoundsData from the same induction that proves the first
stream-regularity increment display. In particular, each positive-scale material field is
derived from the previous scale's stream induction hypothesis.
theorem
AVenhance.Infra.Construction.section2_joint_induction_with_derived_flow
{β : ℝ}
{I : Ingredients β}
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
{hseq : IsStreamSeq I Φ}
{R M : ℕ → ℝ}
(hscales : Section2Scales I R M)
(happB2 : AppB2InverseFlowData I Φ hseq R M)
:
(∀ (m : ℕ), Section2StreamInductionHypothesis R M m) ∧ StreamIncrementBounds I Φ ∧ ∃ (Cmat : ℝ),
1 ≤ Cmat ∧ FlowBoundsData I Φ hseq Cmat ∧ ∀ (m : ℕ), 1 ≤ m → CMaterialGoalSourceData I Φ hseq (materialFlowCompositionConstant β Cmat) m
The joint induction now proves both e.indyhyp and the global source-form
flow/material package, with no full per-scale hypothesis assumed.