Add README describing the Lean 4 proof structure

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

Author: nathanael-fijalkow

README.md

@@ -1 +1,34 @@
-# bolt_lean
+# BoltLean
+
+Lean 4 mechanized proofs for the paper "Bolt: LTLf and LTL Learning Meet Boolean Set Cover".
+
+The development is self-contained and does not depend on Mathlib or any external library beyond the Lean 4 core.
+It is built with Lean 4 version `v4.29.1` (see `lean-toolchain`).
+
+## Structure
+
+The repository is organized into two modules corresponding to the two main theoretical parts of the paper.
+
+### `BoltLean/Ltl/`
+
+**`Basic.lean`**
+Defines `LTLf` formulas in negation normal form (`Formula`) and their semantics (`Formula.accepts`) on finite traces (`Trace`).
+Negations are pushed to variables; the operators are `True`, `False`, `Var`, `Next`, `WeakNext`, `Globally`, `Finally`, `Or`, `And`, and `Until`.
+
+**`UpperBound.lean`**
+Proves the separability upper bound: for any non-empty finite trace `t`, the function `Trace.exact t` constructs an `LTLf` formula accepted by `t` and only by `t`.
+Taking the disjunction over all positive traces then yields a separating formula for any consistent set of examples.
+
+### `BoltLean/Boolean/`
+
+**`Basic.lean`**
+Defines Boolean formulas in negation normal form (`BoolFormula`) over a set of atomic sets indexed by `Fin n_sets`.
+A `Valuation` records membership of an element in each atomic set.
+Also defines the domination preorder: `f1.dominates f2` holds when `f1` has no greater weight than `f2` and correctly classifies a superset of the elements that `f2` classifies correctly.
+
+**`Domination.lean`**
+Proves the key substitution lemma `domin_replace`: if `f1` dominates `f2`, then replacing any occurrence of `f2` by `f1` in a Boolean formula yields a formula that dominates the original.
+This is the formal justification for pruning the candidate family to an antichain during the Boolean Set Cover search.
+
+**`UpperBound.lean`**
+Proves the Boolean Set Cover upper bound: `Valuation.exact v` constructs a Boolean formula accepted by exactly the valuation `v`, establishing that a separating formula always exists when the instance is feasible.