d6g8k5htny-coder · Oct 23, 2026 · Oct 21, 2026 · Oct 22, 2026
diff --git a/docs/manuscript/side24_v3_supplement_draft_20261013/SHA256SUMS b/docs/manuscript/side24_v3_supplement_draft_20261013/SHA256SUMS
@@ -1,8 +1,8 @@
 e215b63c38db3bc453c97acc85fd120aea7597a1237220514b56234238f092bf  CONCORDANCE.md
 328143a6e10e5442fb7d308a103287e45156a7087ae631dac87a2d9e016db40e  SIDE24_V3_SUPPLEMENT_DRAFT_20261013.pdf
 7ac0f45b9e3a13045ba82ade996858ea3d4d965b03f3cc2304e35716c0c5232d  build.sh
-12e9feef7093f021aa1f412b7f3f1897195a03d7fc1970805ab405749553e304  checks/dep_graph_check.out.txt
-784a50dcb0ba57bb282e045fd9f7f008f44e74cace7b5d680e7fa8ce02ea061c  checks/dep_graph_check.py
+6cf9487d2fb909ddb2d83f7bf2f52d935ac9897f0c81f097a157de9e3b7130dc  checks/dep_graph_check.out.txt
+7078952690310e1f2dd4c368e3fe30f916734daaff94bc3affce3f0ff6877b51  checks/dep_graph_check.py
 12c21d6422c768b6c8ef513a6446347a4f29898743b10484931cc98e658e937e  checks/s10_s11_fold_check.out.txt
 ac8e11c44853309ffd5e37726e434d862795c5aa242b9450bd2958420cf30c42  checks/s10_s11_fold_check.py
 49958a1e41e4a738b4f1075ece1cf58dd8367cc301a49436b4285e38ab9d2535  checks/s12_derivations_check.out.txt
@@ -23,7 +23,7 @@ fbf89a522309e551d78c1cf0a9d448414a31707deaf75437e40c6f196ada4708  checks/s8_capK
 fa35cd0003d5e0f3da7caa8da4b2abd69efeae719162030f0981aab8a4bb5e73  checks/s8_capK_check.py
 45bd50a9c7990a1707accffb29df7091bb85d51df37f373ee3ec5ba93758717c  checks/s9_c2_d2_check.out.txt
 2acf388663fd049f912784454bfef629d3e314e677539ee71befe810d75ad486  checks/s9_c2_d2_check.py
-a1dd6e60381428d2fa5ebb676d7492f694d12d1efc8d2953d7a31f3239084a81  checks/test_dep_graph_check.py
+a4bd07174d9f2c498a26f09fa456a61795448f9ed1699d07d133120ab1a633e2  checks/test_dep_graph_check.py
 4b88aba1ccb35a8c24cdf524e88d52e52dccf8efa809308b9ec48401efb260f4  refs.bib
 9f3490c511e210b33bcd712b59d2d17501abe74dc4c69ef1945ddec303b72d63  supp_main.tex
 4ac5436d450d5857a147b42fd2a9a694b59d06ecbb0c147703a65beb48575c36  supp_refs_s12.bib

diff --git a/docs/manuscript/side24_v3_supplement_draft_20261013/checks/dep_graph_check.out.txt b/docs/manuscript/side24_v3_supplement_draft_20261013/checks/dep_graph_check.out.txt
@@ -54,7 +54,7 @@ nontrivial strongly connected components: 7 (7 explained in KNOWN, 0 not)
      explained: S5.30 (robustness) states margins for the inequalities of S5.26-S5.29 and is proved from them; the closing sentence of the proof of S5.26 points forward to S5.30 for the perturbed field, which is not used in S5.26.
      S5.26 (proof) -> S5.30 via lem:selection-robust: ...ves a fixed normalized margin, which persists under the exact $C^1$ perturbation of Lemma~\ref{lem:selection-robust}....
      S5.29 (proof) -> S5.26 via lem:selection-slope: ...of $S$, so it leaves $S$ tangent to $-v$, where $v$ is the positive eigenvector of Lemma~\ref{lem:selection-slope}. The proof of that lemma give...
