# Book VI ch.6, MolecularCascade.lean: compiler output, run by the author on 2026-11-03
# command: cd ~/Desktop/geometry && lake env lean book6/MolecularCascade.lean 2>&1 | tee book6/molecularcascade.axioms.txt
# result: no errors; one warning (push_neg deprecated, line 82); 16 theorems, none depends on sorryAx
book6/MolecularCascade.lean:82:4: warning: `push_neg` has been deprecated. Prefer using `push Not` instead.
If you'd rather continue using `push_neg` in your project, you can implement it as follows:
```
open Lean.Parser.Tactic in
macro "push_neg" cfg:optConfig loc:(location)? : tactic =>
  `(tactic| push $cfg:optConfig Not $[$loc]?)
```
'Book6Molecular.net_error_le_first' depends on axioms: [propext, Classical.choice, Quot.sound]
'Book6Molecular.net_error_le_second' depends on axioms: [propext, Classical.choice, Quot.sound]
'Book6Molecular.double_sieve_example' depends on axioms: [propext, Classical.choice, Quot.sound]
'Book6Molecular.required_pass_fraction' depends on axioms: [propext, Classical.choice, Quot.sound]
'Book6Molecular.required_examples' depends on axioms: [propext, Classical.choice, Quot.sound]
'Book6Molecular.no_gain_if_passes_all' depends on axioms: [propext, Classical.choice, Quot.sound]
'Book6Molecular.strict_gain_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'Book6Molecular.nmd_no_flag_last_exon' depends on axioms: [propext, Quot.sound]
'Book6Molecular.nmd_no_flag_within' depends on axioms: [propext, Quot.sound]
'Book6Molecular.nmd_flag_upstream_monotone' depends on axioms: [propext, Quot.sound]
'Book6Molecular.nmd_threshold_antitone' depends on axioms: [propext, Quot.sound]
'Book6Molecular.nmd_band' depends on axioms: [propext, Classical.choice, Quot.sound]
'Book6Molecular.nmd_band_example' depends on axioms: [propext, Classical.choice, Quot.sound]
'Book6Molecular.misincorporation_inside_window' depends on axioms: [propext, Classical.choice, Quot.sound]
'Book6Molecular.improvement_factors' depends on axioms: [propext, Classical.choice, Quot.sound]
'Book6Molecular.old_vs_new_low_end' depends on axioms: [propext, Classical.choice, Quot.sound]