fix(framework): complete and wire in the Progressive assurance proofs

Ochrance.Framework.Progressive was a dead orphan (not in any ipkg) with an
incomplete Ord instance ('-- ... [Remaining cases]') and an undefined 'atLeast',
so its SatisfiesMinimum / attestedSatisfiesLax threshold proof could not check.

- Define rank/atLeast, add Eq, complete the Ord instance (the same fix already
  landed in ochrance-framework).
- Add the module to ochrance.ipkg so the threshold proof is now built and
  CI-verified rather than dead code.

Verified: ochrance.ipkg builds 16/16; attestedSatisfiesLax and atLeast are total.

Author: Claude

ochrance-core/Ochrance/Framework/Progressive.idr

@@ -23,13 +23,29 @@ module Ochrance.Framework.Progressive
 public export
 data VerificationMode = Lax | Checked | Attested
 
-||| ORDERING: Defines the relationship Lax < Checked < Attested.
+||| RANK: numeric strictness, with Lax < Checked < Attested.
+public export
+rank : VerificationMode -> Nat
+rank Lax      = 0
+rank Checked  = 1
+rank Attested = 2
+
+||| Is `mode` at least as strict as `threshold`?
+public export
+atLeast : (threshold : VerificationMode) -> (mode : VerificationMode) -> Bool
+atLeast threshold mode = rank threshold <= rank mode
+
+public export
+Eq VerificationMode where
+  Lax      == Lax      = True
+  Checked  == Checked  = True
+  Attested == Attested = True
+  _        == _        = False
+
+||| ORDERING: Defines the relationship Lax < Checked < Attested via `rank`.
 public export
 Ord VerificationMode where
-  compare Lax      Lax      = EQ
-  compare Lax      _        = LT
-  compare Checked  Attested = LT
-  -- ... [Remaining cases]
+  compare x y = compare (rank x) (rank y)
 
 --------------------------------------------------------------------------------
 -- Proof Witnesses

ochrance.ipkg

@@ -17,6 +17,7 @@ modules = Ochrance.A2ML.Types
         , Ochrance.Framework.Interface
         , Ochrance.Framework.Proof
         , Ochrance.Framework.Error
+        , Ochrance.Framework.Progressive
         , Ochrance.FFI.Crypto
         , Ochrance.Util.Hex
         , Ochrance.Filesystem.Types