OAI/Combinatorics/ContingencyTables/Counting/CompanionTraceProgram.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Polynomial code for recognizing and locating a trace return

The paired plain-state test sums the two bits of each label. The return program scans the supplied path after its initial state; no enumeration of the exponential paired-state space occurs.

  1. def OAI.ContingencyTables.CompanionTraceProgram.pairedPlainTest line 20
  2. def OAI.ContingencyTables.CompanionTraceProgram.pairedPlainTestRealizer line 24
  3. theorem OAI.ContingencyTables.CompanionTraceProgram.polynomial_pairedPlainTest line 30
  4. abbrev OAI.ContingencyTables.CompanionTraceProgram.ReturnInput line 38
  5. def OAI.ContingencyTables.CompanionTraceProgram.firstPlainCode line 40
  6. def OAI.ContingencyTables.CompanionTraceProgram.firstPlainCodeRealizer line 43
  7. theorem OAI.ContingencyTables.CompanionTraceProgram.polynomial_firstPlainCode line 47
  8. def OAI.ContingencyTables.CompanionTraceProgram.returnCode line 53

    Source documentation

    Strict first return: the initial path entry is omitted.

    def returnCode (z : ReturnInput) : Option (List ℕ) :=
…

    Mentions: OAI.ContingencyTables.CompanionTraceProgram.ReturnInput

  9. def OAI.ContingencyTables.CompanionTraceProgram.returnCodeRealizer line 56
  10. theorem OAI.ContingencyTables.CompanionTraceProgram.polynomial_returnCode line 59
  11. theorem OAI.ContingencyTables.CompanionTraceProgram.pairedPlainTest_encode line 66
  12. theorem OAI.ContingencyTables.CompanionTraceProgram.firstPlainCode_encode line 90

    Source documentation

    The list program returns the encoding of the same first plain state as the semantic scan, including the no-return outcome.

    theorem firstPlainCode_encode (A : Instance I J) (xs : List (State A)) :
    firstPlainCode (pairCatalog A,xs.map (fun S => encodeSet (coordinateEquiv A) S.val))=
      (firstHit (plainPredicate TwoLiftStates.pairs) xs).map
        (fun T => encodeSet (coordinateEquiv A) T.val.val) := by
…

    Mentions: OAI.ContingencyTables.CompanionTraceProgram.firstPlainCode, OAI.ContingencyTables.TwoLiftStates.pairs

  13. theorem OAI.ContingencyTables.CompanionTraceProgram.returnCode_encode line 109