OAI/Combinatorics/ContingencyTables/Counting/CompanionNeighborProgram.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Executable valid-neighbor lists and their binary draw

This composes the actual integer-exchange program with the paired-state validator and the bounded list-index program. The output code is exactly the encoding of the semantic proposal, including its failure outcome.

  1. def OAI.ContingencyTables.CompanionNeighborProgram.validExchanges line 18
  2. def OAI.ContingencyTables.CompanionNeighborProgram.validExchangesRealizer line 21
  3. theorem OAI.ContingencyTables.CompanionNeighborProgram.polynomial_validExchanges line 25
  4. def OAI.ContingencyTables.CompanionNeighborProgram.codeProposal line 30
  5. def OAI.ContingencyTables.CompanionNeighborProgram.codeProposalRealizer line 33
  6. theorem OAI.ContingencyTables.CompanionNeighborProgram.polynomial_codeProposal line 38

    Source documentation

    All loops traverse the supplied profile, pair catalog or quadratic coordinate list. A large binary draw index never determines a loop.

    theorem polynomial_codeProposal : PolynomialTime codeProposalRealizer :=
…

    Mentions: OAI.ContingencyTables.CompanionNeighborProgram.codeProposalRealizer

  7. lemma OAI.ContingencyTables.CompanionNeighborProgram.validExchanges_encode line 46
  8. theorem OAI.ContingencyTables.CompanionNeighborProgram.codeProposal_eq line 66

    Source documentation

    The public binary program computes the exact semantic draw.

    theorem codeProposal_eq (A : Instance I J) (S : State A)
    (bits : Fin (proposalBits A) → Bool) :
    codeProposal ((pairCatalog A,encodeSet (coordinateEquiv A) S.val),List.ofFn bits)=
      (CompanionArithmeticProposal.proposal A S bits).map
        (fun T => encodeSet (coordinateEquiv A) T.val) := by
…

    Mentions: OAI.ContingencyTables.CompanionNeighborProgram.codeProposal, OAI.ContingencyTables.CompanionArithmeticProposal.proposal