Cardano Updates

Complete the LEDGER preservation-of-value proof structure for Dijkstra.

- LEDGER-I: Fully proved via utxow-pov-invalid.
- LEDGER-V: Complete equational chain with no holes or unresolved metas.
  Decomposes into:
  - step-i: combined CERTS accounting (sub + top level)
  - arithmetic-1, arithmetic-2: ℕ rearrangements
  - step-iii-iv: batch UTxO + deposit accounting (assumption)
  - step-ii: applyDirectDeposits cancellation (assumption)

New sub-lemma proved:
- SUBLEDGERS-certs-pov: induction on ReflexiveTransitiveClosure showing
  rewardsBalance decreases by exactly the sum of sub-withdrawal amounts.
  Dispatches SUBLEDGER-I (impossible when isTopLevelValid ≡ true) and
  SUBLEDGER-V (uses sub-level CERTS-pov with NetworkId extracted from
  SUBUTXOW → SUBUTXO premises).

Remaining assumptions (module parameters):
- batch-utxo-accounting: consumedBatch ≡ producedBatch coin projection
  combined with mechanical UTxO tracking and deposit accounting
- applyDirectDeposits-rewardsBalance: gc-hom (∪⁺ distributes getCoin)
- utxow-pov-invalid: collateral collection preserves getCoin utxoSt
- ∪ˡ-res-lookup-preserve, sum-map-proj₂≡getCoin, setToList-Unique

The switch-suppression guard in evaluateBestPeerLocked compared
Tip.BlockNumber (the peer's claimed remote chain tip as advertised
in RollForward messages) rather than SelectionTip().BlockNumber
(the highest block header actually delivered to the chain selector).

These values can diverge: a peer announces Tip=N+1 in a RollForward
message at the same time it delivers the N+1 header. When two peers
are at the same chain position, peer A may announce Tip.BlockNumber=N+1
milliseconds before peer B, while both SelectionTips are still N. The
`>` precondition evaluates as `N+1 > N` (true), IsSignificantlyBetter
returns false for a 1-block lead, and the guard fires — keeping the old
incumbent. On the next cycle peer B catches up and the same logic fires
again in reverse, causing continuous oscillation near the chain tip.

Fix: use SelectionTip().BlockNumber for both the `>` precondition and
the IsSignificantlyBetter call. SelectionTip returns ObservedTip when
available (actual delivered headers), falling back to Tip otherwise.
This ensures the guard only suppresses switches based on headers that
have been concretely observed, not just claimed.

The density comparison case (same BlockNumber, different slots — fork
resolution) is unaffected: N > N is false, so the guard does not fire
and the density tiebreaker path proceeds normally.

Signed-off-by: wcatz <[email protected]>

fix(node-logs): support ISO 8601 Z timezone suffix in log timestamp

Signed-off-by: Allain Magyar <[email protected]>

Signed-off-by: Allain Magyar <[email protected]>