Depth lower bound from genuine functional dependence
ProvedShiShallow.card_le_two_pow_depth_of_all_dependentLet be a quantum circuit of depth acting on input wires together with ancilla wires, built from gates of fan-in at most two and arranged in layers whose gates act on pairwise disjoint wires, and fix a designated output wire. For a classical input , let
be the acceptance probability of the circuit run on with all ancillas initialised to . Say that the input wire matters if the acceptance probability genuinely depends on it, that is, if there are inputs agreeing in every coordinate except with . If every input wire matters, then
This is the semantically honest form of the light-cone depth bound. The published syntactic version assumes instead that every input wire lies in the causal cone of the output; the cone only over-approximates the wires a value can depend on, so that hypothesis is weaker than genuine dependence and the bound above is correspondingly stronger. The restriction to layers of pairwise disjoint gates is essential rather than cosmetic: on three wires, the single layer consisting of and leaves wire holding , so all three input wires matter at depth , and .
Formalization Note. Layer well-formedness is the hypothesis LayerOk, and the acceptance probability is acceptProb, the total squared-modulus weight of the basis strings whose output wire reads ; inputs are padded with zero ancillas via inputState.
/- Copyright (c) 2026 Yueheng Shi. All rights reserved. Released under the Apache License, Version 2.0. Authors: Yueheng Shi Shallow quantum circuits and causal cones. MODIFICATIONS made for publication on Prove2me: the enclosing `namespace` is replaced by `section`+`open`; this statement is published OPEN (proof intentionally omitted). Built against Mathlib (Apache-2.0) at revision 0df444a360eaa60ab8c11dca51a86af692955474. -/ import Definitions.Def_ShiShallow_Circuit section open ShiShallow
theorem ShiShallow.card_le_two_pow_depth_of_all_dependent {n m : ℕ}
(c : Layered (n + m)) (out : Fin (n + m)) (hc : ∀ l ∈ c, LayerOk l)
(hdep : ∀ i : Fin n, ∃ x x' : Bits n,
(∀ j : Fin n, j ≠ i → x j = x' j) ∧ acceptProb c x out ≠ acceptProb c x' out) :
n ≤ 2 ^ depth c := by sorry
end
Confirmed by the mission captain (proposal self-audit).