4f-fluid-lec Transaction-level (accepted-stream) equivalence for elastic valid/retry interfaces

4f = maybe; needs more thought before committing. Promoted from the Pre-TODO bullet of 16/06/2026.

Idea

• accepted := valid && !retry; compare the sequence of accepted transactions rather than cycle-by-cycle waveforms, so retiming / elastic buffering / latency-changing optimizations remain equivalent — exactly the transformations cycle-accurate LEC (and flop correspondence) rejects by construction.
• Collapse two elastic regions into one Shared Stream Transformer (symbolic state advancing only on accept) and run a reduced BMC over accepted steps.
• Long-term: make elasticity a first-class IR property (TransactionStream<T>) so the equivalence obligation is generated, not reverse-engineered.

Before committing (the think-more part)

• Work one micro-example end-to-end by hand: a 2-stage vs 3-stage elastic FIFO pipeline — what exactly is the symbolic state, what is the accepted-step transition relation, and what does the miter compare?
• Decide the interface-discovery story: user annotation (fluid lambdas, 3f-fluid) vs structural inference of valid/retry pairs.
• Fairness/deadlock: accepted-sequence equality says nothing about liveness — scope the verdict wording so a PASS is not read as "makes progress".

Research track on top of the 2f-lec engine; pairs with the 3f-fluid elastic lowering. The full brainstorming text is in git history (old pass/lec/lec.md Appendix A).