feat(ceremony): P0 authority + enforcement-boundary kernel in Rust (Charon/Aeneas refinement target)

[hartsock]

The pure Rust waist begins

First Rust of the narrow waist (roadmap Phase 1, "prove the waist"). New crate agent-bridle-ceremony mirroring formal/Ceremony/P0/Authority.lean:

Authority = Effect × Assurance × Scope   (product meet-lattice, ADR 0020)

• per-axis finite chains with rank()/meet() (GLB = lower rank)
• Authority::meet (componentwise), le, attenuate, BOTTOM (⊥), TOP (⊤)
• Resolution { NeedsDecision | Decided(Authority) }
• resolve(&[Authority]): empty ⇒ NeedsDecision (not ⊤ — the OB-9/OB-12 no-fail-open clause), else the fold-meet of matches (L1)

Why it looks the way it does

Dependency-free, total, panic-free, #![forbid(unsafe_code)] — chosen for Charon/Aeneas extractability (Phase 1c). The Lean file states the laws as theorems; this crate is what a future Aeneas proof will show refines them, once the opam leg lands (docs/TOOLCHAIN.md). No wire format here — serde/records/signatures are P1 and stay HELD until the Phase-1d conformance vectors; publish = false until the waist is proven.

Verification (until Aeneas is wired)

The same laws are discharged by exhaustive enumeration over the 18-point finite domain — the Rust analogue of the Lean proofs' by cases <;> decide. 12 tests + doctest, all green:

• axis + product meet comm/assoc/idem (mirror *.meet_comm/assoc/idem)
• meet_never_amplifies + attenuate bounded by input and ceiling (meet_le_* / PO-4)
• sequential ceilings collapse to one meet (attenuate_compose)
• ⊥ absorbs / ⊤ is identity
• resolve empty ⇒ NeedsDecision, never Decided(⊤) (no fail-open)
• resolve order-independent + = meet of all matches (resolve_swap / L1)

Test plan

• cargo test -p agent-bridle-ceremony → 12 + 1 doctest pass.
• cargo clippy -p agent-bridle-ceremony --all-targets --all-features and --no-default-features → zero warnings.
• Full pre-push gate (workspace matrix + coverage + formal) passed on push.

Risk

Low — a new, isolated, publish = false crate with no dependencies and no consumers yet; touches only the workspace member list. Adds no wire format (nothing frozen).

Next (Phase 1c): stand up the opam/OCaml leg so Aeneas can prove this refines Authority.lean — upgrading "exhaustively tested mirror" to "proven refinement."

[hartsock]

Grew this into the complete P0 Rust kernel: added boundary.rs, the Rust mirror of formal/Ceremony/P0/Boundary.lean (the OCAP two-stream sequencing result). It carries the L3-gated brush default as an Effect::meet in the same algebra — Fence/Request, safe_subset/brush_honest/boundary_verdict, minted_grant — with 7 exhaustive tests mirroring the Lean theorems (fallback_is_forced, attenuation-not-a-new-op, minted ≤ request/enforceable, advisory+dynamic ⇒ Deny, and the proj_effect_meet convergence check). Now 19 tests + doctest, fmt/clippy clean. So this PR = both P0 Lean files (Authority.lean + Boundary.lean) mirrored in one dependency-free, Charon-extractable crate.