Exact Boolean semantics and balancing of the uniform family

Both evaluators always return exactly one bit. The hard family at every positive length is precisely the balanced padding of the preceding length of the source-reduction family, including while the candidate cap is active.

theorem Algebraic.Cutwidth.Extractor.Internal.sourceReductionFamilyEval_length (source : List Bool) : (sourceReductionFamilyEval source).length = 1

theorem Algebraic.Cutwidth.Extractor.Internal.sourceReductionFamilyEval_ofFn (n : ℕ) (x : Fin n → Bool) : sourceReductionFamilyEval (List.ofFn x) = [sourceReductionFamily n x]

theorem Algebraic.Cutwidth.Extractor.Internal.sourceReductionHardEval_ofFn (n : ℕ) (x : Fin n → Bool) : sourceReductionHardEval (List.ofFn x) = [sourceReductionHardFamily n x]

theorem Algebraic.Cutwidth.Extractor.Internal.mem_sourceReductionHardLanguage_ofFn (n : ℕ) (x : Fin n → Bool) : List.ofFn x ∈ sourceReductionHardLanguage ↔ sourceReductionHardFamily n x = true

theorem Algebraic.Cutwidth.Extractor.Internal.sourceReductionHardFamily_succ (n : ℕ) : sourceReductionHardFamily (n + 1) = balancePad (sourceReductionFamily n)

theorem Algebraic.Cutwidth.Extractor.Internal.sourceReductionHardFamily_card_accepting (n : ℕ) : (accepting (sourceReductionHardFamily (n + 1))).card = 2 ^ n