OAI/Combinatorics/ContingencyTables/Machines/PairedFactorialProgram.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

The exact factorial multiplier from the encoded paired state

Every factorial argument is bounded by the supplied code length. In a valid code each cell block has length twice its capacity, so the computed denominator is exactly the manuscript's capacity factorial.

  1. def OAI.ContingencyTables.PairedFactorialProgram.sideFactor line 19
  2. def OAI.ContingencyTables.PairedFactorialProgram.sideFactorRealizer line 20
  3. lemma OAI.ContingencyTables.PairedFactorialProgram.polynomial_sideFactor line 21
  4. def OAI.ContingencyTables.PairedFactorialProgram.pairCount line 27
  5. def OAI.ContingencyTables.PairedFactorialProgram.pairCountRealizer line 28
  6. lemma OAI.ContingencyTables.PairedFactorialProgram.polynomial_pairCount line 30
  7. def OAI.ContingencyTables.PairedFactorialProgram.denominator line 34
  8. def OAI.ContingencyTables.PairedFactorialProgram.denominatorRealizer line 35
  9. lemma OAI.ContingencyTables.PairedFactorialProgram.polynomial_denominator line 36
  10. def OAI.ContingencyTables.PairedFactorialProgram.numerator line 41
  11. def OAI.ContingencyTables.PairedFactorialProgram.numeratorRealizer line 42
  12. lemma OAI.ContingencyTables.PairedFactorialProgram.polynomial_numerator line 50
  13. def OAI.ContingencyTables.PairedFactorialProgram.rowRatio line 57
  14. def OAI.ContingencyTables.PairedFactorialProgram.rowRatioRealizer line 59
  15. lemma OAI.ContingencyTables.PairedFactorialProgram.polynomial_rowRatio line 61
  16. def OAI.ContingencyTables.PairedFactorialProgram.output line 65
  17. def OAI.ContingencyTables.PairedFactorialProgram.outputRealizer line 67
  18. theorem OAI.ContingencyTables.PairedFactorialProgram.polynomial_output line 70
  19. lemma OAI.ContingencyTables.PairedFactorialProgram.rowRatio_value line 74
  20. theorem OAI.ContingencyTables.PairedFactorialProgram.output_canonical line 87
  21. theorem OAI.ContingencyTables.PairedFactorialProgram.output_physical line 110

    Source documentation

    The multiplier used by the executed weight oracle is the literal factorial ratio, for every subset, not just transversal states.

    theorem output_physical (S : Set (Labels A × Bool)) :
    TreeFraction.val (output (List.ofFn (CompanionComputedInitial.capacities A),
      encodeSet (CompanionComputedInitial.coordinateOrder A) S))=
        CompanionWeightOracle.factorialRatio A S := by
…

    Mentions: OAI.ContingencyTables.PairedFactorialProgram.output, OAI.ContingencyTables.CompanionComputedInitial.capacities, OAI.ContingencyTables.CompanionComputedInitial.coordinateOrder, OAI.ContingencyTables.CompanionWeightOracle.factorialRatio