Documentation

Complexity.Computability.PolyTime.LinearAlgebra.ReplacementDesignBuilder

Polynomial-time replacement design builder (Lemma 4.7) #

Executable neutral-singleton scope augmentation (withNeutralScopesList) and deterministic polynomial-time Lemma 4.7 replacement-design construction (buildReplacementDesignData) from §4.6 (Lemma 4.7, pp. 33–34) and §§5.3, 5.5 (pp. 37–38) of OpenAI, The Exponential Time Hypothesis is False. Plain @[fun_prop] Turing.MultiTapeTM.ComputableInPolyTime certificates cover the tape-encoded routines (withNeutralScopesList, scopeIncidencesList, normalizeVarSchedules, normalizeScopeSchedules, incidenceLabelsList, buildReplacementDesignData, ReplacementDesignData projections, and ReplacementDesignData.lookupReplacementRow, with encUnary on (n_free, D_cap, Q, r, A₀, R) and binary/list encodings on scopes, schedules, and ReplacementDesignData), while listScopeFamily, withNeutralScopesIndexEquiv, finToScopeIncidence, scopeIncidenceEquivFin, varAssignOfList, factorAssignOfList, BalancedSchedule, placeFinOfBalanced, constructedReplacementDesign, and ReplacementDesignData.Refines serve as unencoded semantic specification bridges. All executable routines are total: scopes ignore variable indices ≥ n_free; schedule words truncate/pad with 0 to length Q modulo max r 1 with missing rows and empty in-range scopes normalized to List.replicate Q 0; auxiliary tables cap at min D_cap (r ^ (2 * Q)) (copyCount = 0 when r = 0 and Q > 0); and for data produced by the builder, lookupReplacementRow returns [] when (f, v) is absent.

Main definitions #

Main results #

References #

1. Executable neutral-singleton scope augmentation (withNeutralScopesList) #

source
def Cslib.LinearAlgebra.withNeutralScopesList (scopes : List (List ℕ)) (n_free : ℕ) :
List (List ℕ)

Executable neutral-padding scope augmentation appending [0], …, [n_free - 1] to scopes ([OAI26c], §§5.3, 5.5, pp. 37–38).

