A demotion-only composition of a source-admissibility gate and a claim-provenance binder (Totus Canon)

Two deployed deterministic verification organs are composed: a sealed gate that rules a source record admissible, held, or refused against a content-hashed schema before any language model speaks, and a register binder whose machine-checked non-amplification theorem binds every model claim at the weakest register among its sources. The paper reports the design rules the composition forced (a demotion-only interface: the gate can withdraw a source's standing, nothing can grant it; verdict quarantine; epoch boundaries), the formal object underneath it (the composed ruling as the pair of recovery and source standing under a demotion-only constraint), and the exact open proposition the composition now owes a machine check: whether non-amplification remains invariant under composition provided source identity is conserved across the interface. The relocation of the difficulty from the ordering arithmetic to source-identity conservation is the contribution. A worked live transcript against a local 35B model, with both organs' content-addressed bundle hashes, and the complete interface specification are deposited alongside the paper. The composition runs live at fellowship.narrativelogic.co.uk. Every verdict concerns demonstrated provenance, never truth; the machine-checked theorem belongs to the binder alone and the composed property is explicitly conjecture pending mechanisation. Version 1.1 (same day) adds the mechanisation: the open proposition was model-checked with TLC over an identity-extended TLA+ model; eight seeded fault transitions each produced a counterexample against exactly the invariant built to catch it, five reachability probes confirmed non-vacuity, and the conforming specification passed exhaustive bounded search (93,316,238 and 149,677,549 generated states in the one-epoch and two-epoch configurations) with no violation of seventeen invariants. The checked register theorem is narrowed to cited demonstration, as the addendum discloses, and the model checks the interface contract plus the proposed identity discipline, not the deployed implementation. Module, probes, configurations, logs, pre-build contract and mechanisation README are deposited.