Documentation

LeanPool.Sundogcert.Instance

Sundogcert/Instance.lean — the concrete executable ZMod 2 instance. A [n=4, k=2, m=2, τ=1] GF(2) syndrome certificate. Two verifiers on ONE scheme: vSupp (lb = supportLb) — degenerate support bound (rejects only at τ=0) vCol (lb = colWeightLb) — non-degenerate column-weight bound (rejects at τ>0) hHG proved AXIOM-CLEAN by decide (kernel; 4 secrets, tiny matrices). HEADLINE: y=1100 & y=1110 DIVERGE (vSupp quarantine, vCol reject) — the non-degenerate bound earning its keep at τ=1. HONESTY NOTE: colBound H = 1 here, so colWeightLb is TIGHT on this code — a FAVORABLE case. In general (non-uniform H) the bound is loose: it divides by the GLOBAL worst column weight (see Certificate.lean). This instance demonstrates the bound's SOUNDNESS and its τ>0 reach, NOT general tightness.

source
def Sundog.Certificate.Instance.G :
Matrix (Fin 2) (Fin 4) (ZMod 2)

The concrete code is C = ker H = {y : y0 = y1 = 0}. G's rows are codewords (coords 2,3), so H *ᵥ (s ᵥ* G) = 0 for every secret.

Equations
Instances For
    source
    def Sundog.Certificate.Instance.H :
    Matrix (Fin 2) (Fin 4) (ZMod 2)

    Parity-check matrix of the concrete code: H *ᵥ y = (y 0, y 1).

    Equations
    Instances For
      source
      theorem Sundog.Certificate.Instance.hHG_decide (s : Fin 2 → ZMod 2) :
      H.mulVec (Matrix.vecMul s G) = 0

      The dual-pair law, AXIOM-CLEAN by decide (4 secrets over ZMod 2, 2×4 / 2×2 matrices).

      source
      def Sundog.Certificate.Instance.S :
      Scheme (ZMod 2)

      The concrete scheme.

      Equations
      Instances For

        The shared witness search and the two verifiers. #

        source
        def Sundog.Certificate.Instance.witnessOpt (y : Fin S.n → ZMod 2) :
        Option (Fin S.n → ZMod 2)

        Forward witness: if y is already light (wt y ≤ τ) it is its own same-syndrome witness.

        Equations
        Instances For
          source
          theorem Sundog.Certificate.Instance.witness_sound (y e' : Fin S.n → ZMod 2) :
          witnessOpt y = some e' → S.H.mulVec e' = S.H.mulVec y ∧ wt e' ≤ S.τ
          source
          def Sundog.Certificate.Instance.vSupp :
          Verifier S

          Verifier with the degenerate support bound supportLb.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Sundog.Certificate.Instance.vCol :
            Verifier S

            Verifier with the non-degenerate column-weight bound colWeightLb.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For

              Display instance for the three-valued verdict. #

              source
              @[implicit_reducible]
              instance Sundog.Certificate.Instance.instToStringVerdict :
              ToString Verdict
              Equations
              • One or more equations did not get rendered due to their size.

              The six test bodies as Fin 4 → ZMod 2 vectors. #

              source
              def Sundog.Certificate.Instance.y0000 :
              Fin 4 → ZMod 2

              Test body 0000: the zero vector (a codeword).

              Equations
              Instances For
                source
                def Sundog.Certificate.Instance.y0010 :
                Fin 4 → ZMod 2

                Test body 0010: weight-one error inside the code's support.

                Equations
                Instances For
                  source
                  def Sundog.Certificate.Instance.y1000 :
                  Fin 4 → ZMod 2

                  Test body 1000: weight-one error on a syndrome coordinate.

                  Equations
                  Instances For
                    source
                    def Sundog.Certificate.Instance.y0011 :
                    Fin 4 → ZMod 2

                    Test body 0011: weight-two body that is itself a codeword.

                    Equations
                    Instances For
                      source
                      def Sundog.Certificate.Instance.y1100 :
                      Fin 4 → ZMod 2

                      Test body 1100: weight-two error on both syndrome coordinates.

                      Equations
                      Instances For
                        source
                        def Sundog.Certificate.Instance.y1110 :
                        Fin 4 → ZMod 2

                        Test body 1110: weight-three body mixing syndrome and code coordinates.

                        Equations
                        Instances For

                          The verdict table — BOTH verifiers on each body. #

                          Format per line: "input  vSupp  vCol".

                          Axiom audit. #