Explicit repair and rounding loss for exact extraction copies

Proved

mme_exact_step_copies_gt_normalized_count_sub_one

by Robertboy18 · Sep 22, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

regional-extractiontensor-complexity

If B is a real lower bound for the selected count of an exact extraction step, its integer number of repaired copies is strictly greater than B divided by the power-of-eight repair budget minus one.

Preamble

import Theorems.Thm_mme_recursive_profiled_CW_exact_step
import Definitions.Def_mme_recursive_profiled_CW_data
import Mathlib.Algebra.Order.Field.Basic
import Mathlib.Tactic.NormNum
import Mathlib.Tactic.Linarith
open MME MME.ProfiledCW
set_option autoImplicit false
universe u

Formal statement

theorem mme_exact_step_copies_gt_normalized_count_sub_one
    {ell N : ℕ} {P : Predicate N} (E : ExactStep ell N P) {B : ℝ}
    (hB : B ≤ E.count) :
    B / (8 : ℝ) ^ E.stage.repairExponent - 1 < E.copies := by sorry

Source

Released regional integer profiles, quantitative exact extraction, and explicit repair losses.

View graph