Instances For
    source
    @[simp]
    theorem Cslib.LinearAlgebra.length_withNeutralScopesList (scopes : List (List ℕ)) (n_free : ℕ) :
    (withNeutralScopesList scopes n_free).length = scopes.length + n_free
    source
    def Cslib.LinearAlgebra.listScopeFamily (n_free : ℕ) (scopes : List (List ℕ)) (f : Fin scopes.length) :
    Finset (Fin n_free)

    Semantic Fin-indexed scope family induced by scopes : List (List ℕ).

    Instances For
      source
      @[simp]
      theorem Cslib.LinearAlgebra.mem_listScopeFamily {n_free : ℕ} {scopes : List (List ℕ)} {f : Fin scopes.length} {v : Fin n_free} :
      v ∈ listScopeFamily n_free scopes f ↔ ↑v ∈ scopes[f]
      source
      theorem Cslib.LinearAlgebra.card_listScopeFamily_le (n_free : ℕ) (scopes : List (List ℕ)) (f : Fin scopes.length) :
      (listScopeFamily n_free scopes f).card ≤ scopes[f].length

      Every semantic scope listScopeFamily n_free scopes f has size at most scopes[f].length.

      source
      def Cslib.LinearAlgebra.withNeutralScopesIndexEquiv (scopes : List (List ℕ)) (n_free : ℕ) :
      Fin scopes.length ⊕ Fin n_free ≃ Fin (withNeutralScopesList scopes n_free).length

      Factor-index equivalence Fin scopes.length ⊕ Fin n_free ≃ Fin augScopes.length.

      Instances For
        source
        @[simp]
        theorem Cslib.LinearAlgebra.val_withNeutralScopesIndexEquiv_inl (scopes : List (List ℕ)) (n_free : ℕ) (f : Fin scopes.length) :
        ↑((withNeutralScopesIndexEquiv scopes n_free) (Sum.inl f)) = ↑f
        source
        @[simp]
        theorem Cslib.LinearAlgebra.val_withNeutralScopesIndexEquiv_inr (scopes : List (List ℕ)) (n_free : ℕ) (v : Fin n_free) :
        ↑((withNeutralScopesIndexEquiv scopes n_free) (Sum.inr v)) = scopes.length + ↑v
        source
        @[simp]
        theorem Cslib.LinearAlgebra.listScopeFamily_withNeutralScopesList (scopes : List (List ℕ)) (n_free : ℕ) (s : Fin scopes.length ⊕ Fin n_free) :
        listScopeFamily n_free (withNeutralScopesList scopes n_free) ((withNeutralScopesIndexEquiv scopes n_free) s) = BitString.withNeutralScope (listScopeFamily n_free scopes) s

        Exact agreement between withNeutralScopesList and Cslib.BitString.withNeutralScope.

        source
        theorem Cslib.LinearAlgebra.varIncidence_listScopeFamily_withNeutralScopesList (scopes : List (List ℕ)) (n_free : ℕ) (v : Fin n_free) :
        BitString.varIncidence Finset.univ (listScopeFamily n_free (withNeutralScopesList scopes n_free)) v = BitString.varIncidence Finset.univ (listScopeFamily n_free scopes) v + 1

        Variable incidence increases by 1 at every free variable under withNeutralScopesList.

        source
        theorem Cslib.LinearAlgebra.totalIncidence_listScopeFamily_withNeutralScopesList (scopes : List (List ℕ)) (n_free : ℕ) :
        BitString.totalIncidence Finset.univ (listScopeFamily n_free (withNeutralScopesList scopes n_free)) = BitString.totalIncidence Finset.univ (listScopeFamily n_free scopes) + n_free

        Total incidence increases by n_free under withNeutralScopesList.

        2. Canonical scope incidences and Lemma 4.5 schedule balance #

        source
        def Cslib.LinearAlgebra.canonicalScopeVars (n_free : ℕ) (s : List ℕ) :
        List ℕ

        Sorted duplicate-free list of variable indices < n_free belonging to s : List ℕ.

        Instances For
          source
          @[simp]
          theorem Cslib.LinearAlgebra.mem_canonicalScopeVars {n_free v : ℕ} {s : List ℕ} :
          v ∈ canonicalScopeVars n_free s ↔ v < n_free ∧ v ∈ s
          source
          theorem Cslib.LinearAlgebra.nodup_canonicalScopeVars (n_free : ℕ) (s : List ℕ) :
          (canonicalScopeVars n_free s).Nodup
          source
          theorem Cslib.LinearAlgebra.canonicalScopeVars_isEmpty_iff (n_free : ℕ) (scopes : List (List ℕ)) (f : Fin scopes.length) :
          (canonicalScopeVars n_free (scopes.getD ↑f [])).isEmpty = true ↔ listScopeFamily n_free scopes f = ∅
          source
          def Cslib.LinearAlgebra.scopeIncidencesList (n_free : ℕ) (scopes : List (List ℕ)) :
          List (ℕ × ℕ)

          Canonical ordered list of factor–variable incidences (f, v).

          Instances For
            source
            @[simp]
            theorem Cslib.LinearAlgebra.mem_scopeIncidencesList {n_free : ℕ} {scopes : List (List ℕ)} {p : ℕ × ℕ} :
            p ∈ scopeIncidencesList n_free scopes ↔ p.1 < scopes.length ∧ p.2 < n_free ∧ p.2 ∈ scopes.getD p.1 []
            source
            theorem Cslib.LinearAlgebra.nodup_scopeIncidencesList (n_free : ℕ) (scopes : List (List ℕ)) :
            (scopeIncidencesList n_free scopes).Nodup
            source
            def Cslib.LinearAlgebra.finToScopeIncidence (n_free : ℕ) (scopes : List (List ℕ)) (i : Fin (scopeIncidencesList n_free scopes).length) :
            BalancedSchedules.ScopeIncidence (listScopeFamily n_free scopes)

            Map an index in Fin (scopeIncidencesList n_free scopes).length to ScopeIncidence.

            Instances For
              source
              theorem Cslib.LinearAlgebra.bijective_finToScopeIncidence (n_free : ℕ) (scopes : List (List ℕ)) :
              Function.Bijective (finToScopeIncidence n_free scopes)
              source
              noncomputable def Cslib.LinearAlgebra.scopeIncidenceEquivFin (n_free : ℕ) (scopes : List (List ℕ)) :
              BalancedSchedules.ScopeIncidence (listScopeFamily n_free scopes) ≃ Fin (scopeIncidencesList n_free scopes).length

              Canonical bijection ScopeIncidence (listScopeFamily n_free scopes) ≃ Fin M.

              Instances For
                source
                @[simp]
                theorem Cslib.LinearAlgebra.finToScopeIncidence_scopeIncidenceEquivFin (n_free : ℕ) (scopes : List (List ℕ)) (e : BalancedSchedules.ScopeIncidence (listScopeFamily n_free scopes)) :
                finToScopeIncidence n_free scopes ((scopeIncidenceEquivFin n_free scopes) e) = e
                source
                @[simp]
                theorem Cslib.LinearAlgebra.scopeIncidenceEquivFin_finToScopeIncidence (n_free : ℕ) (scopes : List (List ℕ)) (i : Fin (scopeIncidencesList n_free scopes).length) :
                (scopeIncidenceEquivFin n_free scopes) (finToScopeIncidence n_free scopes i) = i
                source
                @[simp]
                theorem Cslib.LinearAlgebra.getElem_scopeIncidencesList_equiv (n_free : ℕ) (scopes : List (List ℕ)) (e : BalancedSchedules.ScopeIncidence (listScopeFamily n_free scopes)) :
                (scopeIncidencesList n_free scopes)[↑((scopeIncidenceEquivFin n_free scopes) e)] = (↑(BalancedSchedules.scopeFactorOf (listScopeFamily n_free scopes) e), ↑(BalancedSchedules.scopeVarOf (listScopeFamily n_free scopes) e))
                source
                theorem Cslib.LinearAlgebra.val_scopeIncidenceEquivFin_eq_idxOf (n_free : ℕ) (scopes : List (List ℕ)) (e : BalancedSchedules.ScopeIncidence (listScopeFamily n_free scopes)) :
                ↑((scopeIncidenceEquivFin n_free scopes) e) = List.idxOf (↑(BalancedSchedules.scopeFactorOf (listScopeFamily n_free scopes) e), ↑(BalancedSchedules.scopeVarOf (listScopeFamily n_free scopes) e)) (scopeIncidencesList n_free scopes)
                source
                theorem Cslib.LinearAlgebra.length_scopeIncidencesList (n_free : ℕ) (scopes : List (List ℕ)) :
                (scopeIncidencesList n_free scopes).length = ∑ f : Fin scopes.length, (listScopeFamily n_free scopes f).card
                source
                def Cslib.LinearAlgebra.normalizeScheduleWord (Q r : ℕ) (w : List ℕ) :
                List ℕ

                Normalize a schedule word w : List ℕ to length Q with entries < max r 1.

                Instances For
                  source
                  @[simp]
                  theorem Cslib.LinearAlgebra.length_normalizeScheduleWord (Q r : ℕ) (w : List ℕ) :
                  (normalizeScheduleWord Q r w).length = Q
                  source
                  def Cslib.LinearAlgebra.normalizeVarSchedules (n_free Q r : ℕ) (schedVar : List (List ℕ)) :
                  List (List ℕ)

                  Normalize schedVar to n_free length-Q words over {0, …, max r 1 - 1}.

                  Instances For
                    source
                    @[simp]
                    theorem Cslib.LinearAlgebra.length_normalizeVarSchedules (n_free Q r : ℕ) (schedVar : List (List ℕ)) :
                    (normalizeVarSchedules n_free Q r schedVar).length = n_free
                    source
                    def Cslib.LinearAlgebra.normalizeScopeSchedules (n_free Q r : ℕ) (scopes schedScope : List (List ℕ)) :
                    List (List ℕ)

                    Normalize schedScope to scopes.length length-Q words, mapping empty in-range scopes to List.replicate Q 0 ([OAI26c], §4.1 & Lemma 4.5, pp. 27, 30–31).

                    Instances For
                      source
                      @[simp]
                      theorem Cslib.LinearAlgebra.length_normalizeScopeSchedules (n_free Q r : ℕ) (scopes schedScope : List (List ℕ)) :
                      (normalizeScopeSchedules n_free Q r scopes schedScope).length = scopes.length
                      source
                      def Cslib.LinearAlgebra.varAssignOfList {r : ℕ} (hr : 1 ≤ r) (n_free Q : ℕ) (schedVar : List (List ℕ)) (v : Fin n_free) (t : Fin Q) :
                      Fin r

                      Typed variable group schedule Fin n_free → Fin Q → Fin r extracted from schedVar.

                      Instances For
                        source
                        def Cslib.LinearAlgebra.factorAssignOfList {r : ℕ} (hr : 1 ≤ r) (n_free Q : ℕ) (scopes schedScope : List (List ℕ)) (f : Fin scopes.length) (t : Fin Q) :
                        Fin r

                        Typed factor group schedule Fin scopes.length → Fin Q → Fin r extracted from schedScope.

                        Instances For
                          source
                          @[simp]
                          theorem Cslib.LinearAlgebra.val_varAssignOfList {r : ℕ} (hr : 1 ≤ r) (n_free Q : ℕ) (schedVar : List (List ℕ)) (v : Fin n_free) (t : Fin Q) :
                          ↑(varAssignOfList hr n_free Q schedVar v t) = ((normalizeVarSchedules n_free Q r schedVar).getD ↑v []).getD (↑t) 0
                          source
                          @[simp]
                          theorem Cslib.LinearAlgebra.val_factorAssignOfList {r : ℕ} (hr : 1 ≤ r) (n_free Q : ℕ) (scopes schedScope : List (List ℕ)) (f : Fin scopes.length) (t : Fin Q) :
                          ↑(factorAssignOfList hr n_free Q scopes schedScope f t) = ((normalizeScopeSchedules n_free Q r scopes schedScope).getD ↑f []).getD (↑t) 0
                          source
                          theorem Cslib.LinearAlgebra.factorAssignOfList_of_empty {r : ℕ} (hr : 1 ≤ r) (n_free Q : ℕ) (scopes schedScope : List (List ℕ)) {f : Fin scopes.length} (hf : listScopeFamily n_free scopes f = ∅) (t : Fin Q) :
                          ↑(factorAssignOfList hr n_free Q scopes schedScope f t) = 0
                          source
                          def Cslib.LinearAlgebra.incidenceLabelsList (n_free Q r : ℕ) (scopes schedVar schedScope : List (List ℕ)) :
                          List ℕ

                          Executable list of packed auxiliary incidence labels u_{f,v} < r ^ (2 * Q).

                          Instances For
                            source
                            @[simp]
                            theorem Cslib.LinearAlgebra.length_incidenceLabelsList (n_free Q r : ℕ) (scopes schedVar schedScope : List (List ℕ)) :
                            (incidenceLabelsList n_free Q r scopes schedVar schedScope).length = (scopeIncidencesList n_free scopes).length
                            source
                            theorem Cslib.LinearAlgebra.incidenceLabelsList_eq_ofFn {r : ℕ} (hr : 1 ≤ r) (n_free Q : ℕ) (scopes schedVar schedScope : List (List ℕ)) :
                            incidenceLabelsList n_free Q r scopes schedVar schedScope = List.ofFn fun (i : Fin (scopeIncidencesList n_free scopes).length) => encodeAuxLabel (BalancedSchedules.incidenceLabel (BalancedSchedules.scopeVarOf (listScopeFamily n_free scopes)) (BalancedSchedules.scopeFactorOf (listScopeFamily n_free scopes)) (varAssignOfList hr n_free Q schedVar) (factorAssignOfList hr n_free Q scopes schedScope) (finToScopeIncidence n_free scopes i))

                            incidenceLabelsList equals List.ofFn of encodeAuxLabel ∘ u ∘ finToScopeIncidence.

                            source
                            def Cslib.LinearAlgebra.BalancedSchedule {r : ℕ} (hr : 1 ≤ r) (n_free Q : ℕ) (scopes schedVar schedScope : List (List ℕ)) :
                            Prop

                            Lemma 4.5 balance predicate on executable schedule lists (schedVar, schedScope) ([OAI26c], Lemma 4.5 & Lemma 4.7, pp. 30–31, 33–34).

                            Instances For
                              source
                              theorem Cslib.LinearAlgebra.balancedSchedule_iff_exec {r : ℕ} (hr : 1 ≤ r) (n_free Q : ℕ) (scopes schedVar schedScope : List (List ℕ)) :
                              BalancedSchedule hr n_free Q scopes schedVar schedScope ↔ (∀ idx < r ^ (2 * Q), List.count idx (incidenceLabelsList n_free Q r scopes schedVar schedScope) * r ^ (2 * Q) ≤ 2 * (scopeIncidencesList n_free scopes).length) ∧ ∀ t < Q, ∀ g < r, (CopyPlacement.varGroupList (normalizeVarSchedules n_free Q r schedVar) t g).length * r ≤ 2 * n_free

                              Pure executable list characterization of BalancedSchedule, enabling decide verification.

                              source
                              theorem Cslib.LinearAlgebra.exists_balancedSchedule_of_scopes {n_free Q r b w : ℕ} (scopes : List (List ℕ)) (hn : 1 ≤ n_free) (hr : 1 ≤ r) (hQ : 1 ≤ Q) (hbw : 0 < b + w) (hb : ∀ (v : Fin n_free), {f : Fin scopes.length | v ∈ listScopeFamily n_free scopes f}.card ≤ b) (hw : ∀ (f : Fin scopes.length), (listScopeFamily n_free scopes f).card ≤ w) (hincidenceSize : 2 * (b + w) * (r ^ (2 * Q)) ^ 2 ≤ ∑ f : Fin scopes.length, (listScopeFamily n_free scopes f).card) (hgroupSize : 2 * Q * r ^ 2 ≤ n_free) :
                              ∃ (schedVar : List (List ℕ)) (schedScope : List (List ℕ)), schedVar.length = n_free ∧ schedScope.length = scopes.length ∧ BalancedSchedule hr n_free Q scopes schedVar schedScope

                              Lemma 4.5 schedule existence on executable scope lists: under Lemma 4.7's size hypotheses, there exist executable schedule lists (schedVar, schedScope) satisfying BalancedSchedule.

                              3. Bundled Lemma 4.7 design data and executable constructor #

                              source
                              structure Cslib.LinearAlgebra.ReplacementDesignData :
                              Type

                              Bundled executable Lemma 4.7 replacement-design arrays ([OAI26c], Lemma 4.7).

                              • varGroups : List (List (List ℕ))

                                Step-and-group variable partitions V_0, …, V_{r - 1} for t < Q.

                              • factorGroups : List (List ℕ)

                                Normalized factor group schedules σ_f ∈ {0, …, r - 1}^Q for f < scopes.length.

                              • incidences : List (ℕ × ℕ)

                                Canonical ordered list of factor–variable incidences (f, v).

                              • copyCount : ℕ

                                Copy count h = 2 * incidences.length / r ^ (2 * Q).

                              • placements : List (ℕ × ℕ)

                                Injective incidence copy placements (c_e, u_e) for e < incidences.length.

                              • measurementMatrix : List (List ℤ)

                                Pulled-back (copyCount * c_B) × n_free integer measurement matrix Ĉ = C̃ ι.

                              • groupMeasurementMatrices : List (List (List (List ℤ)))

                                Step-and-group restricted integer measurement matrices C_{t,g} = Ĉ|_{S_{t,g}}.

                              • denom : ℤ

                                Cleared common denominator d_den = (R - 1)! * Q! as an integer.

                              • replacementRows : List (List (List ℤ))

                                Per-incidence n_free × R cleared replacement-row coefficient tables d_den · P⃗_e(T).

                              Instances For
                                source
                                def Cslib.LinearAlgebra.instDecidableEqReplacementDesignData.decEq (x✝ x✝¹ : ReplacementDesignData) :
                                Decidable (x✝ = x✝¹)
                                Instances For
                                  source
                                  @[instance_reducible]
                                  instance Cslib.LinearAlgebra.instDecidableEqReplacementDesignData :
                                  DecidableEq ReplacementDesignData
                                  source
                                  @[instance_reducible]
                                  instance Cslib.LinearAlgebra.instReprReplacementDesignData :
                                  Repr ReplacementDesignData
                                  source
                                  def Cslib.LinearAlgebra.instReprReplacementDesignData.repr :
                                  ReplacementDesignData → ℕ → Std.Format
                                  Instances For
                                    source
                                    @[reducible, inline]
                                    abbrev Cslib.LinearAlgebra.ReplacementDesignTuple :
                                    Type

                                    Underlying nested product representation of ReplacementDesignData for tape encoding.

                                    Instances For
                                      source
                                      def Cslib.LinearAlgebra.ReplacementDesignData.equivTuple :
                                      ReplacementDesignData ≃ ReplacementDesignTuple

                                      Canonical equivalence between ReplacementDesignData and ReplacementDesignTuple.

                                      Instances For
                                        source
                                        def Cslib.LinearAlgebra.encReplacementDesignTuple :
                                        ReplacementDesignTuple ↪ List Bool

                                        Standard multi-tape Turing machine encoding of ReplacementDesignTuple.

                                        Instances For
                                          source
                                          def Cslib.LinearAlgebra.encReplacementDesignData :
                                          ReplacementDesignData ↪ List Bool

                                          Standard multi-tape Turing machine encoding of ReplacementDesignData.

                                          Instances For
                                            source
                                            def Cslib.LinearAlgebra.buildReplacementDesignData (n_free D_cap Q r A₀ R : ℕ) (scopes schedVar schedScope : List (List ℕ)) :
                                            ReplacementDesignData

                                            Executable Lemma 4.7 replacement-design constructor assembling ExchangeReplacement and CopyPlacement over (schedVar, schedScope) ([OAI26c], §4.6, Lemma 4.7, pp. 33–34).

                                            Instances For
                                              source
                                              def Cslib.LinearAlgebra.ReplacementDesignData.lookupReplacementRow (data : ReplacementDesignData) (f v : ℕ) :
                                              List (List ℤ)

                                              Look up the n_free × R cleared replacement-row coefficient table for (f, v).

                                              Instances For

                                                4. Plain polynomial-time certificates (ComputableInPolyTime) #

                                                source
                                                theorem Cslib.LinearAlgebra.computableInPolyTime_withNeutralScopesListWithInput {Input : Type} {encIn : Input ↪ List Bool} {scopes : Input → List (List ℕ)} {n_free : Input → ℕ} (hscopes : Turing.MultiTapeTM.ComputableInPolyTime scopes encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat))) (hn : Turing.MultiTapeTM.ComputableInPolyTime n_free encIn Turing.MultiTapeTM.encUnary) :
                                                Turing.MultiTapeTM.ComputableInPolyTime (fun (x : Input) => withNeutralScopesList (scopes x) (n_free x)) encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat))

                                                Compositional plain polynomial-time certificate for withNeutralScopesList.

                                                source
                                                theorem Cslib.LinearAlgebra.computableInPolyTime_withNeutralScopesList :
                                                Turing.MultiTapeTM.ComputableInPolyTime (fun (p : List (List ℕ) × ℕ) => withNeutralScopesList p.1 p.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) Turing.MultiTapeTM.encUnary) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat))

                                                withNeutralScopesList is computable in polynomial time with n_free in encUnary.

                                                source
                                                theorem Cslib.LinearAlgebra.computableInPolyTime_scopeIncidencesList {Input : Type} {encIn : Input ↪ List Bool} {n_free : Input → ℕ} {scopes : Input → List (List ℕ)} (hn : Turing.MultiTapeTM.ComputableInPolyTime n_free encIn Turing.MultiTapeTM.encUnary) (hscopes : Turing.MultiTapeTM.ComputableInPolyTime scopes encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat))) :
                                                Turing.MultiTapeTM.ComputableInPolyTime (fun (x : Input) => scopeIncidencesList (n_free x) (scopes x)) encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat))
                                                source
                                                theorem Cslib.LinearAlgebra.computableInPolyTime_normalizeVarSchedules {Input : Type} {encIn : Input ↪ List Bool} {n_free Q r : Input → ℕ} {schedVar : Input → List (List ℕ)} (hn : Turing.MultiTapeTM.ComputableInPolyTime n_free encIn Turing.MultiTapeTM.encUnary) (hQ : Turing.MultiTapeTM.ComputableInPolyTime Q encIn Turing.MultiTapeTM.encUnary) (hr : Turing.MultiTapeTM.ComputableInPolyTime r encIn Turing.MultiTapeTM.encNat) (hsched : Turing.MultiTapeTM.ComputableInPolyTime schedVar encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat))) :
                                                Turing.MultiTapeTM.ComputableInPolyTime (fun (x : Input) => normalizeVarSchedules (n_free x) (Q x) (r x) (schedVar x)) encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat))
                                                source
                                                theorem Cslib.LinearAlgebra.computableInPolyTime_normalizeScopeSchedules {Input : Type} {encIn : Input ↪ List Bool} {n_free Q r : Input → ℕ} {scopes schedScope : Input → List (List ℕ)} (hn : Turing.MultiTapeTM.ComputableInPolyTime n_free encIn Turing.MultiTapeTM.encUnary) (hQ : Turing.MultiTapeTM.ComputableInPolyTime Q encIn Turing.MultiTapeTM.encUnary) (hr : Turing.MultiTapeTM.ComputableInPolyTime r encIn Turing.MultiTapeTM.encNat) (hscopes : Turing.MultiTapeTM.ComputableInPolyTime scopes encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat))) (hsched : Turing.MultiTapeTM.ComputableInPolyTime schedScope encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat))) :
                                                Turing.MultiTapeTM.ComputableInPolyTime (fun (x : Input) => normalizeScopeSchedules (n_free x) (Q x) (r x) (scopes x) (schedScope x)) encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat))
                                                source
                                                theorem Cslib.LinearAlgebra.computableInPolyTime_incidenceLabelsList {Input : Type} {encIn : Input ↪ List Bool} {n_free Q r : Input → ℕ} {scopes schedVar schedScope : Input → List (List ℕ)} (hn : Turing.MultiTapeTM.ComputableInPolyTime n_free encIn Turing.MultiTapeTM.encUnary) (hQ : Turing.MultiTapeTM.ComputableInPolyTime Q encIn Turing.MultiTapeTM.encUnary) (hr : Turing.MultiTapeTM.ComputableInPolyTime r encIn Turing.MultiTapeTM.encNat) (hscopes : Turing.MultiTapeTM.ComputableInPolyTime scopes encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat))) (hschedVar : Turing.MultiTapeTM.ComputableInPolyTime schedVar encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat))) (hschedScope : Turing.MultiTapeTM.ComputableInPolyTime schedScope encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat))) :
                                                Turing.MultiTapeTM.ComputableInPolyTime (fun (x : Input) => incidenceLabelsList (n_free x) (Q x) (r x) (scopes x) (schedVar x) (schedScope x)) encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)
                                                source
                                                theorem Cslib.LinearAlgebra.computableInPolyTime_varGroups {Input : Type} {encIn : Input ↪ List Bool} {d : Input → ReplacementDesignData} (hd : Turing.MultiTapeTM.ComputableInPolyTime d encIn encReplacementDesignData) :
                                                Turing.MultiTapeTM.ComputableInPolyTime (fun (x : Input) => (d x).varGroups) encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)))
                                                source
                                                theorem Cslib.LinearAlgebra.computableInPolyTime_factorGroups {Input : Type} {encIn : Input ↪ List Bool} {d : Input → ReplacementDesignData} (hd : Turing.MultiTapeTM.ComputableInPolyTime d encIn encReplacementDesignData) :
                                                Turing.MultiTapeTM.ComputableInPolyTime (fun (x : Input) => (d x).factorGroups) encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat))
                                                source
                                                theorem Cslib.LinearAlgebra.computableInPolyTime_incidences {Input : Type} {encIn : Input ↪ List Bool} {d : Input → ReplacementDesignData} (hd : Turing.MultiTapeTM.ComputableInPolyTime d encIn encReplacementDesignData) :
                                                Turing.MultiTapeTM.ComputableInPolyTime (fun (x : Input) => (d x).incidences) encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat))
                                                source
                                                theorem Cslib.LinearAlgebra.computableInPolyTime_copyCount {Input : Type} {encIn : Input ↪ List Bool} {d : Input → ReplacementDesignData} (hd : Turing.MultiTapeTM.ComputableInPolyTime d encIn encReplacementDesignData) :
                                                Turing.MultiTapeTM.ComputableInPolyTime (fun (x : Input) => (d x).copyCount) encIn Turing.MultiTapeTM.encNat
                                                source
                                                theorem Cslib.LinearAlgebra.computableInPolyTime_placements {Input : Type} {encIn : Input ↪ List Bool} {d : Input → ReplacementDesignData} (hd : Turing.MultiTapeTM.ComputableInPolyTime d encIn encReplacementDesignData) :
                                                Turing.MultiTapeTM.ComputableInPolyTime (fun (x : Input) => (d x).placements) encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat))
                                                source
                                                theorem Cslib.LinearAlgebra.computableInPolyTime_measurementMatrix {Input : Type} {encIn : Input ↪ List Bool} {d : Input → ReplacementDesignData} (hd : Turing.MultiTapeTM.ComputableInPolyTime d encIn encReplacementDesignData) :
                                                Turing.MultiTapeTM.ComputableInPolyTime (fun (x : Input) => (d x).measurementMatrix) encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))
                                                source
                                                theorem Cslib.LinearAlgebra.computableInPolyTime_groupMeasurementMatrices {Input : Type} {encIn : Input ↪ List Bool} {d : Input → ReplacementDesignData} (hd : Turing.MultiTapeTM.ComputableInPolyTime d encIn encReplacementDesignData) :
                                                Turing.MultiTapeTM.ComputableInPolyTime (fun (x : Input) => (d x).groupMeasurementMatrices) encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))))
                                                source
                                                theorem Cslib.LinearAlgebra.computableInPolyTime_denom {Input : Type} {encIn : Input ↪ List Bool} {d : Input → ReplacementDesignData} (hd : Turing.MultiTapeTM.ComputableInPolyTime d encIn encReplacementDesignData) :
                                                Turing.MultiTapeTM.ComputableInPolyTime (fun (x : Input) => (d x).denom) encIn Turing.MultiTapeTM.encIntBin
                                                source
                                                theorem Cslib.LinearAlgebra.computableInPolyTime_replacementRows {Input : Type} {encIn : Input ↪ List Bool} {d : Input → ReplacementDesignData} (hd : Turing.MultiTapeTM.ComputableInPolyTime d encIn encReplacementDesignData) :
                                                Turing.MultiTapeTM.ComputableInPolyTime (fun (x : Input) => (d x).replacementRows) encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)))
                                                source
                                                theorem Cslib.LinearAlgebra.computableInPolyTime_buildReplacementDesignData {Input : Type} {encIn : Input ↪ List Bool} {n_free D_cap Q r A₀ R : Input → ℕ} {scopes schedVar schedScope : Input → List (List ℕ)} (hn : Turing.MultiTapeTM.ComputableInPolyTime n_free encIn Turing.MultiTapeTM.encUnary) (hD : Turing.MultiTapeTM.ComputableInPolyTime D_cap encIn Turing.MultiTapeTM.encUnary) (hQ : Turing.MultiTapeTM.ComputableInPolyTime Q encIn Turing.MultiTapeTM.encUnary) (hr : Turing.MultiTapeTM.ComputableInPolyTime r encIn Turing.MultiTapeTM.encUnary) (hA₀ : Turing.MultiTapeTM.ComputableInPolyTime A₀ encIn Turing.MultiTapeTM.encUnary) (hR : Turing.MultiTapeTM.ComputableInPolyTime R encIn Turing.MultiTapeTM.encUnary) (hscopes : Turing.MultiTapeTM.ComputableInPolyTime scopes encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat))) (hschedVar : Turing.MultiTapeTM.ComputableInPolyTime schedVar encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat))) (hschedScope : Turing.MultiTapeTM.ComputableInPolyTime schedScope encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat))) :
                                                Turing.MultiTapeTM.ComputableInPolyTime (fun (x : Input) => buildReplacementDesignData (n_free x) (D_cap x) (Q x) (r x) (A₀ x) (R x) (scopes x) (schedVar x) (schedScope x)) encIn encReplacementDesignData

                                                Lemma 4.7 polynomial-time certificate (buildReplacementDesignData): buildReplacementDesignData is computable in polynomial time from unary parameters (n_free, D_cap, Q, r, A₀, R) and list-encoded (scopes, schedVar, schedScope).

                                                source
                                                theorem Cslib.LinearAlgebra.computableInPolyTime_lookupReplacementRow {Input : Type} {encIn : Input ↪ List Bool} {data : Input → ReplacementDesignData} {f v : Input → ℕ} (hdata : Turing.MultiTapeTM.ComputableInPolyTime data encIn encReplacementDesignData) (hf : Turing.MultiTapeTM.ComputableInPolyTime f encIn Turing.MultiTapeTM.encNat) (hv : Turing.MultiTapeTM.ComputableInPolyTime v encIn Turing.MultiTapeTM.encNat) :
                                                Turing.MultiTapeTM.ComputableInPolyTime (fun (x : Input) => (data x).lookupReplacementRow (f x) (v x)) encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))

                                                Compositional plain polynomial-time certificate for lookupReplacementRow.

                                                5. Semantic bridge from buildReplacementDesignData to ReplacementDesign #

                                                source
                                                theorem Cslib.LinearAlgebra.fiberBound_of_balancedSchedule {r : ℕ} (hr : 1 ≤ r) (n_free Q : ℕ) (scopes schedVar schedScope : List (List ℕ)) (hbal : BalancedSchedule hr n_free Q scopes schedVar schedScope) :
                                                let scope := listScopeFamily n_free scopes; have u := BalancedSchedules.incidenceLabel (BalancedSchedules.scopeVarOf scope) (BalancedSchedules.scopeFactorOf scope) (varAssignOfList hr n_free Q schedVar) (factorAssignOfList hr n_free Q scopes schedScope); let M := (scopeIncidencesList n_free scopes).length; ∀ (y : AuxLabel Q r), {i : Fin M | u (finToScopeIncidence n_free scopes i) = y}.card ≤ 2 * M / r ^ (2 * Q)
                                                source
                                                noncomputable def Cslib.LinearAlgebra.placeFinOfBalanced {r : ℕ} (hr : 1 ≤ r) (n_free Q : ℕ) (scopes schedVar schedScope : List (List ℕ)) (hbal : BalancedSchedule hr n_free Q scopes schedVar schedScope) :
                                                have M := (scopeIncidencesList n_free scopes).length; Fin M → Fin (2 * M / r ^ (2 * Q)) × AuxLabel Q r

                                                Concrete Fin M-indexed placement Fin M → Fin h × AuxLabel Q r from BalancedSchedule.

                                                Instances For
                                                  source
                                                  noncomputable def Cslib.LinearAlgebra.constructedReplacementDesign {n_free Q r A₀ R b : ℕ} {τ : ℚ} (scopes schedVar schedScope : List (List ℕ)) (hr : 1 ≤ r) (hQ : 1 ≤ Q) (hb_pos : 1 ≤ b) (hτ : 0 ≤ τ) (hI : ∀ a < R - 1, A₀ + a ≤ Q) (hM_le : ∑ f : Fin scopes.length, (listScopeFamily n_free scopes f).card ≤ b * n_free) (htail : binomTailProb Q r A₀ R ≤ τ / (↑r * ↑b)) (hbal : BalancedSchedule hr n_free Q scopes schedVar schedScope) :
                                                  ReplacementDesign (listScopeFamily n_free scopes) Q r A₀ R τ

                                                  Concrete ReplacementDesign induced by BalancedSchedule (Lemma 4.7, pp. 33–34): constructs ReplacementDesign (listScopeFamily n_free scopes) Q r A₀ R τ from balanced schedules (schedVar, schedScope) and Lemma 4.7's numerical and binomial-tail hypotheses.

                                                  Instances For
                                                    source
                                                    def Cslib.LinearAlgebra.ReplacementDesignData.Refines {n_free Q r A₀ R : ℕ} {τ : ℚ} (scopes : List (List ℕ)) (data : ReplacementDesignData) (D : ReplacementDesign (listScopeFamily n_free scopes) Q r A₀ R τ) :
                                                    Prop

                                                    Componentwise refinement predicate asserting that data : ReplacementDesignData represents D : ReplacementDesign (listScopeFamily n_free scopes) Q r A₀ R τ across all Definition 3.1 components, including global ℚ-kernel equivalence and restricted-kernel evaluation annihilation from C_{t,g}.

                                                    Instances For
                                                      source
                                                      theorem Cslib.LinearAlgebra.buildReplacementDesignData_spec {n_free D_cap Q r A₀ R b : ℕ} {τ : ℚ} (scopes schedVar schedScope : List (List ℕ)) (hD_cap : r ^ (2 * Q) ≤ D_cap) (hr : 1 ≤ r) (hR : 1 ≤ R) (hQ : 1 ≤ Q) (hb_pos : 1 ≤ b) (hτ : 0 ≤ τ) (hI : ∀ a < R - 1, A₀ + a ≤ Q) (htail : binomTailProb Q r A₀ R ≤ τ / (↑r * ↑b)) (hM_le : ∑ f : Fin scopes.length, (listScopeFamily n_free scopes f).card ≤ b * n_free) (hbal : BalancedSchedule hr n_free Q scopes schedVar schedScope) :
                                                      ReplacementDesignData.Refines scopes (buildReplacementDesignData n_free D_cap Q r A₀ R scopes schedVar schedScope) (constructedReplacementDesign scopes schedVar schedScope hr hQ hb_pos hτ hI hM_le htail hbal)

                                                      Main Lemma 4.7 semantic specification (buildReplacementDesignData_spec): under Lemma 4.7's cap, interval, binomial-tail, and BalancedSchedule hypotheses, buildReplacementDesignData refines constructedReplacementDesign.

                                                      source
                                                      theorem Cslib.LinearAlgebra.exists_replacementDesign_of_buildReplacementDesignData {n_free D_cap Q r A₀ R b : ℕ} {τ : ℚ} (scopes schedVar schedScope : List (List ℕ)) (hD_cap : r ^ (2 * Q) ≤ D_cap) (hr : 1 ≤ r) (hR : 1 ≤ R) (hQ : 1 ≤ Q) (hb_pos : 1 ≤ b) (hτ : 0 ≤ τ) (hI : ∀ a < R - 1, A₀ + a ≤ Q) (htail : binomTailProb Q r A₀ R ≤ τ / (↑r * ↑b)) (hM_le : ∑ f : Fin scopes.length, (listScopeFamily n_free scopes f).card ≤ b * n_free) (hbal : BalancedSchedule hr n_free Q scopes schedVar schedScope) :
                                                      ∃ (D : ReplacementDesign (listScopeFamily n_free scopes) Q r A₀ R τ), ReplacementDesignData.Refines scopes (buildReplacementDesignData n_free D_cap Q r A₀ R scopes schedVar schedScope) D

                                                      Bundled existential packaging of buildReplacementDesignData_spec.

                                                      source
                                                      theorem Cslib.LinearAlgebra.exists_replacementDesign_withNeutralScopesList {n_free D_cap Q r A₀ R b₀ : ℕ} {τ : ℚ} (scopes schedVar schedScope : List (List ℕ)) (hD_cap : r ^ (2 * Q) ≤ D_cap) (hr : 1 ≤ r) (hR : 1 ≤ R) (hQ : 1 ≤ Q) (hτ : 0 ≤ τ) (hI : ∀ a < R - 1, A₀ + a ≤ Q) (hb₀ : ∀ (v : Fin n_free), BitString.varIncidence Finset.univ (listScopeFamily n_free scopes) v ≤ b₀) (htail : binomTailProb Q r A₀ R ≤ τ / (↑r * ↑(b₀ + 1))) (hbal : BalancedSchedule hr n_free Q (withNeutralScopesList scopes n_free) schedVar schedScope) :
                                                      have augScopes := withNeutralScopesList scopes n_free; ∃ (D : ReplacementDesign (listScopeFamily n_free augScopes) Q r A₀ R τ), ReplacementDesignData.Refines augScopes (buildReplacementDesignData n_free D_cap Q r A₀ R augScopes schedVar schedScope) D

                                                      Neutral-padded Lemma 4.7 specialization (exists_replacementDesign_withNeutralScopesList): when each free variable belongs to at most b₀ scopes of scopes and (schedVar, schedScope) satisfies BalancedSchedule on withNeutralScopesList scopes n_free, buildReplacementDesignData refines a concrete ReplacementDesign on the augmented scope family with occurrence bound b = b₀ + 1.