Documentation

MIPRE.Background.QLD.PauliBranchPrograms

Faithful finite routing of the Pauli decision rules #

Only the fixed twenty-six types are tabulated. The route retains orientation, basis and actual Magic Square indices. Equal-type consistency is selected only for equal types, and every edge selects a substantive rule rather than the off-graph default. Field computations remain uniform programs supplied by the caller; this finite dispatcher never tabulates field elements or answers.

source
@[reducible, inline]
abbrev MIPRE.QLD.PauliBranchProgram.Route :
Type

Rule number, orientation reversal, primary index, secondary index. Rules zero through seven are consistency and the seven rules of pairTest; eight is its unconditional off-graph fallback.

Equations
Instances For
    source
    def MIPRE.QLD.PauliBranchProgram.basisIndex :
    Bas → ℕ
    Equations
    Instances For
      source
      def MIPRE.QLD.PauliBranchProgram.pairRoute :
      Ty → Ty → Route
      Equations
      Instances For
        source
        def MIPRE.QLD.PauliBranchProgram.route (T U : Ty) :
        Route
        Equations
        Instances For
          source
          noncomputable def MIPRE.QLD.PauliBranchProgram.routeProg :
          Cost.PolyTimeFun (Ty × Ty) Route
          Equations
          Instances For
            source
            @[simp]
            theorem MIPRE.QLD.PauliBranchProgram.routeProg_apply (T U : Ty) :
            routeProg.toFun (T, U) = route T U
            source
            theorem MIPRE.QLD.PauliBranchProgram.consistency_iff (T U : Ty) :
            (route T U).1 = 0 ↔ T = U
            source
            theorem MIPRE.QLD.PauliBranchProgram.route_lt_nine (T U : Ty) :
            (route T U).1 < 9
            source
            theorem MIPRE.QLD.PauliBranchProgram.route_con_var (i : Fin LCS.MagicSquare.layout.r) (j : Fin LCS.MagicSquare.layout.s) :
            route (Ty.con i) (Ty.var j) = (6, false, ↑i, ↑j)
            source
            noncomputable def MIPRE.QLD.PauliBranchProgram.selectProg :
            Cost.PolyTimeFun (Route × List Bool) Bool

            The first eight supplied Boolean checks have the order of the route numbers. The finite fallback is true, exactly as in pairTest.

            Equations
            Instances For
              source
              theorem MIPRE.QLD.PauliBranchProgram.selectProg_apply (r : Route) (checks : List Bool) :
              selectProg.toFun (r, checks) = checks.getD r.1 true
              source
              noncomputable def MIPRE.QLD.PauliBranchProgram.orientProg {α : Type u_1} [Cost.SizedEncoding α] :
              Cost.PolyTimeFun (Bool × α × α) (α × α)

              Put the distinguished point, half-pair or constraint on the left before calling the corresponding uniform field/bit check.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                theorem MIPRE.QLD.PauliBranchProgram.orientProg_apply {α : Type u_1} [Cost.SizedEncoding α] (swap : Bool) (a b : α) :
                orientProg.toFun (swap, a, b) = if swap = true then (b, a) else (a, b)
                source
                noncomputable def MIPRE.QLD.PauliBranchProgram.formatGuard :
                Cost.PolyTimeFun (Bool × Bool × Bool) Bool

                Reject either malformed payload before using the selected Boolean rule.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  theorem MIPRE.QLD.PauliBranchProgram.formatGuard_apply (ha hb result : Bool) :
                  formatGuard.toFun (ha, hb, result) = (ha && hb && result)