idempotent tower constructions with weight filtrations

Stream: new members

[Harikrishnan R]

We are formalizing idempotent tower constructions with weight filtrations in Lean 4. We face 5 blocking issues involving Lean 4 tactic/API usage and mathematical proof gaps. Below is a concise MWE combining all issues as clear questions.

---

1. Tactic rewrite failure when unfolding structure function fields

We have a structure with function fields and want to rewrite/unfold them, but get an error:

structure MySystem (α : Type*) where
  weight_func : ℕ → α → α
  shape_func : α → α
  zero_elem : α

variable {α : Type*} (S : MySystem α)

example (x : α) (i : ℕ) :
  S.weight_func i (S.shape_func x) = S.zero_elem := by
  rw [S.weight_func]  -- Error: tactic 'rewrite' failed, equality or iff proof expected
  sorry

Questions:

• How to properly rewrite or unfold function fields inside structures?
• Should we mark these fields with attributes like @[simp] or @[reducible]?
• Are there better tactics than rw for this?

---

2. Lean 4 API error: Int.natCast unknown constant

We get the following error when trying to use Int.natCast:

example (i : Int) (h_neg : i < 0) : Int.natAbs i = Int.natCast (-i) := by
  sorry

Error message:

unknown constant 'Int.natCast'

Questions:

• What is the correct Lean 4 API to convert Int to Nat?
• How to express Int.natAbs i = (-i).natAbs for negative integers?
• Are there idiomatic ways to handle integer absolute values and coercions in Lean 4?

---

3. Mathematical logic flaw: i ≠ j does not imply Int.natAbs i ≠ Int.natAbs j

We assumed:

example (i j : Int) (h : i ≠ j) : Int.natAbs i ≠ Int.natAbs j := by sorry

But this is false, e.g., i = 2, j = -2 satisfy i ≠ j but Int.natAbs i = Int.natAbs j = 2.

Questions:

• How to handle cases where indices differ but have the same absolute value in orthogonality proofs?
• Should proofs split cases for |i| = |j| and |i| ≠ |j|?
• Is there a standard approach for signed index orthogonality?

---

4. Missing theorem for orthogonality of composed weight filtrations

Given:

structure AlgebraSystem (α : Type*) where
  weight_op : ℕ → α → α
  shape_op : α → α
  zero : α
  orthogonal_with_shape : ∀ i j x, i ≠ j → weight_op i (shape_op (weight_op j x)) = zero

variable {α : Type*} (A : AlgebraSystem α)

example (i j : ℕ) (x : α) (h : i ≠ j) :
  A.weight_op i (A.weight_op j x) = A.zero := by
  sorry

Questions:

• Is there a known principle to remove intermediate shape_op in orthogonality statements?
• Should we add a direct orthogonality axiom for composed operations?
• What properties of shape_op (idempotent, commutative) help prove this?

---

5. Missing finite support property for weight filtrations

We want to prove:

structure FilteredAlgebra (α : Type*) where
  weight_filtration : ℕ → α → α
  zero : α

variable {α : Type*} (F : FilteredAlgebra α)

example (x : α) : ∃ bound : ℕ, ∀ m ≥ bound, F.weight_filtration m x = F.zero := by
  sorry

Questions:

• Is finite support of weight filtrations a standard axiom or derivable?
• Can it be derived from nilpotency or boundedness?
• What are reasonable bounds (e.g., 10 or polynomial degree)?
• Should this be added as a new axiom or proven from fundamentals?

---

We appreciate any guidance on Lean 4 tactics, API usage, and mathematical proof strategies related to these issues. Please let us know if more context or code is needed.

Thank you!