OAI/Probability/RandomSAT/Model.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Proper clauses choose distinct variables with independent fair signs. Formulas are independent clause draws with replacement, and their satisfiability probability is the literal finite cardinality ratio. The empty formula is satisfiable. When there are fewer variables than literals, nonempty formula lengths have probability zero by the convention that division by zero is zero. The threshold assertion concerns fixed clause size and fixed density only, with no assertion at the critical density.

  1. abbrev OAI.FixedClauseThreshold.Assignment line 17

    Also declared: ComparatorChallenges/FixedClauseThreshold.lean:21 (same declaration text), ComparatorChallenges/SATComputability.lean:7 (same declaration text).

  2. abbrev OAI.FixedClauseThreshold.ProperClause line 19

    Also declared: ComparatorChallenges/FixedClauseThreshold.lean:23 (same declaration text), ComparatorChallenges/SATComputability.lean:9 (same declaration text).

  3. abbrev OAI.FixedClauseThreshold.Formula line 22

    Also declared: ComparatorChallenges/FixedClauseThreshold.lean:26 (same declaration text), ComparatorChallenges/SATComputability.lean:12 (same declaration text).

  4. def OAI.FixedClauseThreshold.SatisfiesClause line 24

    Also declared: ComparatorChallenges/FixedClauseThreshold.lean:28 (same declaration text), ComparatorChallenges/SATComputability.lean:14 (same declaration text).

  5. def OAI.FixedClauseThreshold.Satisfies line 27

    Also declared: ComparatorChallenges/FixedClauseThreshold.lean:31 (same declaration text), ComparatorChallenges/SATComputability.lean:17 (same declaration text).

  6. def OAI.FixedClauseThreshold.Satisfiable line 30

    Also declared: ComparatorChallenges/FixedClauseThreshold.lean:34 (same declaration text), ComparatorChallenges/SATComputability.lean:20 (same declaration text).

  7. def OAI.FixedClauseThreshold.properSATProbability line 33

    Also declared: ComparatorChallenges/FixedClauseThreshold.lean:37 (same declaration text), ComparatorChallenges/SATComputability.lean:23 (same declaration text).

  8. def OAI.FixedClauseThreshold.HasLimitingThreshold line 38

    Also declared: ComparatorChallenges/FixedClauseThreshold.lean:42 (same declaration text).