-     S5.30 (statement) -> S5.26 via lem:selection-slope: ...\label{lem:selection-robust} Every strict inequality in Lemmas~\ref{lem:selection-slope}--\ref{lem:selection-capture}...
+     S5.30 (statement) -> S5.26 via lem:selection-slope: ...[exact-field robustness]\label{lem:selection-robust} Every strict inequality in Lemmas~\ref{lem:selection-slope}--\ref{lem:selection-capture}...
      S5.30 (statement) -> S5.29 via lem:selection-capture: ...\label{lem:selection-robust} Every strict inequality in Lemmas~\ref{lem:selection-slope}--\ref{lem:selection-capture} has a margin of at least $\fr...
   COMPONENT: Proposition S8.4 [prop:remainder-Z]; Theorem S8.6 [thm:remainder-vanish]; Theorem S8.9 [thm:remainder-rate]; Lemma S8.14 [lem:remainder-W]
      internal edges: 7

diff --git a/docs/manuscript/side24_v3_supplement_draft_20261013/checks/dep_graph_check.py b/docs/manuscript/side24_v3_supplement_draft_20261013/checks/dep_graph_check.py
@@ -3,7 +3,7 @@
 For every numbered statement (theorem, lemma, proposition, corollary) the script finds its proofs
 (the next ``proof`` environment; every ``\\begin{proof}[Proof of ...~\\ref{label}...]`` naming it, joint
 proofs included; and a ``\\subsection{Proof of ...~\\ref{label}}`` up to the next sectioning command), collects
-every ``\\ref``/``\\eqref`` in the statement and in its proof, maps equation labels to the statement
+every ``\\ref``/``\\eqref`` in the statement (including its optional title) and in its proof, maps equation labels to the statement
 that owns them (the statement or proof in which the display appears), and builds the directed graph
 "A's proof uses B". It then reports:
   1. strongly connected components of size > 1, each with its internal references in context, so that a
@@ -15,8 +15,8 @@
 
 The seven statement-level components of draft 13 are listed in KNOWN with the reason each is acyclic at
 the level of items, definitions and pointers; the script exits 1 only if a component outside that list
-appears, or if the internal edges of a listed component change (KNOWN_EDGES), so it is a regression check
-for later drafts, not a proof of anything. It exits 2, before building the graph, if the directory or any of
+appears, or if the directed internal edge set of a listed component changes (KNOWN_EDGES), so it is a regression check
+for later drafts, not a proof of anything. Unchanged edges do not certify an unchanged explanation or proof. It exits 2, before building the graph, if the directory or any of
 the thirteen section files is missing, or if a \\label is defined twice (a duplicate would overwrite a
 statement and could hide a component).
 
@@ -60,17 +60,61 @@
          'supp_s5_selection.tex', 'supp_s6_limit.tex', 'supp_s7_rate.tex', 'supp_s8_remainder.tex',
          'supp_s9_cusp.tex', 'supp_s10_third.tex', 'supp_s11_ctwo.tex', 'supp_s12_parent.tex', 'supp_s13_cap.tex']
 
