Refine extraction sources on unbroken words
Provedmme_exact_step_source_refinement_on_unbrokenregional-extractiontensor-complexity
An exact extraction step can be transported from source P to source Q when P implies Q on the unbroken words at every selected address. The selected count, repair exponent, number of copies, and output predicate are preserved.
Preamble
import Definitions.Def_mme_recursive_profiled_CW_data open BigOperators MME MME.ProfiledCW MME.RecursiveYZ MME.CompleteSplit open scoped Classical set_option autoImplicit false
Formal statement
theorem mme_exact_step_source_refinement_on_unbroken
{ell N : ℕ} {P Q : Predicate N} (E : ExactStep ell N P)
(hPQ : ∀ j i f, f ∈ unbrokenWords E.stage.total i (E.address j) (E.stage.mu i) →
P i (flatten E.stage.positions E.length f) →
Q i (flatten E.stage.positions E.length f)) :
∃ F : ExactStep ell N Q, F.count = E.count ∧
F.stage.repairExponent = E.stage.repairExponent ∧
F.copies = E.copies ∧ F.output = E.output := by sorrySource
Exact regional extraction and complementary child grades.