Zero-circuit live clearing: conditional kappa = 5.14154245470094e-5 above #71

[alejandrozu]

New conditional kappa=257077122735047/5000000000000000000=5.14154245470094e-5, above the current PR71 witness 5.1414646104039e-5 and its stronger scoped limit. It also exceeds the numeric point of the subsequently withdrawn PR73 note, which is not a construction dependency.

This applies our PR70 profile-aware construction to PR71's anchored split/live-control graph at immutable source 1bef94fd40a746452548c84a4a8f8834670a3113. The new structural idea toggles zero-signal provider circuits to find a cheaper valid clearing relation for the same retired target. Pending live controls retain both containment guards and every actual XOR/promotion is paid. The graph/data geometry remain the PR71 construction.

The selected changed words pass fresh full input/target/arbitrary-dirty bases in both orientations, actual frame/event reconstruction and exact fixed-basis profiles/CRT; exact characteristic, all47 strict constraints and seven margins pass. The complete original71 profile has lower moment >1 at the new bit saving; our new upper is <1. A standalone37-declaration Lean4.31/Std audit passes:4 new universal toggle proofs,11 concrete Taylor8/tail/rounding/moment/frontier proofs and22 reused safety/rational-interface lemmas. No omitted proof, new project axiom or native decision shortcut.

The paper source, code, supplied words, exact certificate, source hashes and reproduction instructions are in research/current-record-circuits/. The broader matrix/parity and compiler toolkit remains in the preceding packages. Analytic logarithm/tail enclosures, all-size compiler/frame/tape/routing/recovery and eventual setup interfaces are inherited contracts. This is not a full formalization, global optimum or measured speedup; inherited full repository verification was pending at the71 draft announcement. No new compiled PDF is claimed.

Alejandro Zarzuelo Urdiales is the human author/developer, following earlier Archivara and personal matrix/parity work developed with multiple AI tools and substantial OpenAI Codex assistance. Credit Chafik Boukhalfa's71 composition, Dominik Scholz's live controls, Rohan Arun's profile-cost work, Rohan Garg's split operation, eumemic's compiler, Avi Eisenberg's interval/core-aware graph and all inherited contributors/notices. Zero-circuit and reversible linear-algebra principles retain prior-work status; the new contribution is their cost-aware integration and verified finite improvement.

[Mister-Meeseeks]

Thank you @alejandrozu. This contribution is now recorded on main in the scoped reconciliation review and contributor credits.

Contribution: Kernel-zero toggles with excluded target and live-frame bounds.

Review and limits: Fresh native full-word checks and CurrentRecordMath Lean build. No full analytic formalization claim.

The complete original source, proof/research notes, notices and relevant replay/CI evidence are retained through the pinned source archive. The review distinguishes fresh runs, exact-head historical CI and prior integration evidence. Closing this historical PR as reconciled; its obsolete headline does not replace the current selected bound, and draft/retracted claims retain their explicit qualifications.

Reviewed head: da9b6cbebb33e8b8293a604dde0eace9de53406b. Publication: b84ba67156a01f9c2cb34fe1e3cb1dcdeab00d9c.