Documentation

Complexitylib.Metacomplexity.NisanWigderson.Reconstruction.Program.Encoding.Defs

Bit encoding of explicit NW reconstruction programs -- definitions #

Every stored Boolean in a reconstruction program is represented by one member of a finite linearly ordered payload-index type: predecessor-table entries, outside-seed bits, later-tail bits, and finally the candidate bit. Encoding the associated Boolean function therefore produces one flat, canonically ordered bit string. The polarity and coordinate remain explicit codec metadata.

source
@[reducible, inline]
abbrev Complexity.NWDesign.ReconstructionPredecessorPayloadIndex {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (current : Fin outputLength) :
Type

Lexicographically ordered indices of all stored predecessor-table entries.

Equations
Instances For
    source
    @[reducible, inline]
    abbrev Complexity.NWDesign.ReconstructionPayloadIndex {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (current : Fin outputLength) :
    Type

    Canonically ordered indices of every Boolean in a reconstruction payload.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Complexity.NWDesign.predecessorPayloadIndex {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (current : Fin outputLength) (previous : ↥(Finset.Iio current)) (assignment : ↥(design.challengeOverlap current ↑previous) → Bool) :
      design.ReconstructionPayloadIndex current

      Inject one predecessor-table entry into the total payload index.

      Equations
      Instances For
        source
        def Complexity.NWDesign.outsidePayloadIndex {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (current : Fin outputLength) (coordinate : ↥(design.outsideCoordinates current)) :
        design.ReconstructionPayloadIndex current

        Inject one outside-seed coordinate into the total payload index.

        Equations
        Instances For
          source
          def Complexity.NWDesign.laterPayloadIndex {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (current : Fin outputLength) (coordinate : ↥(laterCoordinates current)) :
          design.ReconstructionPayloadIndex current

          Inject one later-tail coordinate into the total payload index.

          Equations
          Instances For
            source
            def Complexity.NWDesign.candidatePayloadIndex {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (current : Fin outputLength) :
            design.ReconstructionPayloadIndex current

            Index of the final candidate bit in the total payload.

            Equations
            Instances For
              source
              def Complexity.NWDesign.ReconstructionProgram.booleanPayload {outputLength inputLength seedLength : ℕ} {design : NWDesign outputLength inputLength seedLength} (program : design.ReconstructionProgram) :
              design.ReconstructionPayloadIndex program.current → Bool

              Regard the explicit program fields as one Boolean function on the total payload-index type.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def Complexity.NWDesign.ReconstructionProgram.encodeBooleanPayload {outputLength inputLength seedLength : ℕ} {design : NWDesign outputLength inputLength seedLength} (program : design.ReconstructionProgram) :
                List Bool

                Canonical flat encoding of all Boolean payload fields. The program's polarity and coordinate are not included.

                Equations
                Instances For
                  source
                  def Complexity.NWDesign.ReconstructionProgram.encode {outputLength inputLength seedLength : ℕ} {design : NWDesign outputLength inputLength seedLength} (program : design.ReconstructionProgram) :
                  List Bool

                  Complete program-specific encoding: polarity, fixed-width hybrid coordinate, and the flat Boolean reconstruction payload. The ambient design parameters remain external to the codec.

                  Equations
                  Instances For
                    source
                    def Complexity.NWDesign.decodeReconstructionBooleanPayload? {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (complement : Bool) (current : Fin outputLength) (bits : List Bool) :
                    Option design.ReconstructionProgram

                    Decode a flat Boolean payload using an externally supplied polarity and hybrid coordinate.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      def Complexity.NWDesign.decodeReconstructionProgram? {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (bits : List Bool) :
                      Option design.ReconstructionProgram

                      Decode a complete reconstruction program relative only to its ambient design parameters.

                      Equations
                      Instances For