Coverage

Comment and keyword shading is a reading aid only. It is not a verification marker; the evidence is the build record on the Build page.

1import Foundation2import SharedCircuit3import LocalRestore4import ParityCircuit56/- Phase 4: composition of the phase-4 interfaces (coverage glue).  Written by Claude7   (10 October 2026).  Lean 4.26.0, core/Std only.89   The negative (single-frame) results now accept the classical input in any of three10   forms, each PROVED here to imply the formula premise of phase 3: the formula premise11   itself, the shared-circuit premise (`Shared.DagParityPremise`), or the restriction /12   switching bound (`Foundation.SwitchingBound`, the exact remaining classical content).13   All three remain explicit, unproved hypotheses. -/1415namespace NimAudit16namespace Coverage1718open Prob AC0 AC0.Circ Bridge CorrBridge Game1920/-- Single-frame barrier from the switching bound (no formula premise assumed). -/21theorem no_strong_master_of_switching {S : BinReadout.BCirc} {m r d s : Nat} {p ε : Rat}22    (hb : BinReadout.BBound S (m + 1) 2 r d s) (hm : 1 ≤ m) (hε : ε < 1 / 2)23    (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (h : Foundation.SwitchingBound d s m p ε) :24    ¬ ParityCircuit.StrongMastery S (m + 1) :=25  ParityCircuit.no_strong_master_of_premise hb hm hε (Foundation.premise_of_switching hp0 hp1 h)2627/-- Single-frame barrier from the shared-circuit form of the classical theorem. -/28theorem no_strong_master_of_dag {S : BinReadout.BCirc} {m r d s : Nat} {ε : Rat}29    (hb : BinReadout.BBound S (m + 1) 2 r d s) (hm : 1 ≤ m) (hε : ε < 1 / 2)30    (h : Shared.DagParityPremise d s m ε) : ¬ ParityCircuit.StrongMastery S (m + 1) :=31  ParityCircuit.no_strong_master_of_premise hb hm hε (Shared.formula_premise_of_dag h)3233/-- Network readout bound from the switching bound. -/34theorem network_readout_bound_switching {W M B N j r L : Nat} (hj : j < B) (nets : Bool → List Layer)35    (hlen : ∀ b, (nets b).length = L) (hv : ∀ b, NetValid W (nets b))36    (hb : ∀ b, NetBounded M (nets b)) (hr : N + 1 ≤ 2 ^ r) {p ε : Rat} (hp0 : 0 ≤ p) (hp1 : p ≤ 1)37    (hsw : ∀ m, N + 1 ≤ m → m ≤ B * (N + 1) →38      Foundation.SwitchingBound (3 * L + 2 + 11)39        (12 * Upar (N + 1) B ((r + 1) * (2 * ((2 * W + 3) ^ L * (M + 1) ^ (W * L)) + 1)) ^ 10) m p ε) :40    succCountRO B (N + 1) (BinReadout.binReadoutOf B (N + 1)41        (fun b => BinReadout.netBCirc W B (N + 1) r (nets b))) j /42        nonzeroCount B (N + 1) ≤43      2 / (((2 ^ B : Nat) : Rat) - 1) + (((2 ^ B : Nat) : Rat) - 1) * ε :=44  BinReadout.network_readout_bound hj nets hlen hv hb hr45    (fun m h1 h2 => Foundation.premise_of_switching hp0 hp1 (hsw m h1 h2))4647/-- Positive two-frame result, end to end: from a zero position Q and any legal48    opponent move Q → Q', the purely local circuit (no global nim-sum) selects a legal49    reply restoring nim-sum 0, identical to `NimGame.restore`. -/50theorem two_frame_restoration {B N : Nat} {Q Q' : List Nat} (hQ : Q.length = N) (hQ' : Q'.length = N)51    (hw : Width B Q) (hw' : Width B Q') (h0 : nimSum Q = 0) (hm : Game.Move Q Q') :52    ∃ i v, SelectCircuit.selReadout (LocalRestore.restC B N) (LocalRestore.tf B N Q Q') = some (i, v) ∧53      Game.Move Q' (Q'.set i v) ∧ nimSum (Q'.set i v) = 0 ∧54      SelectCircuit.SelBound (LocalRestore.restC B N) N B (4 + 9 + 4)55        (12 * ((N + 2) * (B + 2) * (B * (2 * B + 3) + 9 + 2)) ^ 8 * (10 * N + 1 + 1)) (2 * (B * N)) := by56  obtain ⟨i, v, h1, _, h3, h4⟩ := LocalRestore.restore_equiv hQ hQ' hw hw' h0 hm57  exact ⟨i, v, h1, h3, h4, LocalRestore.restC_bound⟩5859/-- Positive multi-head result, end to end: the circuit reading the board and the B60    rollout outcomes outputs the verified decision move, with explicit resources. -/61theorem multi_head_selection {B N : Nat} {P : List Nat} (hP : P.length = N) (hw : Width B P) :62    SelectCircuit.selReadout (SelectCircuit.mhSel B N) (SelectCircuit.obsIn B N P (Game.outcomes P)) =63      Controller.decisionMove P ∧64    SelectCircuit.SelBound (SelectCircuit.mhSel B N) N B (4 + 9 + 3)65      (12 * ((N + 2) * (B + 2) * (B * (2 * B + 3) + 9 + 2)) ^ 8 * (9 + 1)) (B * N + B) :=66  ⟨SelectCircuit.mhSel_outcomes hP hw, SelectCircuit.mhSel_bound⟩676869/-! ## Axiom audit -/7071#print axioms no_strong_master_of_switching72#print axioms no_strong_master_of_dag73#print axioms network_readout_bound_switching74#print axioms two_frame_restoration75#print axioms multi_head_selection76end Coverage77end NimAudit