OAI/Probability/RandomSAT/Main.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

For every fixed clause size at least three, the proper-clause satisfiability probability has a positive finite limiting threshold. No conclusion is asserted at the critical density.

  1. def OAI.FixedClauseThreshold.limitingCenter line 19
  2. theorem OAI.FixedClauseThreshold.center_tendsto line 21
  3. theorem OAI.FixedClauseThreshold.limitingCenter_bounds line 37
  4. theorem OAI.FixedClauseThreshold.limitingCenter_pos line 43
  5. theorem OAI.FixedClauseThreshold.limitingCenter_lt_cap line 46
  6. theorem OAI.FixedClauseThreshold.floor_density_le_cap line 53
  7. theorem OAI.FixedClauseThreshold.subcritical_limit line 60
  8. theorem OAI.FixedClauseThreshold.supercritical_limit_below_cap line 84
  9. theorem OAI.FixedClauseThreshold.supercritical_limit line 109
  10. theorem OAI.FixedClauseThreshold.main line 122

    Distinct definitions of this name: ComparatorChallenges/FixedClauseThreshold.lean:51 (same statement text; different proof or body). Qualify references as OAI.FixedClauseThreshold.main@path.