Monotonicity proof

Stream: lean4

[Travis Smith]

Hi everyone! I’ve just posted a preprint and a Lean 4 formalization of a simple monotonicity proof. It’s all in one file (theorems.lean), which you can run in the Lean 4 web IDE, and there’s also a Python prototype for experiments.

I’d be extremely grateful for any feedback on:
  • Lean style / idiomatic Mathlib usage  
  • Proof structure and best practices  
  • General paper comments (organization, clarity, etc.)  

Code & proofs:
https://github.com/rewriteunity/rewrite-normalization/blob/main/lean_proof/RewriteCollapse/theorems.lean  
Preprint:  
https://zenodo.org/records/15736729  
Thanks in advance!

[Aaron Liu]

Why the ∧ True?

/-- Master theorem: going to the collapseical result never increases `EDown`. -/
theorem generalcollapseical {α : Type _} [DecidableEq α]
  (R : RuleSet α) (μ : α → Nat) (S : Finset α) :
  EDown (collapseResult μ S R) μ S ≤ EDown R μ S ∧ True :=
    ⟨collapseMinimal μ S R, trivial⟩

[Travis Smith]

That was a left over boilerplate remark from development. I just completed the proof and am, frankly, new to lean, so that was a mistake.
Looking at it, I can see it's because I posted a slightly outdated version after I had issues with getting imports to work correctly. That's also the reason for the incorrect theorem name, which should be generalCollapse. I apologize for any mistakes and appreciate you looking at it.