formal: prove P1 signed-object contracts

[hartsock]

What this PR does

• Implements the first profile in the formal: prove ceremony algebra and protocol safety kernel #232 formal stack: P1 signed-object contracts from docs(spec): the Ceremony Contract v0.1 draft — five laws, wire objects, chained store #229.
• Models exact signed-envelope decoding: a successful decode recomposes to the received bytes, canonical transport and unsigned encoders are injective, and the universal signature preimage binds profile/version, algorithms, codec, record type, store ID, thread/principal, body, CID, signer, and critical fields.
• Makes cryptographic assumptions explicit and semantic: the claimed CID must equal a collision-binding digest of the body; signature verification carries origin, cross-algorithm/preimage binding, and deterministic-signature evidence.
• Keeps VerifiedEnvelope and Sealed constructors private, requires TrustedProfile for verification and hash dispatch, and proves v1 dispatch cannot reach SHA-1.
• Adds fully mocked mutation tests plus a whole-project Lean gate that rejects proof escapes and modules omitted from the root import graph.
• Runs the P1 proof build on Ubuntu and native Windows.

Authored by OpenAI GPT-5 in the Codex desktop harness on Windows.

Test plan

• just check-formal - passed; 8 Lake jobs plus the all-source proof/import gate.
• Adversarial gate probes - passed: root, nested, and extra Lake-root proof escapes fail; unimported modules fail.
• Private-constructor probe - passed: downstream code cannot name VerifiedEnvelope.verified or Sealed.sealed.
• Mocked P1 mutations - passed: body, CID, record type, store ID, thread/principal, signer, codec interpretation, signature, version, hash, signature algorithm, payload codec, and unknown critical fields all reject.
• cargo fmt --all -- --check - passed.
• actionlint .github/workflows/formal.yml - passed with actionlint 1.7.12.
• just check-windows - passed: 94 core tests, shell engines, launcher, and AppContainer filesystem/exec/network kernel proofs.
• just publish-check - passed.
• just check - blocked by unchanged parent no-default Clippy warnings: unused Tool import and ctx helper in agent-bridle-tool-shell/tests/unbridle.rs. Normal push reproduced this before the author's previously approved --no-verify fallback was used.

All P1 tests are deterministic and fully mocked; no live service is used.

Out of scope

• Concrete DAG-CBOR/JSON/TOML envelope adapters and conformance vectors.
• Proofs of BLAKE3 collision resistance or Ed25519 unforgeability; these remain named Tier-1 assumptions.
• P2 anti-rollback state, P0 authority algebra, P3 protocol analysis, and Rust/Aeneas refinement.
• Fixing the parent branch's unrelated no-default Clippy warnings.

Stacked on #232; derives from #229 at 9e7a245.

[hartsock]

Integrated into #238 (Phase-1 formal foundation): your P1 signed-object Lean contracts (SignedObject.lean, Gate.lean, the counterexample/contract tests, the Lake project + formalGate + formal.yml CI) are harvested as-is and now build alongside the P0 authority algebra (Ceremony/P0/Authority.lean) in one Lake project — lake build 9 jobs, 0 sorry, green. Thank you — this was the right P1 formalization, consistent with the v0.3.1 freeze (OB-13 signature preimage). This PR (#233) can close as integrated once #238 lands. The non-formal glue (TOOLCHAIN/justfile/pre-push) was re-derived against current main to avoid the stale-base conflicts.