-# Number of graph edges inside each KNOWN component when its explanation was written. A different count means
-# the explanation must be reviewed again, so the script then treats the component as unexplained.
+# Exact directed label-pair snapshots observed in the committed draft16 graph report:
+# commit 3d434b425a57e446fa78bb3e9340ab274f65e437, report blob e79fee95e0b3e531dc560e2cc5125648ebfa57fa.
+# These bind structural explanation reuse, not proof text or mathematical correctness.
+# Do not update a snapshot merely to make a changed component pass: review its explanation first.
 KNOWN_EDGES = {
-    frozenset(['prop:parent-KR', 'prop:parent-ledger']): 2,
-    frozenset(['lem:parent-generic', 'prop:parent-push', 'prop:parent-near', 'thm:parent-A', 'thm:parent-B', 'thm:parent-C']): 7,
-    frozenset(['lem:selection-slope', 'lem:selection-capture', 'lem:selection-robust']): 4,
-    frozenset(['lem:selection-collarchart', 'lem:selection-collarfactor', 'lem:selection-singchart', 'lem:selection-singfactor',
-               'lem:selection-finsing', 'lem:selection-fincol']): 12,
-    frozenset(['prop:coefficient-iso', 'cor:coefficient-BF']): 2,
-    frozenset(['prop:correction-firstvar', 'thm:correction-main']): 2,
-    frozenset(['lem:remainder-W', 'prop:remainder-Z', 'thm:remainder-vanish', 'thm:remainder-rate']): 7,
+    frozenset(['prop:parent-KR', 'prop:parent-ledger']): frozenset([
+        ('prop:parent-KR', 'prop:parent-ledger'),
+        ('prop:parent-ledger', 'prop:parent-KR'),
+    ]),
+    frozenset(['lem:parent-generic', 'prop:parent-near', 'prop:parent-push', 'thm:parent-A', 'thm:parent-B', 'thm:parent-C']): frozenset([
+        ('lem:parent-generic', 'thm:parent-C'),
+        ('prop:parent-near', 'prop:parent-push'),
+        ('prop:parent-push', 'thm:parent-B'),
+        ('thm:parent-A', 'lem:parent-generic'),
+        ('thm:parent-B', 'thm:parent-A'),
+        ('thm:parent-C', 'lem:parent-generic'),
+        ('thm:parent-C', 'prop:parent-near'),
+    ]),
+    frozenset(['lem:selection-capture', 'lem:selection-robust', 'lem:selection-slope']): frozenset([
+        ('lem:selection-capture', 'lem:selection-slope'),
+        ('lem:selection-robust', 'lem:selection-capture'),
+        ('lem:selection-robust', 'lem:selection-slope'),
+        ('lem:selection-slope', 'lem:selection-robust'),
+    ]),
+    frozenset(['lem:selection-collarchart', 'lem:selection-collarfactor', 'lem:selection-fincol', 'lem:selection-finsing', 'lem:selection-singchart', 'lem:selection-singfactor']): frozenset([
+        ('lem:selection-collarchart', 'lem:selection-fincol'),
+        ('lem:selection-collarfactor', 'lem:selection-collarchart'),
+        ('lem:selection-fincol', 'lem:selection-collarchart'),
+        ('lem:selection-fincol', 'lem:selection-collarfactor'),
+        ('lem:selection-fincol', 'lem:selection-finsing'),
+        ('lem:selection-finsing', 'lem:selection-singchart'),
+        ('lem:selection-finsing', 'lem:selection-singfactor'),
+        ('lem:selection-singchart', 'lem:selection-finsing'),
+        ('lem:selection-singchart', 'lem:selection-singfactor'),
+        ('lem:selection-singfactor', 'lem:selection-collarfactor'),
+        ('lem:selection-singfactor', 'lem:selection-finsing'),
+        ('lem:selection-singfactor', 'lem:selection-singchart'),
+    ]),
+    frozenset(['cor:coefficient-BF', 'prop:coefficient-iso']): frozenset([
+        ('cor:coefficient-BF', 'prop:coefficient-iso'),
+        ('prop:coefficient-iso', 'cor:coefficient-BF'),
+    ]),
+    frozenset(['prop:correction-firstvar', 'thm:correction-main']): frozenset([
+        ('prop:correction-firstvar', 'thm:correction-main'),
+        ('thm:correction-main', 'prop:correction-firstvar'),
+    ]),
+    frozenset(['lem:remainder-W', 'prop:remainder-Z', 'thm:remainder-rate', 'thm:remainder-vanish']): frozenset([
+        ('lem:remainder-W', 'thm:remainder-vanish'),
+        ('prop:remainder-Z', 'lem:remainder-W'),
+        ('prop:remainder-Z', 'thm:remainder-rate'),
+        ('prop:remainder-Z', 'thm:remainder-vanish'),
+        ('thm:remainder-rate', 'lem:remainder-W'),
+        ('thm:remainder-vanish', 'prop:remainder-Z'),
+        ('thm:remainder-vanish', 'thm:remainder-rate'),
+    ]),
 }
 
 
@@ -133,7 +177,7 @@ def main():
             label = lab.group(1) if lab else '%s@%s:%d' % (env, fn, m.start())
             counter += 1
             nums[label] = 'S%d.%d' % (sec_no, counter)
-            st = dict(label=label, env=env, file=fn, start=m.start(), end=m.end(), text=body)
+            st = dict(label=label, env=env, file=fn, start=m.start(), end=m.end(), text=(m.group(2) or '') + body)
             statements.append(st)
             stmt_by_label[label] = st
             for e in re.finditer(r'\\label\{([^}]*)\}', body):
@@ -260,15 +304,20 @@ def numkey(label):
     def internal(c):
         cs = set(c)
         return sum(1 for a in c for b in edges[a] if b in cs)
