Stage 11R: normalization to the frozen condition number

This file contains only the scalar bridge from the factor-four endpoint of the executable controller amortization to conditionBar = max 1 condition. The constants are explicit and independent of the problem instance.

theorem O3.condition_le_conditionBar {d : ℕ} {p : ℝ} (P : AdmissibleInstance d p) : P.condition ≤ P.conditionBar

theorem O3.one_le_conditionBar {d : ℕ} {p : ℝ} (P : AdmissibleInstance d p) : 1 ≤ P.conditionBar

theorem O3.conditionBar_nonneg {d : ℕ} {p : ℝ} (P : AdmissibleInstance d p) : 0 ≤ P.conditionBar

theorem O3.condition_nonneg {d : ℕ} {p : ℝ} (P : AdmissibleInstance d p) : 0 ≤ P.condition

theorem O3.condition_rpow_le_conditionBar_rpow {d : ℕ} {p : ℝ} (P : AdmissibleInstance d p) {a : ℝ} (ha : 0 ≤ a) : P.condition ^ a ≤ P.conditionBar ^ a

theorem O3.four_mul_rpow_le_conditionBar_rpow {d : ℕ} {p : ℝ} (P : AdmissibleInstance d p) {a : ℝ} (ha : 0 ≤ a) : (4 * P.condition) ^ a ≤ 4 ^ a * P.conditionBar ^ a

theorem O3.sqrt_four_condition_le {d : ℕ} {p : ℝ} (P : AdmissibleInstance d p) : √(4 * P.condition) ≤ 2 * √P.conditionBar

theorem O3.log_exp_one_add_conditionBar_ge_one {d : ℕ} {p : ℝ} (P : AdmissibleInstance d p) : 1 ≤ Real.log (Real.exp 1 + P.conditionBar)

theorem O3.belowWeight_four_condition_le {d : ℕ} {p : ℝ} (P : AdmissibleInstance d p) : belowWrapperWeight (4 * P.condition) ≤ 4 * belowWrapperWeight P.conditionBar

noncomputable def O3.anchorLogConstant : ℝ

Universal coefficient for converting the exact binary-log ceiling of the anchor to the natural-log overhead used in the frozen theorem.

Equations

• O3.anchorLogConstant = 2 + 1 / Real.log 2

theorem O3.anchorLogConstant_pos : 0 < anchorLogConstant

theorem O3.anchor_ceiling_le_log_overhead {L M0 : ℝ} (hM0 : 0 < M0) (hM0L : M0 ≤ L) : ↑(1 + ⌈Real.logb 2 (L / M0)⌉₊) ≤ anchorLogConstant * Real.log (Real.exp 1 + L / M0)

theorem O3.admissible_M0_le_L {d : ℕ} {p : ℝ} (P : AdmissibleInstance d p) : P.M0 ≤ P.L

theorem O3.admissible_log_overhead_ge_one {d : ℕ} {p : ℝ} (P : AdmissibleInstance d p) : 1 ≤ Real.log (Real.exp 1 + P.L / P.M0)

noncomputable def O3.anchorPrefixConstant : ℝ

The positive constant accounting for the initial query and logarithmic anchor overhead.

Equations

• O3.anchorPrefixConstant = 1 + O3.anchorLogConstant

theorem O3.anchorPrefixConstant_pos : 0 < anchorPrefixConstant

theorem O3.anchor_prefix_le_log_overhead {d : ℕ} {p : ℝ} (P : AdmissibleInstance d p) {observations : OracleTrace d} (hcount : List.length observations ≤ 1 + ⌈Real.logb 2 (P.L / P.M0)⌉₊) : ↑(1 + List.length observations) ≤ anchorPrefixConstant * Real.log (Real.exp 1 + P.L / P.M0)

The controller prefix consists of the initial query plus all anchor observations. This is the exact bridge from the anchor's ceiling count to the additive term in the frozen wrapper bounds.

theorem O3.euclidean_envelope_normalized {d : ℕ} {p : ℝ} (P : AdmissibleInstance d p) {pre total A : ℝ} (hA : 0 ≤ A) (henvelope : total ≤ pre + A * euclideanWrapperWeight (4 * P.condition)) (hprefix : pre ≤ anchorPrefixConstant * Real.log (Real.exp 1 + P.L / P.M0)) : total ≤ (anchorPrefixConstant + 2 * A) * √P.conditionBar + (anchorPrefixConstant + 2 * A) * Real.log (Real.exp 1 + P.L / P.M0)

theorem O3.below_envelope_normalized {d : ℕ} {p : ℝ} (P : AdmissibleInstance d p) {pre total A : ℝ} (hA : 0 ≤ A) (henvelope : total ≤ pre + A * belowWrapperWeight (4 * P.condition)) (hprefix : pre ≤ anchorPrefixConstant * Real.log (Real.exp 1 + P.L / P.M0)) : total ≤ (anchorPrefixConstant + 4 * A) * P.conditionBar ^ (1 / 2) * Real.log (Real.exp 1 + P.conditionBar) + (anchorPrefixConstant + 4 * A) * Real.log (Real.exp 1 + P.L / P.M0)

theorem O3.above_envelope_normalized {d : ℕ} {p : ℝ} (P : AdmissibleInstance d p) {a pre total A : ℝ} (ha : 0 ≤ a) (hA : 0 ≤ A) (henvelope : total ≤ pre + A * aboveWrapperWeight a (4 * P.condition)) (hprefix : pre ≤ anchorPrefixConstant * Real.log (Real.exp 1 + P.L / P.M0)) : total ≤ (anchorPrefixConstant + 4 ^ a * A) * P.conditionBar ^ a + (anchorPrefixConstant + 4 ^ a * A) * Real.log (Real.exp 1 + P.L / P.M0)