Regularity and period primitives for the explicit qMNR recursion.

theorem AVenhance.Infra.Section3.QMNRRecursion.matrixEntry_continuous {f : ℝ → Matrix (Fin 2) (Fin 2) ℝ} (hf : Continuous f) (i j : Fin 2) : Continuous fun (t : ℝ) => f t i j

theorem AVenhance.Infra.Section3.qMNR_entry_continuous {β : ℝ} (I : Ingredients β) (κ : ℝ) (m n r : ℕ) (i j : Fin 2) : Continuous fun (t : ℝ) => I.qMNR κ m n r t i j

Every entry in the recursively defined family is continuous.

theorem AVenhance.Infra.Section3.qMNR_timeAvg_zero {β : ℝ} (I : Ingredients β) (κ : ℝ) (m n r : ℕ) : timeAvgMat (I.qMNR κ m n (r + 1)) = 0

Every positive recursion level has zero unit-time average by construction.

theorem AVenhance.Infra.Section3.QMNRRecursion.period_integral_zero_of_unit_average_zero {f : ℝ → ℝ} {P : ℝ} {N : ℕ} (hperiodic : Function.Periodic f P) (hcont : Continuous f) (hunit : ↑N * P = 1) (havg : ∫ (t : ℝ) in 0..1, f t = 0) : ∫ (t : ℝ) in 0..P, f t = 0

theorem AVenhance.Infra.Section3.qMNR_periodic_and_period_mean_zero {β : ℝ} (I : Ingredients β) (κ : ℝ) {m n : ℕ} (hm : 1 ≤ m) (r : ℕ) : Function.Periodic (I.qMNR κ m n r) (4 * tau β I.Λ m) ∧ ∀ (i j : Fin 2), ∫ (t : ℝ) in 0..4 * tau β I.Λ m, I.qMNR κ m n r t i j = 0

Every recursively defined qMNR level is periodic, and has zero mean on one 4τ_m cell. The base case uses the exact integer period count.

theorem AVenhance.Infra.Section3.qMNR_periodic {β : ℝ} (I : Ingredients β) (κ : ℝ) {m n : ℕ} (hm : 1 ≤ m) (r : ℕ) : Function.Periodic (I.qMNR κ m n r) (4 * tau β I.Λ m)

all recursively constructed q_{m,n,r} use the corrected 4τ_m period.

theorem AVenhance.Infra.Section3.qMNR_hasDerivAt {β : ℝ} (I : Ingredients β) (κ : ℝ) (m n r : ℕ) (t : ℝ) (i j : Fin 2) : HasDerivAt (fun (s : ℝ) => I.qMNR κ m n (r + 1) s i j) (-I.qMNR κ m n r t i j) t

The defining primitive step satisfies the derivative recursion.

theorem AVenhance.Infra.Section3.QMNRRecursion.eq_of_same_derivative_and_zero_average {f g : ℝ → ℝ} (hf : Continuous f) (hg : Continuous g) (hderivF : ∀ (t : ℝ), HasDerivAt f (deriv f t) t) (hderivG : ∀ (t : ℝ), HasDerivAt g (deriv g t) t) (hsame : ∀ (t : ℝ), deriv f t = deriv g t) (hzeroF : ∫ (t : ℝ) in 0..1, f t = 0) (hzeroG : ∫ (t : ℝ) in 0..1, g t = 0) : f = g

theorem AVenhance.Infra.Section3.qMNR_unique {β : ℝ} (I : Ingredients β) (κ : ℝ) {m n : ℕ} (_hm : 1 ≤ m) (q' : ℕ → ℝ → Matrix (Fin 2) (Fin 2) ℝ) (hbase : ∀ (t : ℝ), q' 0 t = I.jMN κ m n t - timeAvgMat (I.jMN κ m n)) (_hperiod : ∀ (r : ℕ), Function.Periodic (q' r) (4 * tau β I.Λ m)) (hmean : ∀ (r : ℕ), 1 ≤ r → timeAvgMat (q' r) = 0) (hderiv : ∀ (r : ℕ) (t : ℝ) (i j : Fin 2), HasDerivAt (fun (s : ℝ) => q' (r + 1) s i j) (-q' r t i j) t) (r : ℕ) : q' r = I.qMNR κ m n r

Any family satisfying the stated base value, period, means, and derivative recursion coincides with the explicit qMNR family.