-    unknown = [c for c in bad if frozenset(c) not in KNOWN or (KNOWN_EDGES and KNOWN_EDGES.get(frozenset(c)) != internal(c))]
+    def internal_pairs(c):
+        cs = frozenset(c)
+        return frozenset((a, b) for a in c for b in edges[a] if b in cs)
+    # No truthiness escape: an absent snapshot must not authorize explanation reuse.
+    unknown = [c for c in bad if frozenset(c) not in KNOWN
+               or KNOWN_EDGES.get(frozenset(c)) != internal_pairs(c)]
     print('nontrivial strongly connected components: %d (%d explained in KNOWN, %d not)' % (len(bad), len(bad) - len(unknown), len(unknown)))
     for c in bad:
         print('  COMPONENT:', '; '.join(name(x) for x in c))
         print('     internal edges: %d' % internal(c))
         if frozenset(c) in KNOWN and c not in unknown:
             print('     explained:', KNOWN[frozenset(c)])
         elif frozenset(c) in KNOWN:
-            print('     CHANGED: internal edges differ from KNOWN_EDGES (%s); review the explanation' % KNOWN_EDGES.get(frozenset(c)))
+            print('     CHANGED: directed internal edges differ from or lack a KNOWN_EDGES snapshot; review the explanation')
         else:
             print('     NOT EXPLAINED: a new statement-level component')
         cs = set(c)

