formal: compositional adequacy of differential dataflow operators

[frankmcsherry]

Adds formal/Differential/Compositional.lean: a machine-checked account of the axis
orthogonal to the interesting-times/compaction work already in Coverage/Model — that
differential computation abstractly produces the right thing, and composes.

The single claim: each operator, as a transformation of difference traces, computes what
re-evaluating its mathematics moment by moment would — Adequate D impl := acc ∘ impl = D ∘ acc
— and these squares compose, so any program built from the operators maintains the value it was
meant to compute. All axiom-clean (propext, Classical.choice, Quot.sound; no sorryAx),
nothing sorryed.

What's proved

• Spine. acc_injective (a trace is determined by its accumulation, so the implementing
  trace is unique), the Adequate square, and its composition law Adequate.comp — correctness
  of a program reduces to correctness of its pieces.
• Operator squares. linImpl_adequate (LINEAR/SUM), timeImpl_adequate (enter/temporal,
  via a Galois adjoint), reduce_adequate (REDUCE — its existence half is exactly
  Coverage.exists_diff_trace_comp), and join_adequate (JOIN as a bilinear convolution =
  bilinearity + sup_le_iff).
• Capstone. Program.adequate over id / linear / reduce / par / join / seq, by induction
  (JOIN is Adequate.join, a bilinear par).
• Incremental refinement. Refines (per-batch increment) composes by a discrete chain rule
  (Refines.comp) — this is why difference traces are the composable interface between operators;
  the locality that makes the increment cheap for the nonlinear REDUCE is precisely the
  interesting-times argument of Coverage/Model.
• ITERATE. Over an iteration coordinate T × ℕ: round_matches/iterate_program (the loop's
  accumulated output is the from-scratch iteration of the body's denotation), leave_stabilizes
  (stabilization is free from finite support — no termination hypothesis), leave_fixpoint with
  re-add (leave_fixpoint_enter) and start-from-X (leave_fixpoint_impulse) regimes, and, for a
  DELAY-ing (Causal) body, acc_unique — any two solutions accumulate identically, i.e.
  evaluation-order independence is the adequacy statement. acc_prod_fst shows mutual recursion
  needs no product lemma.

Two commits

1. Compositional adequacy — the new file (purely additive: one file + one import line).
2. Extract the accumulation core into Differential/Basic.lean — acc and its group-hom API
   move out of Model.lean (where the abstraction layer was borrowing a primitive) into a
   foundational file imported by both Model and Compositional. Semantics-preserving:
   Model.streamCorrectness_holds and everything else stays axiom-clean. Coverage's
   Represents/Cut/Simple are left in place.

Each commit builds on its own. Deferred (noted in the file header): a typed Program X Y for
verified program transformations and key/value-changing joins, and the confluence question of
when different arrival schedules compute the same value (distinct from the adequacy proved here).

Nothing in the Rust workspace depends on formal/, and no CI gates on it. The README's
Contents and axiom-check instructions are updated.

🤖 Generated with Claude Code