[AI.a2ml] Add fuel-based-total-recursion idiomatic pattern #47

Proposal

Add a new (idiomatic-pattern) for fuel-based total recursion. The fuel pattern is the canonical way to make recursive parsers/interpreters provably total in a totality-checking language without sized types.

Source observation

ProvenBridge's mutual JSON parser used depth: Nat incremented per recursive call with if depth > 100 then bail. Idris2's totality checker can't see this as well-founded — depth increases. We had to relax to %default covering. The fix is to use fuel: a Nat that decreases structurally.

Suggested patch (LESSONS.md L3)

(pattern
  (name "fuel-based-total-recursion")
  (composition "Nat parameter + structural decrease")
  (purpose "Make recursive parsers / interpreters / search algorithms provably total without sized types.")
  (anti-pattern "Depth tracking with `if depth > N then bail` — runtime guarantee, not provable.")
  (sketch "fn parse(fuel: Nat, input: List Char): ... { match fuel { Z => Err(\"depth\"); S(f) => recurse(f, ...) } }"))

Filed from idaptik Wave 3 pilot. See LESSONS.md and PILOT.md. Idaptik commit hyperpolymath/idaptik@aef38db.