From fffaa0c8ef7e305c3cf2cd8eba251d99435637a2 Mon Sep 17 00:00:00 2001 From: Dylan Roy <249851642+d6g8k5htny-coder@users.noreply.github.com> Date: Wed, 21 Oct 2026 18:44:58 -0500 Subject: [PATCH 1/2] checks: publish reviewed SIDE24 dependency-graph guard proposal Publish the exact OpenAI-authored edge-identity and statement-title deltas reviewed by xAI Grok 4.7 in main#389 comments 6327779834 and 6328304829. Actual publisher: OpenAI / GPT-6 Astra Pro, RESUME-LINK-SEMANTICS. Canonical publication pickup: main#389 comment 6328967488. Source-only isolated proposal on supplement draft16. No adoption on the manuscript author's branch. SHA256SUMS and retained report remain frozen and must be reconciled before adoption; this is not a merge-ready package. No mathematical or scientific-status change. --- .../checks/dep_graph_check.py | 81 ++++++++++++---- .../checks/test_dep_graph_check.py | 94 ++++++++++++++++++- 2 files changed, 156 insertions(+), 19 deletions(-) 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 index 38a6f722a..09446f4d1 100644 --- 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,7 +304,12 @@ 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)) @@ -268,7 +317,7 @@ def 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 index 3d9252515..98e30365d 100644 --- 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() From ac5e6552fbb4f3fa9333da39f5f0ab59b6f37890 Mon Sep 17 00:00:00 2001 From: Dylan Roy <249851642+d6g8k5htny-coder@users.noreply.github.com> Date: Thu, 22 Oct 2026 11:15:22 -0500 Subject: [PATCH 2/2] checks: reconcile SIDE24 dependency report and source checksums Update only the generated dependency report's documented S5.30 title context and the checker/test/report checksum entries. The two reviewed Python files and all manuscript/TeX/PDF/status bytes remain unchanged. Actual publisher: OpenAI / GPT-6 Astra Pro, RESUME-LINK-SEMANTICS. Canonical stage: main#486 comment6345222484. Manuscript replay and 46-entry package checksum evidence: xAI Grok4.7, Cursor run bc-9d5981fd, main#389 comment6345370814. Fresh build aux provenance is recorded there. OpenAI independently reconstructed and matched both record blobs and the exact allowed delta. This updates only the isolated proposal branch. No author-branch adoption, merge authorization, mathematical acceptance or scientific-status change. --- .../side24_v3_supplement_draft_20261013/SHA256SUMS | 6 +++--- .../checks/dep_graph_check.out.txt | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/docs/manuscript/side24_v3_supplement_draft_20261013/SHA256SUMS b/docs/manuscript/side24_v3_supplement_draft_20261013/SHA256SUMS index fbcfe5684..54d2c03cb 100644 --- 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 index e79fee95e..07f1ec153 100644 --- 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