diff --git a/docs/manuscript/side24_v3_supplement_draft_20261013/checks/test_dep_graph_check.py b/docs/manuscript/side24_v3_supplement_draft_20261013/checks/test_dep_graph_check.py
@@ -2,7 +2,9 @@
 
 They encode the coverage findings DG-COV-01..04 of an OpenAI engineering probe (main#389 6325826874):
 a duplicate label must not hide a cycle; missing inputs must not pass; the DOT export must not depend on
-the hash seed; a change of the internal edges of a KNOWN component must fail.
+the hash seed; a change of the directed internal edge set of a KNOWN component must fail.
+Every helper invocation runs the real checker in both normal and optimized mode, with site loading
+suppressed. Outer unittest optimization and warning flags are not used as child-coverage evidence.
 
 Run from the supplement directory:  python3 -B -m unittest checks.test_dep_graph_check -v
 """
@@ -29,8 +31,17 @@ def lemma(label, refs=(), proof_refs=()):
 def run(d, *extra, seed='0'):
     env = {k: v for k, v in os.environ.items() if not k.startswith('PYTHON')}
     env['PYTHONHASHSEED'] = seed
-    r = subprocess.run([sys.executable, '-B', CHECKER, d] + list(extra), capture_output=True, text=True, env=env, timeout=60)
-    return r.returncode, r.stdout
+    results = []
+    for optimize in (False, True):
+        command = [sys.executable, '-B'] + (['-O'] if optimize else [])
+        command += ['-S', CHECKER, d] + list(extra)
+        r = subprocess.run(command, capture_output=True, text=True, env=env, timeout=60)
+        if r.stderr:
+            raise AssertionError('Unexpected checker stderr (%r): %s' % (command, r.stderr))
+        results.append((r.returncode, r.stdout))
+    if results[0] != results[1]:
+        raise AssertionError('Normal and optimized checker results differ: %r' % (results,))
+    return results[0]
 
 
 class DepGraphCheck(unittest.TestCase):
@@ -82,6 +93,26 @@ def test_dot_is_seed_independent(self):  # DG-COV-03
                 outs.append(f.read())
         self.assertEqual(len(set(outs)), 1)
 
+    def test_known_component_exact_edges_pass(self):  # DG-COV-04 control
+        # From the committed draft16 report, not from the implementation's snapshot table:
+        # S5.26 -> S5.30; S5.29 -> S5.26; S5.30 -> S5.26 and S5.29.
+        a, b, c = ('lem:selection-slope', 'lem:selection-capture', 'lem:selection-robust')
+        text = lemma(a, proof_refs=[c]) + lemma(b, proof_refs=[a]) + lemma(c, proof_refs=[a, b])
+        code, out = run(self.make(text))
+        self.assertEqual(code, 0, out)
+        self.assertIn('internal edges: 4', out)
+        self.assertIn('1 explained in KNOWN, 0 not', out)
+
+    def test_known_component_equal_count_rewire_fails(self):  # DG-COV-04 RED on count-only source
+        # Replace C->B by A->B. Same three labels, four edges and one strongly connected component.
+        a, b, c = ('lem:selection-slope', 'lem:selection-capture', 'lem:selection-robust')
+        text = lemma(a, proof_refs=[b, c]) + lemma(b, proof_refs=[a]) + lemma(c, proof_refs=[a])
+        code, out = run(self.make(text))
+        self.assertEqual(code, 1, out)
+        self.assertIn('CHANGED', out)
+        self.assertIn('internal edges: 4', out)
+        self.assertIn('0 explained in KNOWN, 1 not', out)
+
     def test_known_component_with_changed_edges_fails(self):  # DG-COV-04
         # A KNOWN three-member component with all six internal edges (KNOWN_EDGES records four).
         labs = ['lem:selection-slope', 'lem:selection-capture', 'lem:selection-robust']
@@ -91,5 +122,62 @@ def test_known_component_with_changed_edges_fails(self):  # DG-COV-04
         self.assertIn('CHANGED', out)
 
 
+    def test_statement_body_references_remain_edges(self):
+        text = lemma('lem:a', refs=['lem:b']) + lemma('lem:b', refs=['lem:a'])
+        code, out = run(self.make(text))
+        self.assertEqual(code, 1, out)
+        self.assertIn('proofs: 2; edges: 2', out)
+        self.assertIn('UNEXPLAINED_COMPONENT_FOUND', out)
+
+    def test_statement_title_references_cannot_hide_a_cycle(self):
+        # Statement-title text is a reference source, not a proof-validity judgment.
+        for kind in ('theorem', 'lemma', 'proposition', 'corollary'):
+            for command in ('ref', 'eqref'):
+                with self.subTest(kind=kind, command=command):
+                    title = r'From \%s{lem:b}' % command
+                    a = (r'\begin{%s}[%s]\label{lem:a}Statement.\end{%s}'
+                         r'\begin{proof}Argument.\end{proof}' % (kind, title, kind))
+                    code, out = run(self.make(a + lemma('lem:b', proof_refs=['lem:a'])))
+                    self.assertEqual(code, 1, out)
+                    self.assertIn('edges: 2', out)
+                    self.assertIn('UNEXPLAINED_COMPONENT_FOUND', out)
+                    self.assertIn('(statement) -> S1.2 via lem:b:', out)
+
+    def test_statement_title_equation_reference_uses_its_proof_owner(self):
+        a = (r'\begin{lemma}[From \eqref{eq:b}]\label{lem:a}Statement.\end{lemma}'
+             r'\begin{proof}Argument.\end{proof}')
+        b = (r'\begin{lemma}\label{lem:b}Statement.\end{lemma}'
+             r'\begin{proof}\begin{equation}\label{eq:b}1=1\end{equation}'
+             r'Uses \ref{lem:a}.\end{proof}')
+        code, out = run(self.make(a + b))
+        self.assertEqual(code, 1, out)
+        self.assertIn('edges: 2', out)
+        self.assertIn('(statement) -> S1.2 via eq:b:', out)
+
+    def test_acyclic_title_references_are_edges_not_automatic_failure(self):
+        title = r'From \ref{lem:b}; again \ref{lem:b}; self \ref{lem:a}; external \ref{outside}'
+        a = (r'\begin{lemma}[%s]\label{lem:a}Statement.\end{lemma}'
+             r'\begin{proof}Argument.\end{proof}' % title)
+        d = self.make(a + lemma('lem:b'))
+        dot = os.path.join(d, 'title.dot')
+        code, out = run(d, '--dot', dot)
+        self.assertEqual(code, 0, out)
+        self.assertIn('proofs: 2; edges: 1', out)
+        with open(dot, encoding='utf-8') as f:
+            edges = [line.strip() for line in f if ' -> ' in line]
+        self.assertEqual(edges, ['"S1.1" -> "S1.2";'])
+
+    def test_plain_and_commented_titles_preserve_acyclic_behavior(self):
+        for title in ('A descriptive title', 'A title % ignored '+r'\ref{lem:b}'+'\ncontinued'):
+            with self.subTest(title=title):
+                a = (r'\begin{lemma}[%s]\label{lem:a}Statement.\end{lemma}'
+                     r'\begin{proof}Argument.\end{proof}' % title)
+                code, out = run(self.make(a + lemma('lem:b', proof_refs=['lem:a'])))
+                self.assertEqual(code, 0, out)
+                self.assertIn('proofs: 2; edges: 1', out)
+                self.assertIn('NO_UNEXPLAINED_COMPONENT', out)
+
+
+
 if __name__ == '__main__':
     unittest.main()