Keyboard shortcuts

Press or to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Mechanization

The wire shape, validation predicates, composition_signature, and four-axis versioning are mechanized in spec/lean/Argon/BuildArtifact/: Section.lean (section type + flags, @[language_interface]), Header.lean (preamble + version axes), Oxbin.lean (the Oxbin record + section invariants), ContentHash.lean (Merkle-of-sections), Validation.lean (Layer 1 + Layer 2 predicates), CompositionSignature.lean, and Versioning.lean (four-axis robustness). The Rust crate oxc-protocol::oxbin mirrors the @[language_interface]-tagged inductives; CI fails on drift.