Add partial _<ᵇ_ order on Buchholz terms (WF-0, partial) (#11)

First step of the Buchholz well-foundedness workstream. Introduces
the binary strict order `_<ᵇ_ : BT → BT → Set` together with the
auxiliary strict order `_<Ω_` on Ω-indices. Irreflexivity and
transitivity are both proved for the constructors that ship.

What lands:

OmegaMarkers.agda
  * `_<Ω_` with constructors `fin<fin` and `fin<ω` (no `ω <Ω _`
    case since ω is the top marker).
  * `<Ω-irrefl`, `<Ω-trans`, `<Ω→≤Ω`.
  * Named strict witnesses: `Omega0<Omega1`, `Omega0<Omegaω`,
    `Omega1<Omegaω`.

Ordinal/Buchholz/Order.agda (new)
  * `_<ᵇ_` as a 7-constructor inductive relation covering:
      - bzero vs every non-zero head (three cases)
      - bOmega μ <ᵇ bOmega ν via μ <Ω ν
      - bOmega μ <ᵇ bpsi ν α via μ <Ω ν
      - bpsi μ α <ᵇ bpsi ν β via μ <Ω ν
      - bplus x₁ x₂ <ᵇ bplus y₁ y₂ via x₁ <ᵇ y₁
  * `<ᵇ-irrefl` and `<ᵇ-trans` proved by case analysis.
  * Named strict-below-ψ witnesses: `bzero<Ω0`, `Ω0<Ω1`, `Ω1<Ωω`,
    `Ω0<ψ1-zero`.
  * Wired into All.agda; all above names pinned in Smoke.agda.

What is *explicitly deferred* (documented in-file):

  * bOmega vs bplus (either direction) — needs CNF-normal-form
    comparison between atomic heads and additive forms.
  * bpsi vs bplus (either direction) — same reason.
  * bpsi ν α <ᵇ bOmega μ with ν ≤Ω μ — the Buchholz-1986
    admissibility ordering; deferred.
  * Two same-binder sub-cases whose natural shape shares a binder
    on both sides of `_<ᵇ_` and runs into Agda 2.6.3's
    `--without-K` restriction on reflexive-equation elimination at
    irreflexivity-matching time:
      - bpsi ν α <ᵇ bpsi ν β with α <ᵇ β (same Ω-index).
      - bplus x y₂ <ᵇ bplus x z₂ with y₂ <ᵇ z₂ (same left summand).
    A rank-function embedding or a non-propositional Ω-equality
    is the next follow-up on this branch.

Totality of `_<ᵇ_` and well-foundedness (`Acc _<ᵇ_`) are the subject
of the follow-up WF-1 milestone once the deferred cases land.

Verified: `agda proofs/agda/All.agda` and `agda proofs/agda/Smoke.agda`
both exit 0 under --safe --without-K. No postulates introduced.

https://claude.ai/code/session_01JRLz84fAaWvRBKyXuc4tyK

Co-authored-by: Claude <noreply@anthropic.com>

Author: hyperpolymath