OAI/Combinatorics/ContingencyTables/Counting/CompanionComputedProposal.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The companion proposal with computed metadata

The executable proposal receives only a binary profile and fresh bits. It computes the consecutive-pair catalog itself and scans coordinate exchanges. Its semantic law is the same ordered proposal law.

  1. def OAI.ContingencyTables.CompanionComputedProposal.proposalProgram line 20
  2. def OAI.ContingencyTables.CompanionComputedProposal.catalogInputRealizer line 23
  3. def OAI.ContingencyTables.CompanionComputedProposal.proposalProgramRealizer line 27
  4. theorem OAI.ContingencyTables.CompanionComputedProposal.polynomial_proposalProgram line 31
  5. def OAI.ContingencyTables.CompanionComputedProposal.pairLabels line 39
  6. lemma OAI.ContingencyTables.CompanionComputedProposal.pair_coordinate line 42
  7. lemma OAI.ContingencyTables.CompanionComputedProposal.generated_catalog line 49
  8. theorem OAI.ContingencyTables.CompanionComputedProposal.proposalProgram_eq line 63

    Source documentation

    Every proposed code is the encoding of the actual ordered proposal state, and unused binary indices give precisely the same none result.

    theorem proposalProgram_eq (S : State A) (bits : Fin (proposalBits A) → Bool) :
    proposalProgram (encodeSet (coordinateOrder A) S.val,List.ofFn bits)=
      (orderedProposal A (coordinateOrder A) S bits).map
        (fun T => encodeSet (coordinateOrder A) T.val) := by
…

    Mentions: OAI.ContingencyTables.CompanionComputedProposal.proposalProgram