Complementary child grades recover parent grades
Provedmme_child_grading_implies_parent_gradingregional-extractiontensor-complexity
For any regional address, a word satisfying its child grading has the prescribed parent grade at each parent position: the two child grades sum to that parent grade.
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_child_grading_implies_parent_grading
{half R ell : ℕ} {parent : Fin R → Fin 3 → ℕ} {n : Fin R → ℕ}
(htotal : ∀ r, parent r 0 + parent r 1 + parent r 2 = 2 * half)
(i : Fin 3) (a : Address half R parent n) (f : Position n → CompleteWord ell)
(hf : Graded htotal i a f) (r : Fin R) (t : Fin (n r)) :
(∑ h : Fin 2, ∑ q, (f ⟨r,t,h⟩ q).val) = parent r i := by sorrySource
Exact regional extraction and complementary child grades.