Distinct odd covering system

Decide whether the four-prime weight-function theorem can be rigorously repaired.

First action: Test and then prove or falsify |C_d intersection W|/|W| <= product over support of p^(-b)(p-1)/(p-2), beginning with exact exhaustive controls for primes {3,5,7} and exponents <=3.

Stop or redirect when: Stop at the first exact counterexample; otherwise stop after a complete proof and novelty audit determine whether the resulting theorem is valid and new.

• Repair or refute the four-prime weight-region argument using normalized intersection ratios.
  Exhaust tower assignments at primes 3,5,7 and exponents at most 3 using exact Fractions.
• Machine-check published condensed covering trees.
  Define a JSON split-tree schema and encode the published t_15 <= 4 construction.
• Seek a square-free near-cover with one prime repeated exactly twice.
  After tree tooling exists, encode the published tau_7 <= 6 tree and test a bounded replacement grammar.

• counterexample-guided inductive synthesis
  Use a verified split-tree grammar to replace repeated leaves while retaining counterexample CRT fibres.
• symbolic and congruence family discovery
  Replace absolute weight-region cardinalities by normalized CRT fibre ratios and sum geometric prime-power towers.
• isolated adversarial reconstruction
  Compare exact source hypotheses with claimed encodings, isolate the smallest exact discrepancy, and validate witness tooling using independent algorithms.
  Reopen only if: For the few-prime route, establish a corrected normalized-region lemma handling arbitrary tower overlaps and edge cases; for the Lean route, replace both custom axioms with proofs.

• Use the April 2026 four-prime proof as written to prune search.
  The asserted exact cardinality is false for overlapping tower congruences.
  Reopen only if: Supply and independently audit a corrected actual-region or weighted-region proof.
• Treat the May 2026 Lean repository as an unconditional resolution.
  Its main theorem depends on two custom axioms not supplied by the cited BBMST results.
  Reopen only if: Replace both custom axioms with faithful proofs.
• Odd LCM search avoiding both 9 and 15.
  Published BBMST work excludes the entire scope.
  Reopen only if: A demonstrated error in the published theorem.
• Square-free or p<=73-square-free candidate search.
  Published BBMST work excludes the entire scope.
  Reopen only if: A demonstrated error in the published theorem.