OAI/Combinatorics/ContingencyTables/Machines/FractionAcceptanceProgram.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Binary execution of the rational acceptance coin

The integer quotient computes the exact floor threshold used by the finite-word acceptance law. The word length controls all powering and word traversal, even for malformed fraction inputs.

  1. abbrev OAI.ContingencyTables.FractionAcceptanceProgram.Input line 17
  2. def OAI.ContingencyTables.FractionAcceptanceProgram.scaledNumerator line 19
  3. def OAI.ContingencyTables.FractionAcceptanceProgram.scaledNumeratorRealizer line 21
  4. lemma OAI.ContingencyTables.FractionAcceptanceProgram.polynomial_scaledNumerator line 26
  5. def OAI.ContingencyTables.FractionAcceptanceProgram.threshold line 31
  6. def OAI.ContingencyTables.FractionAcceptanceProgram.thresholdRealizer line 33
  7. lemma OAI.ContingencyTables.FractionAcceptanceProgram.polynomial_threshold line 38
  8. def OAI.ContingencyTables.FractionAcceptanceProgram.acceptCode line 42
  9. def OAI.ContingencyTables.FractionAcceptanceProgram.acceptCodeRealizer line 44
  10. theorem OAI.ContingencyTables.FractionAcceptanceProgram.polynomial_acceptCode line 49
  11. lemma OAI.ContingencyTables.FractionAcceptanceProgram.fraction_threshold line 56
  12. theorem OAI.ContingencyTables.FractionAcceptanceProgram.acceptCode_ofFn line 73

    Source documentation

    The compiled decision agrees on every Boolean word with the rational threshold used in the proved companion transition law.

    theorem acceptCode_ofFn (q : TreeFraction.Fraction) (B : ℕ) (bits : Fin B → Bool) :
    acceptCode (q,List.ofFn bits)=decide (FairBits.rationalThresholdAccept B (TreeFraction.val q) bits) := by
…

    Mentions: OAI.ContingencyTables.FractionAcceptanceProgram.acceptCode, OAI.ContingencyTables.FairBits.rationalThresholdAccept