feat(abi): close TacticRecord round-trip lemmas (closes #152)

Discharges the two round-trip lemmas deferred at lines 88-93 and
187-196 of `src/abi/EchidnaABI/TacticRecord.idr`:

    natToFinToNat        : Nat → 0 LT n (S MaxConfidence) →
                           finToNat (natToFinLT n) = n
    clampRoundtripInRange: Nat → LT n (S MaxConfidence) →
                           finToNat (clampConfidence n) = n

Approach — what the original deferral comment got nearly right:

The note "requires careful LTE-weakening that has not yet been spelled
out structurally" identified a real symptom but mis-located the cause.
The trap is a unification artefact, not a missing weakening lemma:
specialising the round-trip at `S MaxConfidence` forces the recursive
call to discharge `LTE (S k) (S MaxConfidence)` while the LTESucc
pattern only hands you `LTE (S k) MaxConfidence` — the same proposition
off-by-one. Explicit weakening with `lteSuccRight` works but is
inelegant.

Cleaner shape: introduce a polymorphic helper

    finToNatNatToFinLT :
      (n : Nat) -> {m : Nat} -> (0 prf : LT n m) ->
      finToNat (natToFinLT n {prf}) = n

with `m` implicit so the recursive call's `m` is structurally inferred
to the predecessor — the LTESucc constraint then matches exactly,
no glue. The `S MaxConfidence` instance specialises in one line.

`clampRoundtripInRange` closes by `with`-abstracting on the same
`isLT n (S MaxConfidence)` that `clampConfidence` inspects: the Yes
branch reduces and discharges via `natToFinToNat`, the No branch is
contradicted by the in-range hypothesis via `absurd`.

Verification:

  - Module type-checks clean on Idris2 0.8.0
    `idris2 --check EchidnaABI/TacticRecord.idr` → 1/1: Building OK
  - All three new lemmas confirmed total via `:total` REPL
  - Constraint preserved: zero believe_me, zero postulates, zero admits,
    zero assert_total. Only standard-library inhabitants used.

Refs the deferred proof debt called out in commit 4118893 (the
introducing change for TacticRecord.idr).

Author: hyperpolymath

src/abi/EchidnaABI/TacticRecord.idr

@@ -85,12 +85,38 @@ clampConfidence n = case isLT n (S MaxConfidence) of
   Yes prf => natToFinLT n
   No _    => last  -- saturate to MaxConfidence
 
--- Round-trip lemma `natToFinToNat` is desirable but requires careful
--- LTE-weakening that has not yet been spelled out structurally. The
--- absence of this lemma here is INTENTIONAL: the file ships with the
--- comparison total order proven and the round-trip property captured
--- as a Wave-3 sub-issue rather than a believe-me hole. See issue
--- breadcrumb at the top of this file.
+------------------------------------------------------------------------
+-- natToFinLT / finToNat Round-Trip
+------------------------------------------------------------------------
+
+-- The LTE-weakening worry recorded in the original deferral comment was
+-- a unification trap, not a missing lemma. Specialising on
+-- `S MaxConfidence` directly forces the recursive call to see
+-- `LTE (S k) MaxConfidence`, but the recursive obligation needs
+-- `LTE (S k) (S MaxConfidence)` — the same proposition off-by-one.
+-- The polymorphic helper sidesteps the trap: with `m` implicit the
+-- recursive `m` is inferred to the structural predecessor, so the
+-- LTESucc pattern matches without explicit weakening. The
+-- `S MaxConfidence` instance is then a one-line specialisation.
+
+||| Generic round-trip: every nat strictly below `m` is faithfully
+||| recovered by `finToNat . natToFinLT`. Polymorphic in `m` so the
+||| recursion's implicit upper bound shrinks structurally and the
+||| LTESucc pattern can be unpacked without `lteSuccRight` glue.
+public export
+finToNatNatToFinLT :
+  (n : Nat) -> {m : Nat} -> (0 prf : LT n m) ->
+  finToNat (natToFinLT n {prf}) = n
+finToNatNatToFinLT 0     (LTESucc _)  = Refl
+finToNatNatToFinLT (S k) (LTESucc lt) = cong S (finToNatNatToFinLT k lt)
+
+||| In-range nat ↔ ConfidenceFP round-trip. Discharges the round-trip
+||| obligation flagged at lines 88-93 of the original file.
+public export
+natToFinToNat :
+  (n : Nat) -> (0 prf : LT n (S MaxConfidence)) ->
+  finToNat (natToFinLT n {prf}) = n
+natToFinToNat n prf = finToNatNatToFinLT n prf
 
 ------------------------------------------------------------------------
 -- Comparison: by confidence, descending
@@ -188,9 +214,15 @@ confidenceFloatZero = Refl
 -- ABI Roundtrip Invariant
 ------------------------------------------------------------------------
 
--- clampRoundtripInRange is deferred along with natToFinToNat above;
--- the constructive round-trip proof requires the in-range
--- nat-fin-nat lemma which is the Wave-3 sub-issue. The clamp
--- operation itself is total and that totality is verified by
--- Idris2's pattern-matching exhaustiveness on the `with` of
--- `isLT n (S MaxConfidence)`.
+||| Clamp is the identity on in-range inputs. The `with`-abstraction
+||| pivots on the very `isLT n (S MaxConfidence)` that `clampConfidence`
+||| inspects, so the `Yes` branch reduces the case and we discharge it
+||| via the round-trip lemma; the `No` branch is contradicted by the
+||| in-range hypothesis, closed by `absurd`. Total, no admits.
+public export
+clampRoundtripInRange :
+  (n : Nat) -> (prf : LT n (S MaxConfidence)) ->
+  finToNat (clampConfidence n) = n
+clampRoundtripInRange n prf with (isLT n (S MaxConfidence))
+  _ | Yes prf' = natToFinToNat n prf'
+  _ | No nlt   = absurd (nlt prf)