From ca0898b01559b22b8ec1d339ed2b167f4051f90d Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 31 Oct 2026 01:01:01 -0400 Subject: [PATCH] =?UTF-8?q?doc(circuit/frontier):=20quote=20the=20child=20?= =?UTF-8?q?edge=20bound=20of=20=C2=A7D.4.6=20in=20full?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The module docstring quoted "at most 6M / r < M / 8 edges", dropping "= 3M/32" from the manuscript's sentence without marking the cut. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- .../Circuit/Frontier/TensorNetwork/ChildSize.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/ChildSize.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/ChildSize.lean index 390e7d8943..5b5b429d66 100644 --- a/Complexity/Computability/Circuit/Frontier/TensorNetwork/ChildSize.lean +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/ChildSize.lean @@ -23,7 +23,8 @@ The child networks of a mode splitting (`TensorNetwork.ModeSplitting.child`, §D "a new packet vertex has at most `2L ⩽ Δ` ports"; * the child has one edge per port of its group (`ModeSplitting.card_edges_child`), so with at most `c M / r` ports per group on each side (Lemma D.3 (3)) it has at most `2 c M / r` edges - (`ModeSplitting.mul_card_edges_child_le`): the manuscript's "at most `6M / r < M / 8` edges". + (`ModeSplitting.mul_card_edges_child_le`): the manuscript's "at most `6M/r = 3M/32 < M/8` + edges" (§D.4.6, p. 63). ## Main results