diff --git a/.github/workflows/d1-chain-reconciliation.yml b/.github/workflows/d1-chain-reconciliation.yml new file mode 100644 index 000000000..167cf9206 --- /dev/null +++ b/.github/workflows/d1-chain-reconciliation.yml @@ -0,0 +1,65 @@ +name: D1 chain reconciliation checks + +'on': + pull_request: + paths: + - 'reviews/d1_chain_reconciliation_20260928/**' + - '.github/workflows/d1-chain-reconciliation.yml' + - 'imports/lifetime_parent_20260925/**' + - 'reviews/d1_section9_borel_repair_20260925/**' + - 'reviews/d1_theorem_a_nonauthor_20260928/**' + - 'frontiers/downstream_gate_20260925/GRAPH.json' + workflow_dispatch: + +permissions: + contents: read + +jobs: + exact-and-probe: + runs-on: ubuntu-latest + timeout-minutes: 10 + steps: + - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 + with: + persist-credentials: false + - uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 + with: + python-version: '3.11.16' + - name: Verify sources, replay both modes, reject mutants + env: + PYTHONDONTWRITEBYTECODE: '1' + run: | + set -euo pipefail + python -B -S - <<'PY' + import hashlib, json, pathlib, subprocess, sys + root = pathlib.Path('reviews/d1_chain_reconciliation_20260928').resolve() + manifest = json.loads((root / 'SOURCE_FILES.json').read_text())['files'] + present = sorted(p.name for p in root.iterdir()) + expected_names = sorted([e['path'] for e in manifest] + ['SOURCE_FILES.json']) + if present != expected_names: + raise ValueError('packet tree differs from manifest: ' + repr(present)) + for entry in manifest: + path = root / entry['path'] + if pathlib.PurePosixPath(entry['path']).name != entry['path'] or path.is_symlink(): + raise ValueError('flat regular source required: ' + entry['path']) + data = path.read_bytes() + if len(data) != entry['bytes'] or hashlib.sha256(data).hexdigest() != entry['sha256']: + raise ValueError('source identity mismatch: ' + entry['path']) + script = str(root / 'reconciliation_check.py') + expected = (root / 'RESULTS.json').read_bytes() + mutants = ['allow-author-review', 'skip-coverage', 'displayed-congruence', 'drop-mixed-square', + 'drop-far-branch', 'embedding-radius', 'difference-exponent', 'gamma-24', + 'unbind-component'] + for flags in (['-B', '-S'], ['-B', '-O', '-S']): + out = subprocess.run([sys.executable, *flags, script], + check=True, capture_output=True, timeout=300).stdout + if out != expected: + raise RuntimeError('output differs from RESULTS.json under ' + ' '.join(flags)) + for m in mutants: + rc = subprocess.run([sys.executable, *flags, script, '--mutant', m], + capture_output=True, timeout=300).returncode + if rc != 1: + raise RuntimeError('mutant ' + m + ' not rejected') + print(json.dumps({'check': 'd1-chain-reconciliation', 'custody_graph_ledger_math': 'PASS', 'analytic_acceptance_by_this_check': False})) + PY + git diff --exit-code diff --git a/.github/workflows/downstream-gate.yml b/.github/workflows/downstream-gate.yml index 70699422f..8e86eee86 100644 --- a/.github/workflows/downstream-gate.yml +++ b/.github/workflows/downstream-gate.yml @@ -56,7 +56,7 @@ jobs: raise RuntimeError('actual Python 3.11 required') verify() out = pathlib.Path(os.environ['RUNNER_TEMP']) / 'downstream-gate-results' - subprocess.run([sys.executable, '-B', '-S', str(root / 'run_validation.py'), '--output', str(out)], check=True, timeout=240) + subprocess.run([sys.executable, '-B', '-S', str(root / 'run_validation.py'), '--output', str(out)], check=True, timeout=480) subprocess.run([ sys.executable, '-B', '-S', str(root / 'git_transition_audit.py'), '--repo', str(pathlib.Path.cwd()), '--base', os.environ['BASE_SHA'], @@ -81,13 +81,13 @@ jobs: raise RuntimeError('regression failed: ' + folder) verify() report = json.loads((out / 'REPORT.json').read_text()) - if not report['passed'] or report['distinct_tests'] != 67 or report['distinct_semantic_mutations'] != 24: + if not report['passed'] or report['distinct_tests'] != 71 or report['distinct_semantic_mutations'] != 24: raise RuntimeError('unexpected new-test scope') (out / 'GITHUB_CONTEXT.json').write_text(json.dumps({ 'run': os.environ['GITHUB_RUN_ID'], 'tested_commit': os.environ['GITHUB_SHA'], 'base_commit': os.environ['BASE_SHA'], 'event': os.environ['GITHUB_EVENT_NAME'], - 'python': sys.version, 'gate_distinct_tests': 67, - 'regression_distinct_tests': 177, 'total_distinct_tests': 244, + 'python': sys.version, 'gate_distinct_tests': 71, + 'regression_distinct_tests': 177, 'total_distinct_tests': 248, 'semantic_mutations': 24, 'source_files_verified': len(pins), 'lemma_closed': False, 'scientific_effect': 'NONE', 'meaning': 'same-author software verification; no independent theorem acceptance', diff --git a/PROOF_INDEX.md b/PROOF_INDEX.md index d66770afd..dc7cea156 100644 --- a/PROOF_INDEX.md +++ b/PROOF_INDEX.md @@ -15,7 +15,8 @@ The shared [public inventory](https://github.com/d6g8k5htny-coder/main/tree/main ## Reviewed scoped results -- D2 lifetime remainder: proof [frontiers/three_fronts_20260924/LIFETIME_REMAINDER.md](frontiers/three_fronts_20260924/LIFETIME_REMAINDER.md); [R1–R4 review](https://github.com/d6g8k5htny-coder/main/issues/67#issuecomment-5841270276) and [R5/R6 delta review](https://github.com/d6g8k5htny-coder/main/issues/67#issuecomment-5841782206) record ACCEPT for Theorem R at its stated existential `O(1)`-remainder scope. The delta identifies its exact parent imports and does not consume the still-open Theorem A cubic selection bound. Numerical constants/radii, a second coefficient, and RN/24-jet closure are outside this verdict. [main #67](https://github.com/d6g8k5htny-coder/main/issues/67) remains open for other bundled fronts. +- D2 lifetime remainder: proof [frontiers/three_fronts_20260924/LIFETIME_REMAINDER.md](frontiers/three_fronts_20260924/LIFETIME_REMAINDER.md); [R1–R4 review](https://github.com/d6g8k5htny-coder/main/issues/67#issuecomment-5841270276) and [R5/R6 delta review](https://github.com/d6g8k5htny-coder/main/issues/67#issuecomment-5841782206) record ACCEPT for Theorem R at its stated existential `O(1)`-remainder scope. The delta identifies its exact parent imports (the D1-A–E interfaces) and does not consume Theorem A's cubic bound (1.1); those imports are now reconciled in [reviews/d1_chain_reconciliation_20260928/](reviews/d1_chain_reconciliation_20260928/RECONCILIATION.md). Numerical constants/radii, a second coefficient, and RN/24-jet closure are outside this verdict. [main #67](https://github.com/d6g8k5htny-coder/main/issues/67) remains open for other bundled fronts. +- D1 parent lifetime theorem (Theorems A, B, C): proof [imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md](imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md) read with the [congruence erratum](imports/lifetime_parent_20260925/ERRATUM_CONGRUENCE.md), the [Section 9 replacement v1.1](reviews/d1_section9_borel_repair_20260925/REPAIR.md), wording W1 and the embedding radius `r < L/(4√2)`; deterministic support [imports/lifetime_parent_20260925/MARKED_CYLINDER_CAP_PROOF.md](imports/lifetime_parent_20260925/MARKED_CYLINDER_CAP_PROOF.md). [Reconciliation](reviews/d1_chain_reconciliation_20260928/RECONCILIATION.md) binds the [D1-A–E review](https://github.com/d6g8k5htny-coder/main/issues/63#issuecomment-5841570965) (xAI/Grok, Sections 8–15), the [A1–A7, cap and Section 9 review](reviews/d1_theorem_a_nonauthor_20260928/REVIEW.md) (Anthropic/Claude), the [Section 9 Grok/Lucas record](reviews/d1_section9_borel_grok_lucas_20260928/REVIEW.md), and its own review of the previously unreviewed Sections 11–12, and records ACCEPT for Theorems A, B and C at existential scope: fixed `d>=2` and `L`, compact births and positive gap marks for A and B (with `B` and `K` of positive length for B's positive constant), all frames, leading term only for C. No numerical `C`, `r_*`, `z_*` or coefficient; no lower bound for `d>=3` (the planar lower bound is [ELDER_LOWER_AND_DENSITY_GAP.md](frontiers/window_multiplicity_laws_20260928/ELDER_LOWER_AND_DENSITY_GAP.md) (E2)); no unrestricted difference rate; no RN/24-jet certificate. The immutable parent bytes are unchanged. - D3 SIDE24 coefficient: proof [coefficients/side24_v1/PROOF.md](coefficients/side24_v1/PROOF.md); [C1–C6 review](https://github.com/d6g8k5htny-coder/main/issues/65#issuecomment-5841269490) verifies the coefficient calculation; [reconciliation](https://github.com/d6g8k5htny-coder/main/issues/65#issuecomment-5841779222) closes the coefficient-review work package. Interpretation as the parent lifetime law retains the parent's separate dependency and review boundaries. - D4 fixed-remote RN theorem: proof [frontiers/remote_window_20260924/PROOF.md](frontiers/remote_window_20260924/PROOF.md); [source-bound review](https://github.com/d6g8k5htny-coder/main/issues/76#issuecomment-5841783172) and [scoped reconciliation](https://github.com/d6g8k5htny-coder/main/issues/76#issuecomment-5841861362) record ACCEPT on the seven fixed-rho/fixed-eta interfaces. Shrinking spatial cutoffs, pin/intermediate regions, and shrinking witness separation are outside that review. - D5 all-height fixed annulus: proof [frontiers/rn_annulus_bridge_20260925/PROOF.md](frontiers/rn_annulus_bridge_20260925/PROOF.md); review [reviews/pr28_annulus_bridge_nonauthor_20260925/REVIEW.md](reviews/pr28_annulus_bridge_nonauthor_20260925/REVIEW.md) records R1–R7 ACCEPT at fixed `d=2`, fixed `L`, compact positive-gap marks, and fixed annulus `1=2 and L; compact births and positive gap marks for Theorems A and B, with B and K of positive length for Theorem B (singleton intervals give zero mark-window intensity); embedding radius r < L/(4 sqrt 2); all frames; Theorem C leading term only; no numerical C, r_*, z_* or coefficient; no d>=3 lower bound; no RN/24-jet", + "reading_rule": [ + "math.d1-component.congruence-erratum", + "math.d1-component.section9-replacement-v1_1", + "math.d1-component.marked-cylinder-cap", + "math.d1-component.reconciliation-record" + ] + }, + "math.d1-component.congruence-erratum": { + "layer": "D1", + "kind": "reading_rule_component", + "classification": "PROVED_REVIEWED", + "controlling": false, + "component_of": "math.uniform-matrix-cap-lifetime", + "component_role": "amendment", + "author_provider": "OpenAI", + "fingerprint": "bad7ef609c4ad8c41ad6af562c1b6807921e19a9d556ed793ad1a0db6e202028", + "source": "imports/lifetime_parent_20260925/ERRATUM_CONGRUENCE.md", + "ledger_items": [ + "A3-E1" + ], + "review_basis": [ + { + "review": "C1", + "provider": "Anthropic", + "verdict": "ACCEPT", + "depth": "full" + }, + { + "review": "G3", + "provider": "xAI", + "verdict": "ACCEPT", + "depth": "full" + } + ], + "review_source": "reviews/d1_chain_reconciliation_20260928/LEDGER.json", + "scope": "congruence factor D_r = diag(r^-1/2, I) in parent section 5; replaces the displayed factor" + }, + "math.d1-component.section9-replacement-v1_1": { + "layer": "D1", + "kind": "reading_rule_component", + "classification": "PROVED_REVIEWED", + "controlling": false, + "component_of": "math.uniform-matrix-cap-lifetime", + "component_role": "amendment", + "author_provider": "OpenAI", + "fingerprint": "845abf9f9c99d672c2a10a887b5a2e7206a3d2de3d876f35f75ff6e2dc13e62f", + "source": "reviews/d1_section9_borel_repair_20260925/REPAIR.md", + "ledger_items": [ + "D1-B-E2" + ], + "review_basis": [ + { + "review": "C1", + "provider": "Anthropic", + "verdict": "ACCEPT", + "depth": "full" + }, + { + "review": "G2", + "provider": "xAI", + "verdict": "ACCEPT", + "depth": "full" + } + ], + "review_source": "reviews/d1_chain_reconciliation_20260928/LEDGER.json", + "scope": "replaces parent section 9 (Borel elder mark in weighted pair Kac-Rice), C1-C6" + }, + "math.d1-component.marked-cylinder-cap": { + "layer": "D1", + "kind": "reading_rule_component", + "classification": "PROVED_REVIEWED", + "controlling": false, + "component_of": "math.uniform-matrix-cap-lifetime", + "component_role": "deterministic_support", + "author_provider": "OpenAI", + "fingerprint": "0bf922b9203c29088b12388807aa0e2ecd020485eb0f6e919679841b5b2636fc", + "source": "imports/lifetime_parent_20260925/MARKED_CYLINDER_CAP_PROOF.md", + "ledger_items": [ + "CAP" + ], + "review_basis": [ + { + "review": "C1", + "provider": "Anthropic", + "verdict": "ACCEPT", + "depth": "full" + }, + { + "review": "G3", + "provider": "xAI", + "verdict": "ACCEPT", + "depth": "full" + } + ], + "review_source": "reviews/d1_chain_reconciliation_20260928/LEDGER.json", + "scope": "deterministic separating cap, sections 1-5 (lines 1-168) only; sections 6-8 are not consumed" + }, + "math.d1-component.reconciliation-record": { + "layer": "D1", + "kind": "reading_rule_component", + "classification": "PROVED_REVIEWED", + "controlling": false, + "component_of": "math.uniform-matrix-cap-lifetime", + "component_role": "reading_rule_record", + "author_provider": "Anthropic", + "source": "reviews/d1_chain_reconciliation_20260928/", + "ledger_items": [ + "S11", + "S12", + "R-W1", + "R-embedding-radius" + ], + "review_basis": [ + { + "review": "C2", + "provider": "Anthropic", + "verdict": "ACCEPT", + "depth": "full", + "item": "S11, S12 (record section 6)" + }, + { + "item": "R-W1", + "raised_in": "C1", + "raised_by_provider": "Anthropic", + "discharged_in": "RECONCILIATION.md section 5" + }, + { + "item": "R-embedding-radius", + "raised_in": "G3", + "raised_by_provider": "xAI", + "discharged_in": "RECONCILIATION.md section 5" + } + ], + "technical_checks_non_discharge": [ + { + "review": "https://github.com/d6g8k5htny-coder/Math-/pull/126#pullrequestreview-5345687857", + "provider": "OpenAI", + "role": "author provider of the parent; A4, section 12 and register binding; never discharge" + } + ], + "review_source": "reviews/d1_chain_reconciliation_20260928/LEDGER.json", + "scope": "nonauthor record binding the reading rule (E1, E2, W1, r < L/(4 sqrt 2)) and the interface-to-review ledger; the whole directory is bound" }, "math.lifetime-remainder": { "layer": "D2", @@ -130,7 +280,11 @@ "review_issue": 67, "fingerprint": "380b7d0abdb0fe2de5a6564565af9560d3f1b1ce22fd5538927db0c52f4f3a4a", "source": "frontiers/three_fronts_20260924/LIFETIME_REMAINDER.md", - "notes": "Imports named #63 interfaces; not parent collapse" + "notes": "Imports named #63 interfaces (D1-A-E); not parent collapse; does not consume Theorem A (1.1)", + "review_disposition": "ACCEPT", + "review_provider": "xAI/Grok via Cursor", + "review_source": "https://github.com/d6g8k5htny-coder/main/issues/67#issuecomment-5841782206", + "scope": "Theorem R at its stated existential O(1)-remainder scope; no numerical constants or radii" }, "math.side24-coefficient": { "layer": "D3", @@ -140,7 +294,11 @@ "review_issue": 65, "fingerprint": "c06daccc4ba4b9168522b9888b76a7d599934fc3b91bd753ee5d492262917769", "source": "coefficients/side24_v1/PROOF.md", - "notes": "Evaluates #63 Eq15.2; parent unreviewed" + "notes": "Evaluates parent Eq15.2; parent reconciled in reviews/d1_chain_reconciliation_20260928/RECONCILIATION.md", + "review_disposition": "ACCEPT", + "review_provider": "xAI/Grok via Cursor", + "review_source": "https://github.com/d6g8k5htny-coder/main/issues/65#issuecomment-5841269490", + "scope": "coefficient calculation for SIDE24 d=2,3; persistence reading via reconciled parent Theorem C; no finite-radius band" }, "math.rn-count-interface": { "layer": "D4", @@ -314,6 +472,30 @@ "required": true, "relation": "evaluates_eq_15_2" }, + { + "from": "math.uniform-matrix-cap-lifetime", + "to": "math.d1-component.congruence-erratum", + "required": true, + "relation": "reads_with_congruence_erratum" + }, + { + "from": "math.uniform-matrix-cap-lifetime", + "to": "math.d1-component.section9-replacement-v1_1", + "required": true, + "relation": "reads_section9_as_replaced_v1_1" + }, + { + "from": "math.uniform-matrix-cap-lifetime", + "to": "math.d1-component.marked-cylinder-cap", + "required": true, + "relation": "consumes_cap_sections_1_5" + }, + { + "from": "math.uniform-matrix-cap-lifetime", + "to": "math.d1-component.reconciliation-record", + "required": true, + "relation": "reads_with_reconciled_rule_W1_radius" + }, { "from": "math.rn-fixed-remote-window", "to": "math.rn-count-interface", diff --git a/frontiers/downstream_gate_20260925/README.md b/frontiers/downstream_gate_20260925/README.md index 7f07316b7..6ff49b966 100644 --- a/frontiers/downstream_gate_20260925/README.md +++ b/frontiers/downstream_gate_20260925/README.md @@ -39,11 +39,17 @@ python -B -S run_validation.py --output /tmp/downstream-gate-new-run python -B -S git_transition_audit.py --repo /path/to/repository --base FULL_BASE_SHA --head FULL_HEAD_SHA --output /tmp/new-transition.json ``` -67 distinct tests and 24 assertion-detected semantic mutants are required in both Python modes. +71 distinct tests and 24 assertion-detected semantic mutants are required in both Python modes. The source-bound CI workflow also runs 177 existing coefficient/lifetime/price/remote regressions, -for 244 distinct methods, and audits actual PR base/test-merge source objects. Workflow execution +for 248 distinct methods, and audits actual PR base/test-merge source objects. Workflow execution and branch-protection enforcement are separate; no administration setting is claimed here. +D1 is a composite object. Its congruence erratum, Section 9 replacement v1.1, cap Sections 1-5 and the +reconciliation record (wording W1, embedding radius, interface ledger) are separate source nodes that D1 +requires, so a byte change or deletion of any of them proposes D1, D2 and D3 for revalidation even when the +parent bytes are unchanged. Real two-commit regressions cover each component, an unrelated edit, and the +pre-binding graph that missed such changes. + The source manifest includes the nested D0 patch. All pins are checked before and after execution. A changed source requires a deliberately regenerated manifest and result file, not a skipped check. diff --git a/frontiers/downstream_gate_20260925/RESULTS.json b/frontiers/downstream_gate_20260925/RESULTS.json index 869d7170e..65b2bdb3f 100644 --- a/frontiers/downstream_gate_20260925/RESULTS.json +++ b/frontiers/downstream_gate_20260925/RESULTS.json @@ -6,7 +6,7 @@ "hist.rnu_env.py" ], "illegal_controlling_count": 0, - "open_or_author_side_count": 21 + "open_or_author_side_count": 20 }, "d0_ci_unblock": { "ci_error": "PROBLEM packet: unexpected files ['DOWNSTREAM_CROSSWALK_20260925.md']", @@ -107,20 +107,18 @@ "allowed": false, "blocked_absent": [], "meaning": "integrity decision only; not theorem acceptance", - "missing_terminal": [ - { - "classification": "AUTHOR_SIDE_CANDIDATE", - "id": "math.uniform-matrix-cap-lifetime" - } - ], + "missing_terminal": [], "node": "math.lifetime-remainder", "reasons": [ - "node classification is not eligible for positive CONTROLLING status: AUTHOR_SIDE_CANDIDATE", - "required transitive dependency is not satisfied" + "node classification is not eligible for positive CONTROLLING status: AUTHOR_SIDE_CANDIDATE" ], "refuted_required": [], "required_dependencies": [ - "math.uniform-matrix-cap-lifetime" + "math.uniform-matrix-cap-lifetime", + "math.d1-component.congruence-erratum", + "math.d1-component.section9-replacement-v1_1", + "math.d1-component.marked-cylinder-cap", + "math.d1-component.reconciliation-record" ], "would_be_controlling": false }, @@ -149,20 +147,18 @@ "allowed": false, "blocked_absent": [], "meaning": "integrity decision only; not theorem acceptance", - "missing_terminal": [ - { - "classification": "AUTHOR_SIDE_CANDIDATE", - "id": "math.uniform-matrix-cap-lifetime" - } - ], + "missing_terminal": [], "node": "math.side24-coefficient", "reasons": [ - "node classification is not eligible for positive CONTROLLING status: AUTHOR_SIDE_CANDIDATE", - "required transitive dependency is not satisfied" + "node classification is not eligible for positive CONTROLLING status: AUTHOR_SIDE_CANDIDATE" ], "refuted_required": [], "required_dependencies": [ - "math.uniform-matrix-cap-lifetime" + "math.uniform-matrix-cap-lifetime", + "math.d1-component.congruence-erratum", + "math.d1-component.section9-replacement-v1_1", + "math.d1-component.marked-cylinder-cap", + "math.d1-component.reconciliation-record" ], "would_be_controlling": false } diff --git a/frontiers/downstream_gate_20260925/SOURCE_FILES.json b/frontiers/downstream_gate_20260925/SOURCE_FILES.json index 00b547252..19363814c 100644 --- a/frontiers/downstream_gate_20260925/SOURCE_FILES.json +++ b/frontiers/downstream_gate_20260925/SOURCE_FILES.json @@ -5,16 +5,16 @@ "sha256": "2423fa7d3519a5ba06739cb43cc72e26db70020350338a1fa508e5adfb109643" }, "GRAPH.json": { - "bytes": 15375, - "sha256": "065e6a756060097bcef35055cbf2aa099905f615e82b2942770b142cf4bf2f8f" + "bytes": 22830, + "sha256": "53057a110d64e8bf135a19b8e7681a594c3c3fda18b1133136ba1b0ebba7ce20" }, "README.md": { - "bytes": 3559, - "sha256": "574ed537cf8992bb3f86fae109e18336e51c18ea814e69451d39901b94fea80a" + "bytes": 4025, + "sha256": "13fc1accebebd6017f34b0e5473bf6338f2604948c25a002051b5f0620fc327a" }, "RESULTS.json": { - "bytes": 6509, - "sha256": "2fd874894334f65b57bbab438d093c7dee37395e8352bdd49ee04410da9240da" + "bytes": 6535, + "sha256": "a513d80f0e54e229955cd2f63e1119e029ee13105c5531359cda1cb411801545" }, "SCOPE.md": { "bytes": 2218, @@ -38,15 +38,15 @@ }, "run_validation.py": { "bytes": 7517, - "sha256": "2f71b34d5a241402e26c0e0046fece88e1c9f2ea07c4920735b0a3d1306fba6c" + "sha256": "276e69c2b29e012c386db615ed64e24badf3726a9f122fd9d77776a9c4f00711" }, "test_hard_gate.py": { - "bytes": 18920, - "sha256": "24bf0ae39c3b36ff253ee7dbbb5c5b347ab8c528c88d2d9cf578ef6b3ab04e51" + "bytes": 22691, + "sha256": "0f28ed996a50a1676b91a17198cf090086976e9eaf6a61aa9652f03acc427cf0" }, "test_transition_contract.py": { - "bytes": 8006, - "sha256": "d9851a322274fea01e7f74db283ed70ea798bc6a35423f66c7cfddad7d92c829" + "bytes": 12679, + "sha256": "ab69008b5c0c136dcdf742ecd1213e1c5b4b08e7aa4c9d0747037acaa8633c37" } }, "meaning": "Exact identity, not theorem correctness", diff --git a/frontiers/downstream_gate_20260925/run_validation.py b/frontiers/downstream_gate_20260925/run_validation.py index d0607468b..58c2b5e85 100644 --- a/frontiers/downstream_gate_20260925/run_validation.py +++ b/frontiers/downstream_gate_20260925/run_validation.py @@ -8,7 +8,7 @@ import sys ROOT = Path(__file__).resolve().parent -EXPECTED_TESTS = 67 +EXPECTED_TESTS = 71 MUTANTS = { 'bypass_own_node_eligibility': ("if node_classification not in CONTROLLING_ELIGIBLE:", "if False:"), 'allow_required_superseded_label': ( diff --git a/frontiers/downstream_gate_20260925/test_hard_gate.py b/frontiers/downstream_gate_20260925/test_hard_gate.py index 62c5e249b..1c8c9f63e 100644 --- a/frontiers/downstream_gate_20260925/test_hard_gate.py +++ b/frontiers/downstream_gate_20260925/test_hard_gate.py @@ -48,15 +48,72 @@ def test_lemma_closed_never_true(self): def test_lifetime_requires_parent(self): deps = m.required_dependencies(self.graph, 'math.lifetime-remainder') self.assertEqual(deps, ['math.uniform-matrix-cap-lifetime']) - decision = m.promotion_allowed(self.graph, 'math.lifetime-remainder') + # Pre-reconciliation fixture: an unreviewed parent must block the dependent. + pre = copy.deepcopy(self.graph) + pre['nodes']['math.uniform-matrix-cap-lifetime']['classification'] = 'AUTHOR_SIDE_CANDIDATE' + decision = m.promotion_allowed(pre, 'math.lifetime-remainder') self.assertFalse(decision['allowed']) self.assertTrue(any(x['id'] == 'math.uniform-matrix-cap-lifetime' for x in decision['missing_terminal'])) + # Live graph: the reconciled parent satisfies the edge; the dependent's own + # author-side classification still refuses promotion. + live = m.promotion_allowed(self.graph, 'math.lifetime-remainder') + self.assertEqual(self.graph['nodes']['math.uniform-matrix-cap-lifetime']['classification'], + 'PROVED_REVIEWED') + self.assertEqual(live['missing_terminal'], []) + self.assertFalse(live['allowed']) + + def test_d1_reading_rule_components_bound_and_reviewed(self): + # Every mandatory reading-rule component is its own source node, required by D1, so a byte change + # in any of them reaches D1, D2 and D3 through reverse impact. Each carries the review its role needs. + d1 = 'math.uniform-matrix-cap-lifetime' + roles = { + 'imports/lifetime_parent_20260925/ERRATUM_CONGRUENCE.md': 'amendment', + 'reviews/d1_section9_borel_repair_20260925/REPAIR.md': 'amendment', + 'imports/lifetime_parent_20260925/MARKED_CYLINDER_CAP_PROOF.md': 'deterministic_support', + 'reviews/d1_chain_reconciliation_20260928/': 'reading_rule_record', + } + nodes = self.graph['nodes'] + author = nodes[d1]['author_provider'] + components = [c for c in m.required_dependencies(self.graph, d1)] + bound = {nodes[c]['source']: c for c in components} + self.assertEqual(len(bound), len(components)) + self.assertEqual(set(bound), set(roles)) + for path, role in roles.items(): + node = nodes[bound[path]] + self.assertEqual(node['classification'], 'PROVED_REVIEWED') + self.assertFalse(node['controlling']) + self.assertEqual((node['component_of'], node['component_role']), (d1, role)) + basis = node['review_basis'] + if role == 'reading_rule_record': + self.assertNotEqual(node['author_provider'], author) + self.assertFalse(any(author in (b.get('provider'), b.get('raised_by_provider')) for b in basis)) + self.assertTrue(node['technical_checks_non_discharge']) + self.assertTrue(all(c['provider'] == author for c in node['technical_checks_non_discharge'])) + else: + self.assertEqual(node['author_provider'], author) + self.assertTrue(any(b['provider'] != author and b['verdict'] == 'ACCEPT' and b['depth'] == 'full' + for b in basis)) + for child in ('math.lifetime-remainder', 'math.side24-coefficient'): + self.assertTrue(set(components) <= set(m.transitive_required(self.graph, child))) + # An unreviewed component still blocks both dependents. + pre = copy.deepcopy(self.graph) + pre['nodes'][bound['reviews/d1_section9_borel_repair_20260925/REPAIR.md']]['classification'] = 'AUTHOR_SIDE_CANDIDATE' + decision = m.promotion_allowed(pre, 'math.side24-coefficient') + self.assertIn(bound['reviews/d1_section9_borel_repair_20260925/REPAIR.md'], + [x['id'] for x in decision['missing_terminal']]) def test_side24_requires_parent(self): - decision = m.promotion_allowed(self.graph, 'math.side24-coefficient') + pre = copy.deepcopy(self.graph) + pre['nodes']['math.uniform-matrix-cap-lifetime']['classification'] = 'AUTHOR_SIDE_CANDIDATE' + decision = m.promotion_allowed(pre, 'math.side24-coefficient') self.assertFalse(decision['allowed']) self.assertIn('math.uniform-matrix-cap-lifetime', decision['required_dependencies']) + self.assertTrue(any(x['id'] == 'math.uniform-matrix-cap-lifetime' + for x in decision['missing_terminal'])) + live = m.promotion_allowed(self.graph, 'math.side24-coefficient') + self.assertEqual(live['missing_terminal'], []) + self.assertFalse(live['allowed']) def test_fixed_remote_requires_count_interface(self): deps = m.transitive_required(self.graph, 'math.rn-fixed-remote-window') diff --git a/frontiers/downstream_gate_20260925/test_transition_contract.py b/frontiers/downstream_gate_20260925/test_transition_contract.py index 0316d8da5..fca3ee258 100644 --- a/frontiers/downstream_gate_20260925/test_transition_contract.py +++ b/frontiers/downstream_gate_20260925/test_transition_contract.py @@ -8,6 +8,16 @@ import hard_gate as m import git_transition_audit as gitaudit +LIVE_GRAPH = Path(__file__).resolve().parent / 'GRAPH.json' +GRAPH_REL = 'frontiers/downstream_gate_20260925/GRAPH.json' +D1, D2, D3 = 'math.uniform-matrix-cap-lifetime', 'math.lifetime-remainder', 'math.side24-coefficient' +D1_COMPONENT_FILES = ( + 'imports/lifetime_parent_20260925/ERRATUM_CONGRUENCE.md', + 'reviews/d1_section9_borel_repair_20260925/REPAIR.md', + 'imports/lifetime_parent_20260925/MARKED_CYLINDER_CAP_PROOF.md', + 'reviews/d1_chain_reconciliation_20260928/RECONCILIATION.md', +) + def graph(): return {'schema_version': 1, 'nodes': { @@ -140,6 +150,76 @@ def run(*args): r = gitaudit.audit(repo, new, run('rev-parse', 'HEAD'), 'GRAPH.json') self.assertFalse(r['check_passed']); self.assertEqual(r['controlling_impacted'], ['L']) + def _live_fixture(self, tmp, graph_obj): + """A real Git repository holding the given graph and placeholder bytes at every repository source path.""" + repo = Path(tmp) + def run(*args): + return subprocess.run(['git', '-C', tmp, *args], check=True, capture_output=True).stdout.decode().strip() + run('init', '-q'); run('config', 'user.name', 'local test'); run('config', 'user.email', 'test@example.invalid') + (repo/GRAPH_REL).parent.mkdir(parents=True, exist_ok=True) + (repo/GRAPH_REL).write_text(json.dumps(graph_obj)) + paths = list(D1_COMPONENT_FILES) + ['UNRELATED.md'] + for node in graph_obj['nodes'].values(): + src = node.get('source') + if src and not src.startswith(('https://', 'http://', 'external:')): + paths.append(src + 'README.md' if src.endswith('/') else src) + for rel in paths: + (repo/rel).parent.mkdir(parents=True, exist_ok=True) + if not (repo/rel).exists(): + (repo/rel).write_text('fixture bytes for ' + rel + '\n') + run('add', '.'); run('commit', '-qm', 'baseline') + return repo, run + + def test_git_d1_component_change_revalidates_d1_d2_d3(self): + live = json.loads(LIVE_GRAPH.read_text()) + with tempfile.TemporaryDirectory() as tmp: + repo, run = self._live_fixture(tmp, live) + base = run('rev-parse', 'HEAD') + parent = live['nodes'][D1]['source'] + parent_bytes = (repo/parent).read_bytes() + for rel in D1_COMPONENT_FILES: + for action in ('edit', 'delete'): + with self.subTest(component=rel, action=action): + run('reset', '-q', '--hard', base) + if action == 'edit': + (repo/rel).write_text('amended bytes\n'); run('add', rel) + else: + run('rm', '-q', rel) + run('commit', '-qm', action + ' ' + rel) + r = gitaudit.audit(repo, base, run('rev-parse', 'HEAD'), GRAPH_REL) + self.assertEqual((repo/parent).read_bytes(), parent_bytes) + self.assertEqual(r['old_sources'][D1], r['new_sources'][D1]) + self.assertNotIn(D1, r['changed_nodes']) + for nid in (D1, D2, D3): + self.assertEqual(r['revalidation_proposals'].get(nid), 'REVALIDATION_REQUIRED') + self.assertTrue(r['check_passed']); self.assertFalse(r['promotion_permission']) + + def test_git_unrelated_edit_does_not_revalidate_d1(self): + live = json.loads(LIVE_GRAPH.read_text()) + with tempfile.TemporaryDirectory() as tmp: + repo, run = self._live_fixture(tmp, live) + base = run('rev-parse', 'HEAD') + (repo/'UNRELATED.md').write_text('changed\n'); run('add', '.'); run('commit', '-qm', 'unrelated') + r = gitaudit.audit(repo, base, run('rev-parse', 'HEAD'), GRAPH_REL) + self.assertEqual((r['changed_nodes'], r['impacted']), ([], [])) + + def test_git_pre_repair_graph_misses_component_change(self): + # The fault this binding closes: with the components only named in metadata, an erratum edit left D1, + # D2 and D3 untouched. Kept as a sensitivity control for the fixture above. + live = json.loads(LIVE_GRAPH.read_text()) + pre = copy.deepcopy(live) + comps = {nid for nid, n in pre['nodes'].items() if n.get('component_of') == D1} + self.assertEqual(len(comps), len(D1_COMPONENT_FILES)) + for nid in comps: + del pre['nodes'][nid] + pre['edges'] = [e for e in pre['edges'] if e['to'] not in comps] + with tempfile.TemporaryDirectory() as tmp: + repo, run = self._live_fixture(tmp, pre) + base = run('rev-parse', 'HEAD') + (repo/D1_COMPONENT_FILES[0]).write_text('amended bytes\n'); run('add', '.'); run('commit', '-qm', 'erratum') + r = gitaudit.audit(repo, base, run('rev-parse', 'HEAD'), GRAPH_REL) + self.assertEqual(r['impacted'], []) + def test_git_requires_immutable_revision(self): with self.assertRaises(ValueError): gitaudit.read_snapshot(Path('.'), 'main', 'GRAPH.json') diff --git a/reviews/d1_chain_reconciliation_20260928/LEDGER.json b/reviews/d1_chain_reconciliation_20260928/LEDGER.json new file mode 100644 index 000000000..f6c329fb0 --- /dev/null +++ b/reviews/d1_chain_reconciliation_20260928/LEDGER.json @@ -0,0 +1,80 @@ +{ + "schema": 1, + "object": "D1-CHAIN-RECONCILIATION-20260928-v1", + "meaning": "Interface ledger for the D1 parent chain. A review discharges an interface only if its provider is not an author provider and its depth is full.", + "author_providers": ["OpenAI"], + "sources": { + "P": {"path": "imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md", "git_blob": "dfed3b8d318a3ab1950957f393307733a4bef3f2", "bytes": 40261, "sha256": "9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7", "lines": 494}, + "CAP": {"path": "imports/lifetime_parent_20260925/MARKED_CYLINDER_CAP_PROOF.md", "git_blob": "0633aca3c2a2882b0de4399da0a75d64c2e6b2e1", "bytes": 15160, "sha256": "0bf922b9203c29088b12388807aa0e2ecd020485eb0f6e919679841b5b2636fc", "lines": 230}, + "E1": {"path": "imports/lifetime_parent_20260925/ERRATUM_CONGRUENCE.md", "git_blob": "213594d6ca6a86fb938110f4d166d9ce275a02d0", "bytes": 1782, "sha256": "bad7ef609c4ad8c41ad6af562c1b6807921e19a9d556ed793ad1a0db6e202028"}, + "E2": {"path": "reviews/d1_section9_borel_repair_20260925/REPAIR.md", "git_blob": "fe9b9ce4999908bb3814b500ee2d0ceb0c6f704a", "bytes": 9062, "sha256": "845abf9f9c99d672c2a10a887b5a2e7206a3d2de3d876f35f75ff6e2dc13e62f"} + }, + "local_records": { + "C1": {"path": "reviews/d1_theorem_a_nonauthor_20260928/REVIEW.md", "git_blob": "bc11369c41ebc76de5700df3f931939ccfc88b9b", "bytes": 24105, "sha256": "b7328d4bab97fa2d12622ca730dc698970febc1ea8bcbc0b24555e69e2a66392"}, + "G2": {"path": "reviews/d1_section9_borel_grok_lucas_20260928/REVIEW.md", "git_blob": "48ea9ad5a3ae5a1515a3533a4c776800547a92bc", "bytes": 4287, "sha256": "a654ea6b52181fa46371c3a2ef9ee17e82f8e365f9de24857526c6dd48154d7e"}, + "LOWER": {"path": "frontiers/window_multiplicity_laws_20260928/ELDER_LOWER_AND_DENSITY_GAP.md", "git_blob": "aaefc8da9668e819591dd9db0b34442394f2362e", "bytes": 10229, "sha256": "8ce05a43bde8e0d718f09e2da1ffe75d3ec5893489254afdbf5b58b602cdba0c"}, + "LOWER_REVIEW": {"path": "reviews/d1_elder_lower_claude_20260928/REVIEW.md", "git_blob": "179c1e6d3d4005b2e406b1bd4d9584caf5465793", "bytes": 16640, "sha256": "53bd5289a2060ce6c906023ed09a5aec457313e782135e1df86e743941839495"}, + "D2": {"path": "frontiers/three_fronts_20260924/LIFETIME_REMAINDER.md", "git_blob": "247b3ecf80bfbe896948d5d489b2d5842a81c481", "bytes": 17734, "sha256": "380b7d0abdb0fe2de5a6564565af9560d3f1b1ce22fd5538927db0c52f4f3a4a"}, + "D3": {"path": "coefficients/side24_v1/PROOF.md", "git_blob": "44b66f04f89fcd87383b3603fa69f1feb64cdddd", "bytes": 10272, "sha256": "c06daccc4ba4b9168522b9888b76a7d599934fc3b91bd753ee5d492262917769"} + }, + "reviews": { + "G1": {"provider": "xAI", "model": "Grok 4.7 via Cursor", "session": "bc-ce4bf0bc-0a0b-4cb1-abaf-7c5b8914418c", "locator": "https://github.com/d6g8k5htny-coder/main/issues/63#issuecomment-5841570965"}, + "C1": {"provider": "Anthropic", "model": "Claude (Claude Code)", "session": "session_017Mi3hxjaxV45x6zo6o1ee3", "locator": "local_records.C1 and https://github.com/d6g8k5htny-coder/main/issues/63#issuecomment-5873873903"}, + "G2": {"provider": "xAI", "model": "Grok, Lucas lane", "session": "Math-#112 body (attributed narrative record)", "locator": "local_records.G2"}, + "G3": {"provider": "xAI", "model": "Grok via Cursor, replay rounds 3-9", "session": "main#163 incoming packet", "locator": "https://github.com/d6g8k5htny-coder/main/tree/main/incoming/grok-session-20260926-replay"}, + "G4": {"provider": "xAI", "model": "Grok 4.7 via Cursor", "session": "bc-81faa729 and bc-dfbce246", "locator": "https://github.com/d6g8k5htny-coder/main/issues/67#issuecomment-5841270276 and #issuecomment-5841782206"}, + "C2": {"provider": "Anthropic", "model": "Claude (Claude Code)", "session": "session_017Mi3hxjaxV45x6zo6o1ee3", "locator": "RECONCILIATION.md section 6"}, + "O1": {"provider": "OpenAI", "model": "OpenAI technical review", "session": "Math-#106 review 5341593068", "locator": "https://github.com/d6g8k5htny-coder/Math-/pull/106#pullrequestreview-5341593068"} + }, + "interfaces": [ + {"id": "S1", "source": "P", "lines": [[9, 53]], "component": "statements", "claim": "model, conventions and the statements of Theorems A-C", "reviews": [{"by": "G1", "verdict": "ACCEPT", "depth": "full"}, {"by": "C1", "verdict": "ACCEPT", "depth": "full"}]}, + {"id": "A1", "source": "P", "lines": [[54, 68]], "component": "I-normalizer", "claim": "positive Fourier spectrum, finite-jet rank, smooth version", "reviews": [{"by": "C1", "verdict": "ACCEPT", "depth": "full"}, {"by": "G3", "verdict": "ACCEPT", "depth": "partial"}]}, + {"id": "A2", "source": "P", "lines": [[69, 114]], "component": "I-normalizer", "claim": "contact frame, |det T_r| = 12 r^-(d+3), uniform covariance gap, density (3.5)", "reviews": [{"by": "C1", "verdict": "ACCEPT", "depth": "full"}, {"by": "G3", "verdict": "ACCEPT", "depth": "partial"}]}, + {"id": "A4", "source": "P", "lines": [[115, 137]], "component": "I-normalizer", "claim": "(4.1)-(4.3), independent matrix residual, uniform moments", "reviews": [{"by": "C1", "verdict": "ACCEPT", "depth": "full"}]}, + {"id": "A3", "source": "P", "lines": [[138, 183]], "component": "I-normalizer", "claim": "(5.1)-(5.5) with erratum E1 and wording W1: type convergence, UI, floor z_*", "reviews": [{"by": "C1", "verdict": "ACCEPT", "depth": "full"}, {"by": "G3", "verdict": "ACCEPT", "depth": "partial"}, {"by": "O1", "verdict": "ACCEPT", "depth": "full"}]}, + {"id": "A3-E1", "source": "E1", "lines": "all", "component": "I-normalizer", "claim": "congruence factor D_r = diag(r^-1/2, I)", "reviews": [{"by": "C1", "verdict": "ACCEPT", "depth": "full"}, {"by": "G3", "verdict": "ACCEPT", "depth": "full"}]}, + {"id": "A5", "source": "P", "lines": [[184, 197]], "component": "II-defect", "claim": "(6.1) canceled-pivot bound, every m", "reviews": [{"by": "C1", "verdict": "ACCEPT", "depth": "full"}, {"by": "G3", "verdict": "ACCEPT", "depth": "partial"}]}, + {"id": "A6", "source": "P", "lines": [[198, 211]], "component": "II-defect", "claim": "(6.2) two soft factors including the 3/2 saddle mixed-square term", "reviews": [{"by": "C1", "verdict": "ACCEPT", "depth": "full"}, {"by": "G4", "verdict": "ACCEPT", "depth": "full"}]}, + {"id": "A7", "source": "P", "lines": [[212, 275]], "component": "II-defect", "claim": "(7.1)-(7.8): r^5 numerators, corank strata, m=1 far branch, M4 exception, division by the full floor", "reviews": [{"by": "C1", "verdict": "ACCEPT", "depth": "full"}, {"by": "G4", "verdict": "ACCEPT", "depth": "partial"}]}, + {"id": "CAP", "source": "CAP", "lines": [[1, 168]], "component": "III-elder", "claim": "deterministic separating cap: unique ridge, boundary exits <= s, ridge to a point above b, global maximin level s", "reviews": [{"by": "C1", "verdict": "ACCEPT", "depth": "full"}, {"by": "G3", "verdict": "ACCEPT", "depth": "full"}]}, + {"id": "D1-A", "source": "P", "lines": [[276, 297]], "component": "III-elder", "claim": "pinned genericity, Borel elder event, G_r implies global elder partner S", "reviews": [{"by": "G1", "verdict": "ACCEPT", "depth": "full"}, {"by": "C1", "verdict": "ACCEPT", "depth": "full"}]}, + {"id": "D1-B", "source": "P", "lines": [[298, 309]], "component": "IV-kac-rice", "claim": "Borel marked Kac-Rice interface (read as replaced by E2)", "reviews": [{"by": "G1", "verdict": "ACCEPT", "depth": "full"}]}, + {"id": "D1-B-E2", "source": "E2", "lines": "all", "component": "IV-kac-rice", "claim": "section 9 replacement v1.1, C1-C6", "reviews": [{"by": "C1", "verdict": "ACCEPT", "depth": "full"}, {"by": "G2", "verdict": "ACCEPT", "depth": "full"}]}, + {"id": "D1-C", "source": "P", "lines": [[310, 336]], "component": "IV-kac-rice", "claim": "radial ledger r A_r dr db dk dsigma, A_r = 12 pi_r Z_r/r^2", "reviews": [{"by": "G1", "verdict": "ACCEPT", "depth": "full"}, {"by": "C1", "verdict": "ACCEPT", "depth": "partial"}]}, + {"id": "S11", "source": "P", "lines": [[337, 364]], "component": "IV-lifetime", "claim": "lifetime pushforward (11.1)-(11.3) and the compact difference (1.2)", "reviews": [{"by": "C2", "verdict": "ACCEPT", "depth": "full"}, {"by": "G4", "verdict": "ACCEPT", "depth": "partial"}]}, + {"id": "S12", "source": "P", "lines": [[365, 385]], "component": "IV-lifetime", "claim": "cumulative and moment corollaries (12.1)-(12.3)", "reviews": [{"by": "C2", "verdict": "ACCEPT", "depth": "full"}]}, + {"id": "D1-D", "source": "P", "lines": [[386, 446]], "component": "IV-lifetime", "claim": "target-growth majorant, k->0 integrability, off-diagonal (14.1), Theorem C assembly", "reviews": [{"by": "G1", "verdict": "ACCEPT", "depth": "full"}, {"by": "C2", "verdict": "ACCEPT", "depth": "partial"}]}, + {"id": "D1-E", "source": "P", "lines": [[447, 481]], "component": "IV-lifetime", "claim": "parity, b-disintegration and the gamma factor in (15.2)", "reviews": [{"by": "G1", "verdict": "ACCEPT", "depth": "full"}, {"by": "C2", "verdict": "ACCEPT", "depth": "partial"}]} + ], + "meta_ranges": { + "P": [{"lines": [1, 8], "reason": "object header, no mathematical claim"}, {"lines": [482, 494], "reason": "supplied-interface list, limits and attribution; no mathematical claim"}], + "CAP": [{"lines": [169, 230], "reason": "fixed-axis 2D SIDE24 numerical corollary and constant comparison; NOT consumed by P and NOT accepted here"}] + }, + "theorems": { + "Theorem A (1.1)": ["S1", "A1", "A2", "A4", "A3", "A3-E1", "A5", "A6", "A7", "CAP", "D1-A"], + "Theorem B (1.2)": ["S1", "A1", "A2", "A4", "A3", "A3-E1", "A5", "A6", "A7", "CAP", "D1-A", "D1-B", "D1-B-E2", "D1-C", "S11"], + "Theorem C (1.3)": ["S1", "A1", "A2", "A4", "A3", "A3-E1", "A5", "A6", "A7", "CAP", "D1-A", "D1-B", "D1-B-E2", "D1-C", "D1-D", "D1-E"], + "Section 12 corollaries": ["S11", "S12", "D1-D", "D1-E"] + }, + "residual_items": [ + {"id": "R-A3-congruence", "raised_in": "main#63 5841947606; G3 A3_TYPE_CONVERGENCE C1", "discharged_by": ["A3-E1"], "status": "DISCHARGED"}, + {"id": "R-A3-UI", "raised_in": "G3 A3_TYPE_CONVERGENCE C4", "discharged_by": ["A3"], "status": "DISCHARGED"}, + {"id": "R-A3-type", "raised_in": "G3 A3_TYPE_CONVERGENCE", "discharged_by": ["A3"], "status": "DISCHARGED"}, + {"id": "R-A3-floor", "raised_in": "G3 A3_TYPE_CONVERGENCE C3", "discharged_by": ["A3"], "status": "DISCHARGED"}, + {"id": "R-A3-AM-A0", "raised_in": "G3 A_M_TO_A0", "discharged_by": ["A3", "A1", "A2"], "status": "DISCHARGED"}, + {"id": "R-A2-gap", "raised_in": "G3 A2_RESIDUAL_GAP", "discharged_by": ["A2"], "status": "DISCHARGED"}, + {"id": "R-A5-m2", "raised_in": "G3 D1_INTERFACE_TABLE", "discharged_by": ["A5"], "status": "DISCHARGED"}, + {"id": "R-A7-r5", "raised_in": "G3 D1_INTERFACE_TABLE; C1 v1 far-branch wording", "discharged_by": ["A7"], "status": "DISCHARGED"}, + {"id": "R-cap-pairing", "raised_in": "G3 EMBEDDED_CHART_AND_MORSE; CAP_PAIRING_IDENTITIES", "discharged_by": ["CAP", "D1-A"], "status": "DISCHARGED"}, + {"id": "R-embedding-radius", "raised_in": "G3 EMBEDDED_CHART_AND_MORSE (slogan AMEND)", "discharged_by": ["RECONCILIATION.md section 5"], "status": "DISCHARGED"}, + {"id": "R-section9-writeup", "raised_in": "Math-PR112 review", "discharged_by": ["D1-B-E2"], "status": "DISCHARGED"}, + {"id": "R-sections-11-12", "raised_in": "this reconciliation line audit", "discharged_by": ["S11", "S12"], "status": "DISCHARGED"}, + {"id": "R-W1", "raised_in": "C1 A3 wording", "discharged_by": ["RECONCILIATION.md section 5"], "status": "DISCHARGED"} + ], + "second_provider_invited": ["A4", "A2 uniform gap", "A5 m>=2", "S11 difference bound", "S12"], + "not_consumable": ["numerical C, r_*, z_*, c_{B,K}, c_{d,L}", "(1.2) outside compact marks", "any lower bound for d>=3", "globally uniform O(r^3) over unbounded marks", "RN/24-jet/JETMOD/H3/LPW certificates", "lemma_closed, prizes, unconditional acceptance of the lifetime parent"], + "transitions": { + "Math-": ["PROOF_INDEX.md D1 to reviewed scoped", "claims/LANDING_CLAIMS.json lifetime-remainder FAIL_CLOSED->REVIEWED_SCOPED", "claims/LANDING_CLAIMS.json side24-coefficient HOLD_WITH_DOMAIN->REVIEWED_SCOPED", "GRAPH.json math.uniform-matrix-cap-lifetime AUTHOR_SIDE_CANDIDATE->PROVED_REVIEWED (controlling false)", "GRAPH.json D2/D3 review_disposition ACCEPT metadata", "GRAPH.json reading-rule components E1, E2, CAP and this record bound as PROVED_REVIEWED source nodes behind required edges from D1 (controlling false)"], + "main": ["STATUS.md D1 AMEND/open -> ACCEPT scoped (companion PR)", "formal/GLOSSARY.md D1 row", "museum/shop projections"] + } +} diff --git a/reviews/d1_chain_reconciliation_20260928/RECONCILIATION.md b/reviews/d1_chain_reconciliation_20260928/RECONCILIATION.md new file mode 100644 index 000000000..75da25979 --- /dev/null +++ b/reviews/d1_chain_reconciliation_20260928/RECONCILIATION.md @@ -0,0 +1,309 @@ +# D1 Theorem A selection chain — source-bound reconciliation + +**Object:** D1-CHAIN-RECONCILIATION-20260928-v1. +**Reconciler:** Anthropic Claude, Claude Code session `session_017Mi3hxjaxV45x6zo6o1ee3`. +**Effect:** register reconciliation. This record introduces **no new mathematical claim** about the parent. It binds +existing nonauthor reviews to exact source bytes, discharges every residual item they left open, reviews the two +parent sections that no earlier review covered (§§11–12), and states the resulting scoped status. The register edits +it justifies are listed in §9. `lemma_closed`, prizes and premises are untouched. + +## 1. The reconciled object and its reading rule + +The D1 parent is OpenAI/ChatGPT's UNIFORM-MATRIX-CAP-LIFETIME-20260924-v1, with the imported deterministic +MARKED-CYLINDER-CAP-20260924-v1. The parent bytes are immutable. The object reconciled here is the parent **read +together with** the three amendments in the table below. Every consumer must cite this identity set, not the parent +alone. + +| Role | Path (Math-) | Git blob | Bytes | SHA256 | +|---|---|---|---|---| +| Parent (P) | `imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md` | `dfed3b8d318a3ab1950957f393307733a4bef3f2` | 40261 | `9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7` | +| Cap import (CAP) | `imports/lifetime_parent_20260925/MARKED_CYLINDER_CAP_PROOF.md` | `0633aca3c2a2882b0de4399da0a75d64c2e6b2e1` | 15160 | `0bf922b9203c29088b12388807aa0e2ecd020485eb0f6e919679841b5b2636fc` | +| Amendment E1: congruence erratum | `imports/lifetime_parent_20260925/ERRATUM_CONGRUENCE.md` | `213594d6ca6a86fb938110f4d166d9ce275a02d0` | 1782 | `bad7ef609c4ad8c41ad6af562c1b6807921e19a9d556ed793ad1a0db6e202028` | +| Amendment E2: §9 replacement v1.1 | `reviews/d1_section9_borel_repair_20260925/REPAIR.md` | `fe9b9ce4999908bb3814b500ee2d0ceb0c6f704a` | 9062 | `845abf9f9c99d672c2a10a887b5a2e7206a3d2de3d876f35f75ff6e2dc13e62f` | +| Amendment E3: wording W1 and embedding radius | this record, §5 | — | — | — | + +**Reading rule.** + +- Read P §5 with E1. The congruence factor is `D_r = diag(r^{-1/2}, I)`, not the displayed `diag(√r, I)`. +- Read P §9 as replaced by E2. +- Read P l. 165 with W1 (§5 below). +- Read P §1's "sufficiently small r" as including the explicit embedding bound `r < L/(4√2)` (§5 below). + +No formula of P changes. + +**Machine binding.** Each component above is also its own source node in the hard-gate graph +(`frontiers/downstream_gate_20260925/GRAPH.json`), required by the D1 node: E1, E2, CAP (whole file; only §§1–5 +are consumed) and this record's directory, which carries E3 and `LEDGER.json`. A byte change or deletion of any +component therefore proposes D1, D2 and D3 for revalidation even when P's bytes are unchanged (§9, §10). + +**Name collision.** "Theorem A" here always means P (1.1). The fixed-remote mean-measure theorem in +`frontiers/remote_window_20260924/PROOF.md` is also called "Theorem A". That is a different theorem (D4), and +nothing in this record concerns it. + +## 2. Reconciled statements + +The model is P §1: + +- the exact L-periodized Gaussian field on `R^d/(LZ^d)`, for fixed `d >= 2` and `L > 0`; +- the six pins, generally `2(d+1)` observations; +- the typed weight `W_r` and the FULL normalizer `Z_r = E_Q W_r`; +- `p_r(b,k,R)`, the `Q^W`-probability that the global ordinary superlevel elder partner of `M` is `S`. + +The three statements below are accepted at existential scope. There is no numerical `C`, `r_*`, `z_*`, `c_{B,K}` +or `c_{d,L}`. + +- **Theorem A (P 1.1).** For compact `B` and `K ⊂ (0,∞)`, there are `C` and `r_* > 0` such that + `0 <= 1 - p_r <= C r^3`. This holds uniformly over `b ∈ B`, `k ∈ K`, all orthonormal frames and `0 < r <= r_*`. +- **Theorem B (P 1.2).** Let `B` and `K ⊂ (0,∞)` be compact intervals **of positive length** (P l. 37; a singleton + interval gives zero mark-window intensity). The compact-window densities satisfy + `ν_cand ~ ν_eld ~ c_{B,K} ℓ^{-1/3}` with `c_{B,K} > 0`. Their difference satisfies `0 <= ν_cand - ν_eld <= C ℓ^{2/3}`. +- **Theorem C (P 1.3).** All births, all positive gaps and all separations are included, and the essential class is + excluded. Then `ν_cand^all ~ ν_eld^all ~ c_{d,L} ℓ^{-1/3}` with `0 < c_{d,L} < ∞` given by (15.2). This is the + leading term only: no unrestricted remainder or difference rate is included. +- **§12 corollaries.** These are the cumulative and moment consequences (12.1)–(12.3) and their unrestricted leading + forms. + +**Sharpness in d = 2 (composition, separately sourced).** In the plane, the direct lower bound +`1 - p_r >= c r^3` combines with Theorem A to give `1 - p_r = Θ(r^3)` and `ν_cand - ν_eld = Θ(ℓ^{2/3})` on compact +marks. The lower bound is (E2) of `frontiers/window_multiplicity_laws_20260928/ELDER_LOWER_AND_DENSITY_GAP.md`, +blob `aaefc8da…`, reviewed in `reviews/d1_elder_lower_claude_20260928/`. **No lower bound is asserted for `d >= 3`.** + +## 3. The four components of the chain + +| Component | Sections | Output | Interfaces | +|---|---|---|---| +| (I) Matrix-cap normalizer | P §§2–5 with E1 and W1 | `Z_r/r^2 -> z_0 > 0` uniformly; floor `z_* r^2 <= Z_r <= z^* r^2` (5.4)–(5.5) | A1, A2, A4, A3 | +| (II) Cubic pairing-defect bound | P §§6–7 | `E_Q[W_r 1_{G_r^c}] <= C r^5`, hence `Q^W(G_r^c) <= C r^3` (7.8) | A5, A6, A7 | +| (III) Global elder selection | CAP §§2–5 and P §8 | on `G_r` ∩ {Morse, distinct values}, the global elder partner of `M` is `S`; hence `1-p_r <= Q^W(G_r^c)` | CAP, D1-A | +| (IV) Marked Kac–Rice and lifetime | E2 (§9), P §§10–15 | intensity identities, radial ledger, pushforward, majorant, off-diagonal bound, coefficient (15.2) | D1-B/E2, D1-C, §11, §12, D1-D, D1-E | + +Theorem A = (I) + (II) + (III). Theorem B = Theorem A + (IV) through §11. Theorem C = (IV) + Theorem A, which gives +`p_r -> 1` pointwise in §13. + +## 4. Interface ledger + +**Providers.** OpenAI is the author of P, CAP, E1 and E2. The nonauthor providers are xAI/Grok and Anthropic/Claude. +All lanes share one GitHub account, so no organizational independence is claimed anywhere. The full machine-readable +ledger, with every review locator, is `LEDGER.json`. + +**Review records.** + +| ID | Provider and session | Record | Verdicts | +|---|---|---|---| +| G1 | xAI Grok 4.7 via Cursor, `bc-ce4bf0bc` | [main#63 comment 5841570965](https://github.com/d6g8k5htny-coder/main/issues/63#issuecomment-5841570965) | D1-A–E ACCEPT | +| C1 | Anthropic Claude, this session | `reviews/d1_theorem_a_nonauthor_20260928/REVIEW.md` (blob `bc11369c…`, Math-#106 v2) and [main#63 comment 5873873903](https://github.com/d6g8k5htny-coder/main/issues/63#issuecomment-5873873903) | A1–A7, CAP, Theorem A and E2 C1–C6 ACCEPT; W1 | +| G2 | xAI Grok, Lucas lane | `reviews/d1_section9_borel_grok_lucas_20260928/REVIEW.md` (blob `48ea9ad5…`) | E2 C1–C6 ACCEPT. Narrative record; its runner is absent. | +| G3 | xAI Grok via Cursor, replay rounds 3–9 | main `incoming/grok-session-20260926-replay/` | Partial slices; see the table below | +| G4 | xAI Grok 4.7 via Cursor, `bc-81faa729` and `bc-dfbce246` | [main#67 5841270276](https://github.com/d6g8k5htny-coder/main/issues/67#issuecomment-5841270276), [5841782206](https://github.com/d6g8k5htny-coder/main/issues/67#issuecomment-5841782206) | While reviewing D2, re-derived P (6.2), the depth-failure integral, the m=1 split, and the far and M4 Markov pieces. Also checked the (11.3) = (13.6) coefficient identity. | +| C2 | Anthropic Claude, this record | §6 below | §11 and §12 ACCEPT; spot re-derivations of (13.1), (13.4) and (15.2) | +| O1 | OpenAI technical review of Math-#106, [5341593068](https://github.com/d6g8k5htny-coder/Math-/pull/106#pullrequestreview-5341593068) | — | Confirms W1 and the A5/A6 fixtures. **Author provider, so non-discharge.** | + +**Interfaces.** "Full" means a nonauthor provider re-derived the whole interface. "Partial" means a nonauthor provider +checked part of it; partial checks never discharge on their own. `reconciliation_check.py` computes the full-depth +counts from `LEDGER.json`. + +| Interface | P lines | Claim | Full-depth nonauthor ACCEPT | Partial second-provider check | +|---|---|---|---|---| +| S1 §1 | 9–53 | model, conventions, statements of A–C | G1, C1 (xAI, Anthropic) | — | +| A1 §2 | 54–68 | positive spectrum, jet rank, smooth version | C1 | G3 "qualitative positivity OK" | +| A2 §3 | 69–114 | contact frame, `12 r^{-(d+3)}`, uniform gap, (3.5) | C1 (including the gap proof) | G3 certified `det T_r` | +| A4 §4 | 115–137 | (4.1)–(4.3), independent residual | C1 | — | +| A3 §5 | 138–183 | (5.1)–(5.5), type convergence, UI, floor | C1 (O1 agrees but is author-provider) | G3 UI-majorant structure and `A_M -> A_0` | +| A3-E1 | erratum | `D_r = diag(r^{-1/2}, I)` | C1, G3 | — | +| A5 (6.1) | 184–197 | canceled-pivot bound, all m | C1 | G3 (m=1) | +| A6 (6.2) | 198–211 | two soft factors, including the 3/2 saddle term | C1, G4 | — | +| A7 §7 | 212–275 | `r^5` numerators, corank strata, m=1 far branch, M4, (7.8) | C1 | G4 numerator structure | +| CAP §§1–5 | cap 1–168 | deterministic separating cap, global maximin | C1, G3 | — | +| D1-A §8 | 276–297 | pinned genericity, Borel elder event, `G_r =>` partner S | G1, C1 | — | +| D1-B §9 | 298–309 | Borel marked Kac–Rice as written | G1 | — | +| D1-B-E2 | E2 | §9 replacement v1.1, C1–C6 | C1, G2 | — | +| D1-C §10 | 310–336 | radial ledger `r A_r dr db dk dσ` | G1 | C1 (#123 E9 check) | +| §11 | 337–364 | pushforward, (11.3), difference (1.2) | C2 | G4 ((11.1) and the (11.3) identity) | +| §12 | 365–385 | cumulative and moment corollaries | C2 | — | +| D1-D §§13–14 | 386–446 | target-growth majorant, `k -> 0`, off-diagonal (14.1) | G1 | C2 spot checks | +| D1-E §15 | 447–481 | parity, disintegration, (15.2) | G1 | C2 gamma factor | + +Every interface has a full-depth ACCEPT from at least one nonauthor provider. Six have full-depth ACCEPTs from both +nonauthor providers: S1, A3-E1, A6, CAP, D1-A and D1-B-E2. Nine more have a partial check by the other provider. Three +have a single provider at any depth: A4, §12, and D1-B. D1-B is the original §9 text, which the reading rule replaces by +D1-B-E2 (two providers), so it needs no second check. The project's established reconciliations (D2, D3, D4, D6 in STATUS) +each rest on one provider-distinct nonauthor review, so this meets the existing bar. §8 invites second-provider checks, +prioritized by that gap, but they are not a precondition. + +## 5. Residual items and their discharge + +Every item that an earlier record left open, AMEND or "not closed" is listed below with where it is discharged. + +| Open item | Raised in | Discharge | +|---|---|---| +| A3: wrong congruence factor `diag(√r,I)` | main#63 5841947606; G3 `A3_TYPE_CONVERGENCE` C1 | E1, landed by Math-#64 at `d8f5505`. Algebra confirmed by G3 and C1. | +| A3: UI of `W_r/r^2` | G3 C4 | C1 A3 item 4: `sup E(W_r/r^2)^2 < ∞` from (5.3), (5.1), `‖A_S‖ <= ‖A_M‖ + rM3` and A4. G3 `A3_UI_MAJORANT` gives the same majorant. | +| A3: type-indicator convergence under `D_r` | G3 | C1 W1: Slutsky joint convergence in law. The discontinuity set lies in `{det A_0 = 0}`, which is null (C1 item 5). | +| A3: `z_* > 0` | G3 C3 | C1: `A_0` is a nondegenerate Gaussian on `Sym_m`, so it charges the open cone `{A < 0}`. Continuity plus compactness gives (5.5). | +| A3: `A_M -> A_0` uniformly | G3 `A_M_TO_A0` (conditional on A1–A2) | C1 A3 item 3 and A1–A2 below. | +| A2: "single missing estimate", the uniform Gramian gap | G3 `A2_RESIDUAL_GAP` | C1 A2. Each coordinate of `U_r ⊕ vec A_r` is `∫ ∂^α f(tu) dμ_r(t)` with `μ_r -> δ_0`, so the covariance is jointly continuous on `[0,r_0] × O(d)`. It is positive definite at `r=0` by A1. Compactness gives `λ_min >= c_* > 0`. This is existential, which is all Theorem A claims. | +| A5 for `m >= 2` | G3 table | C1 A5: `det H_M = rα det(B' )` with `B' = A - (r/α)ββ^T`, and `0 < -B' <= B` on typed support. Symbolic for m=1,2,3; probed on 1,962 exact instances. | +| A7 `r^5` integrals; far branch | G3 table; C1 v1 | C1 A7, and G4. The v2 correction is that `λ >= 1/(Dr)` lies in the **majorant** event, not necessarily in depth failure. The far branch is kept in the upper bound. | +| Cap pairing: embedded chart and Morse/§8 | G3 `EMBEDDED_CHART_AND_MORSE`, `CAP_PAIRING_IDENTITIES` | §8 by G1 and C1. The embedding radius is made explicit below. | +| Embedding radius not displayed | G3 `EMBEDDED_CHART_AND_MORSE` ("AMEND the slogan") | Below: `r < L/(4√2)`. | +| §9 write-up gap (monotone-class passage) | Math-PR112 review, recorded in E2 | E2 v1.1, reviewed by C1 and G2. C1 withdrew the theorem-number objection on primary-source grounds (arXiv:2304.07424v3, Theorems 2.1, 2.2, 7.1, Remarks 7–8). | +| §§11–12 never reviewed | This reconciliation (line audit) | §6 below. | +| "Second non-Claude review of W1 and A2 before integration" | C1 request | W1 is wording only and is confirmed by O1 (non-discharge) and G3's in-law route. For A2 see the provider note in §4. The request stands as §8's open invitation. It is not a blocker under the existing bar. | + +**W1 (wording; proof unchanged).** P l. 165 says the scaled endpoint Hessians converge "in probability" to +`diag(∓6k, A_0)`. Correctly: + +- `D_r H_M D_r - diag(-6k, A_M)` and `D_r H_S D_r - diag(6k, A_M)` tend to 0 in probability, by (5.1), (5.2) and + `‖A_S - A_M‖ <= rM3`; +- `A_M -> A_0` in law. + +Slutsky then gives joint convergence in law, and continuous mapping applies off the null set `{det A_0 = 0}`. P's +subsequence paragraph (l. 176) already argues in law. + +**Embedding radius.** Let `D = [-2r, 2r] × B̄(0, 2r)`, the cap cylinder, which contains all of `G_r`'s geometry. Then +`D ⊂ B̄(0, 2√2 r)`. On `R^d/(LZ^d)` the exponential chart at any point is injective on the open ball of radius +`L/2`. So `D` is embedded whenever `2√2 r < L/2`, that is `r < L/(4√2)`. Theorem A's existential `r_*` may be, and is, +taken below this. This makes explicit what P §1 says with "for sufficiently small r". + +## 6. Review of the previously unreviewed §§11–12 (C2) + +The line audit found that no earlier record reviewed P lines 337–384. G1 lists 215–217, 276–296, 298–308, +88–94 and 310–335, 386–445, and 447–480. C1 assumed that D1-A–E covered "§§10–15", which it did not. Both sections +were reviewed here from the bytes. + +**§11 — ACCEPT.** + +- (11.1): `r = (ℓ/k)^{1/3}` gives `r dr/dℓ = (1/3) k^{-2/3} ℓ^{-1/3}`. +- Restriction: for `ℓ < k_- r_*^3`, every `k ∈ K` has `r < r_*`, so the whole pushforward stays inside Theorem A's + range. +- (11.2): at fixed `(b,k,u)`, pushing `r A_r dr` forward to `ℓ` gives `ℓ^{-1/3} A_{(ℓ/k)^{1/3}}/(3k^{2/3}) dℓ`. + Integrating over `B × K × S^{d-1}` gives the density version; `ν_eld` carries the extra factor `p_r`. +- (11.3): as `ℓ -> 0`, `A_r -> A_0` uniformly with a uniform bound (10.3), and `p_r -> 1` uniformly by Theorem A. + Dominated convergence on the compact domain gives `ℓ^{1/3} ν -> ∫ A_0/(3k^{2/3}) = 4∫ k^{-2/3} π_0 z_0 = c_{B,K}`, + using `A_0 = 12 π_0 z_0`. Positivity follows from `π_0, z_0 > 0` on a set of positive measure. G4 verified the same + identity in (13.6)'s form. +- Difference: `ν_cand - ν_eld = ℓ^{-1/3}∫ A_r(1-p_r)/(3k^{2/3})`. Theorem A gives `<= ℓ^{-1/3} ∫ A^* C r^3/(3k^{2/3})` + with `r^3 = ℓ/k`, so the bound is `C ℓ^{2/3} ∫ A^*/(3k^{5/3})`. This is finite because `k >= k_- > 0`, which proves + (1.2). The exponent `ℓ^{2/3} k^{-5/3}` is checked exactly. + +**§12 — ACCEPT.** + +- (12.1): `∫_0^t c ℓ^{-1/3}(1+o(1)) dℓ = (3/2)c t^{2/3}(1+o(1))`, and `∫_0^t C ℓ^{2/3} = (3/5)C t^{5/3}`. +- (12.2): for `q > -2/3` the integrand `ℓ^{q-1/3}` is integrable at 0, giving `c t^{q+2/3}/(q+2/3)`. +- (12.3): for `q > -5/3`, `∫_0^t ℓ^q C ℓ^{2/3} = C t^{q+5/3}/(q+5/3)`. +- For `q <= -2/3`, each individual expectation diverges because `c > 0`. (12.3) is stated for the nonselected measure + directly, not as a difference of infinities. +- The unrestricted leading forms follow from Theorem C in the same way. The compact difference rates are correctly + **not** extended. + +**Spot re-derivations for §§13–15.** These do not replace G1; they are a second provider's check. + +- (13.1): `(b - kr^3/2)^2 + 144k^2 >= (b^2+k^2)/2` for `r <= 1`. Checked exactly at sample rationals and by the + inequality `b^2 <= 2(b - kr^3/2)^2 + k^2/2`. +- (13.4): `W_r/r^2 <= C(1+‖f‖_{C^3})^{2d}` follows from (5.1) and (5.3) with no division by `k`. +- (15.2): with `t = 12k` and `w = s^2/2`, `144∫_0^∞ k^{4/3}φ_τ(12k)dk = Γ(7/6)τ^{4/3}/(24^{1/3}√π)`. Checked + numerically to relative `1e-9` in `reconciliation_check.py`, and exactly for the power bookkeeping. + +## 7. Consumption contract + +| Consumer | Consumes from D1 | After this reconciliation | +|---|---|---| +| D2 Theorem R, `frontiers/three_fronts_20260924/LIFETIME_REMAINDER.md` (blob `247b3ecf…`) | The §8 comparison `1-p_r <= Q^W(G_r^c)`, §9 (read as E2), §10, §14 (14.1), and (15.2) as `c`. **Not** (1.1). | Every consumed interface is reconciled. `claims` moves FAIL_CLOSED -> REVIEWED_SCOPED at Theorem R's stated `O(1)` scope. | +| D3 SIDE24 coefficient, `coefficients/side24_v1/PROOF.md` (blob `44b66f04…`) | (15.2) as the leading coefficient of Theorem C | The persistence interpretation is reconciled. `claims` moves HOLD_WITH_DOMAIN -> REVIEWED_SCOPED. The arithmetic acceptance (#65) is unchanged. | +| Direct lower bound, `ELDER_LOWER_AND_DENSITY_GAP.md` (E4)/(E11) | Theorem A (1.1) upper half, §§9–11 | The two-sided planar composition is now fully sourced. (E2) itself stays as reviewed in #123. | +| D4 fixed-remote (RM), RC (#110), IW (#107), #120 | P's model and observation **conventions** only, plus RM's own "Theorem A" | Unaffected. No D1 theorem is consumed. | +| Any new consumer | — | Cite the §1 identity set, this record, and a scope no larger than §2. | + +**Still not consumable.** + +- Numerical `C`, `r_*`, `z_*`, `c_{B,K}` or `c_{d,L}`. +- (1.2)'s difference rate outside compact marks. +- Any lower bound for `d >= 3`. +- A globally uniform `O(r^3)` constant over unbounded marks. +- RN, 24-jet, JETMOD or H3/LPW numerical certificates. +- `lemma_closed`, any prize, or "unconditional acceptance of the lifetime parent", which is a forbidden global + inference in `claims/LANDING_CLAIMS.json`. This acceptance is scoped. + +## 8. Independence, lineage and requests + +**Dual role.** The reconciler is also reviewer C1 of A1–A7, CAP and E2, and reviewer C2 of §§11–12. This is disclosed +rather than hidden. + +**What the reconciliation relies on, and what it does not.** Nothing here is accepted on the strength of a green test, +a hash, a same-provider review or O1. Every interface rests on a written nonauthor derivation. + +**Merge.** The register PR carrying this record must be merged by a non-Claude lane after reading it. Claude does not +self-merge. + +**Invitation.** A second-provider check is invited in this priority order: + +1. A4 and §12, which have one provider at any depth; +2. the full-depth gaps behind partial checks: A2's uniform gap, A5 for `m >= 2`, A7's division by the floor, and + §11's difference bound; +3. the reverse direction for D1-C, D1-D and D1-E, where xAI is full-depth and Claude is partial. + +Any lane may return COUNTEREXAMPLE with an exact equation. That would reopen only the affected interface and its +dependents, and the graph's reverse-impact rule would mark them REVALIDATION_REQUIRED. + +## 9. Register transitions justified by this record + +Math-, in the same PR: + +- `PROOF_INDEX.md`: D1 moves to "Reviewed scoped results" with the §2 scope. The §9 repair is recorded as reviewed by + C1 and G2. The D2 entry is updated to name its reconciled imports. +- `claims/LANDING_CLAIMS.json`: + - `lifetime-remainder` FAIL_CLOSED -> REVIEWED_SCOPED; + - `side24-coefficient` HOLD_WITH_DOMAIN -> REVIEWED_SCOPED; + - dependency reviews are bound to local review files. +- `frontiers/downstream_gate_20260925/GRAPH.json`: + - `math.uniform-matrix-cap-lifetime` AUTHOR_SIDE_CANDIDATE -> PROVED_REVIEWED, with this record as evidence and + the §2 scope. It is the only classification that satisfies a still-required premise, and D2 and D3 require it. + - D2 and D3 gain `review_disposition: ACCEPT` metadata under the existing convention (commit `cc3a991`). + - Four reading-rule component nodes (E1, E2, CAP and this record's directory) are added as `PROVED_REVIEWED` + source nodes with required edges from D1. Each carries the ledger reviews its role needs: C1 and G3 for E1 and + CAP, C1 and G2 for E2. This record is an Anthropic, nonauthor record; its W1 and radius items were raised in C1 + and G3 and its §6 is C2. OpenAI's technical check of this record (review 5345687857) is listed as author-provider + non-discharge. This closes the gap that review found: before it, E1, E2 and W1 were named only in metadata, so + editing them left D1's source snapshot unchanged. + - No node becomes `controlling`. Satisfying D2's and D3's required edge to D1 is not promotion: their own + classifications stay author-side, so `promotion_allowed` still refuses both. + - The fail-closed tests are kept on a pre-reconciliation fixture, so they still prove that an unreviewed parent + blocks both dependents. New tests make real two-commit edits and deletions of each component with P unchanged, + and require D1, D2 and D3 to be proposed `REVALIDATION_REQUIRED`. An unrelated edit must propose nothing, and + the pre-binding graph is shown to miss the component edit. + +main, in a companion PR pinned to this record's merged commit: + +- `STATUS.md`: D1 moves from AMEND/open to ACCEPT — scoped. +- The glossary's D1 row is updated. +- The museum and shop projections are regenerated. + +## 10. Checks + +`reconciliation_check.py` (Python standard library): + +1. Binds every §1 source and every local review record by Git blob, bytes and SHA256. +2. Cross-checks the hard-gate graph against `LEDGER.json`: + - D1 is bound to P's exact bytes; + - E1, E2, CAP and this directory are D1 source nodes behind required edges; + - each component node carries exactly the ledger reviews of its interfaces; + - the record's author provider differs from P's; + - two negative controls (a dropped edge; an author-only review basis) are rejected. +3. Validates `LEDGER.json`: + - every interface has at least one nonauthor ACCEPT; + - author-provider reviews are non-discharge; + - P's §§1–16 line ranges are fully covered; + - every residual item has a discharge pointer. +4. Re-verifies the reading-rule mathematics exactly: + - E1 congruence versus the displayed factor; + - (5.3), (6.1) and (6.2) on exact rational instances; + - (7.3) and the (7.5) split; + - the cap constants and κ-scaling; + - the embedding radius, the radial and lifetime ledgers, (11.1)–(11.3), the difference exponent and the §12 + integrals; + - the (13.1) coercivity bound; + - the (15.2) gamma factor, numerically. +5. Rejects nine semantic mutants. + +A green run is evidence that the bookkeeping and finite identities hold. It is not the analytic review, which lives in +C1, G1, G2, G4 and §6. diff --git a/reviews/d1_chain_reconciliation_20260928/RESULTS.json b/reviews/d1_chain_reconciliation_20260928/RESULTS.json new file mode 100644 index 000000000..e2de6c41e --- /dev/null +++ b/reviews/d1_chain_reconciliation_20260928/RESULTS.json @@ -0,0 +1,77 @@ +{ + "checks": { + "CUSTODY": { + "local_records.C1": true, + "local_records.D2": true, + "local_records.D3": true, + "local_records.G2": true, + "local_records.LOWER": true, + "local_records.LOWER_REVIEW": true, + "sources.CAP": true, + "sources.E1": true, + "sources.E2": true, + "sources.P": true + }, + "GRAPH": { + "author_only_component_review_rejected": true, + "d1_components_bound_by_required_edges": true, + "d1_components_carry_ledger_reviews": true, + "unbound_component_rejected": true + }, + "LEDGER": { + "P_and_CAP_lines_covered_exactly_once": true, + "author_only_interface_rejected": true, + "coverage_gap_rejected": true, + "discharging_provider_counts": { + "A1": 1, + "A2": 1, + "A3": 1, + "A3-E1": 2, + "A4": 1, + "A5": 1, + "A6": 2, + "A7": 1, + "CAP": 2, + "D1-A": 2, + "D1-B": 1, + "D1-B-E2": 2, + "D1-C": 1, + "D1-D": 1, + "D1-E": 1, + "S1": 2, + "S11": 1, + "S12": 1 + }, + "every_interface_has_nonauthor_full_accept": true, + "every_residual_item_discharged": true, + "every_review_is_registered": true, + "theorems_cite_known_interfaces": true + }, + "MATH": { + "6_2_extremal_equality": true, + "E1_congruence_scaled_matrix_and_det": true, + "block_determinant_5_3": true, + "canceled_pivot_6_1": true, + "cap_constants": true, + "cap_exterior_integral_9_32": true, + "cap_kappa_scaling": true, + "coefficient_factor_12_over_3_is_4": true, + "coefficient_power_bookkeeping": true, + "contact_jacobian_12_r_minus_d_plus_3": true, + "depth_failure_integral_7_3": true, + "difference_exponent_l_2_3_k_minus_5_3": true, + "displayed_factor_puts_r2_alpha_in_corner": true, + "embedding_radius_L_over_4_sqrt2": true, + "gamma_factor_15_2_numerical_1e-9": true, + "m1_far_branch_nonempty_in_majorant": true, + "m1_split_7_5": true, + "pushforward_jacobian_11_1": true, + "section12_integrals": true, + "target_coercivity_13_1": true, + "two_soft_factors_6_2": true + } + }, + "object": "D1-CHAIN-RECONCILIATION-20260928-v1", + "passed": true, + "scope": "custody, ledger rules and exact reading-rule identities; one numerical (15.2) check; not an analytic proof" +} diff --git a/reviews/d1_chain_reconciliation_20260928/SOURCE_FILES.json b/reviews/d1_chain_reconciliation_20260928/SOURCE_FILES.json new file mode 100644 index 000000000..0ade05ab9 --- /dev/null +++ b/reviews/d1_chain_reconciliation_20260928/SOURCE_FILES.json @@ -0,0 +1,42 @@ +{ + "schema": 1, + "object": "D1-CHAIN-RECONCILIATION-20260928-v1", + "effect": "REGISTER_RECONCILIATION", + "review_status": "RECONCILIATION_OF_NONAUTHOR_REVIEWS", + "reconciled_object": { + "parent": "imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md", + "parent_sha256": "9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7", + "reading_rule": [ + "imports/lifetime_parent_20260925/ERRATUM_CONGRUENCE.md", + "reviews/d1_section9_borel_repair_20260925/REPAIR.md", + "RECONCILIATION.md section 5 (W1, embedding radius)" + ], + "base_commit": "d39dbbc25c25a7bc3f6c15b21f957a7fcac30615" + }, + "files": [ + { + "path": "RECONCILIATION.md", + "bytes": 23312, + "sha256": "451b9d7ffee072a73fc904cab891b6693e3f233808b89df10cce1b57036b65da", + "git_blob": "75da2597971510f843f8d90c743950cb8c177342" + }, + { + "path": "LEDGER.json", + "bytes": 12545, + "sha256": "5d39b07556fd356344b6e5d576acabbcd5e67c6dcc8da0bb26c1bb2cac0c591f", + "git_blob": "f6c329fb0f21a6cc2cc690240e86aa0a86114d4e" + }, + { + "path": "reconciliation_check.py", + "bytes": 23779, + "sha256": "c83b7c04217259e8c9bcd5ffda9c4bc259d09fc558a4a6ef78632ae4bd41d814", + "git_blob": "c2f413e47feef42d57034685b1f504dd48ed2ed3" + }, + { + "path": "RESULTS.json", + "bytes": 2387, + "sha256": "1d01d2afe9881a4a9ba04c6ba3cb9da6f3284f06a7952ece1a45baeac9f469ca", + "git_blob": "e2de6c41e87ce64196dfbe5077ead2f09d87b367" + } + ] +} diff --git a/reviews/d1_chain_reconciliation_20260928/reconciliation_check.py b/reviews/d1_chain_reconciliation_20260928/reconciliation_check.py new file mode 100644 index 000000000..c2f413e47 --- /dev/null +++ b/reviews/d1_chain_reconciliation_20260928/reconciliation_check.py @@ -0,0 +1,478 @@ +"""Checks for the D1 chain reconciliation (D1-CHAIN-RECONCILIATION-20260928-v1). + +Python standard library only. Exact rational arithmetic, except one clearly labelled numerical check of (15.2). +Run from the repository root or from this directory. Groups: + + CUSTODY every bound source and local review record matches its Git blob, byte count and SHA256. + GRAPH the hard-gate graph binds P, E1, E2, CAP and this record as D1 source nodes joined by required edges, + and each component node carries exactly the ledger reviews its role needs. Two negative controls. + LEDGER every interface has a full-depth ACCEPT from a nonauthor provider; author-provider reviews never + discharge; P and CAP line ranges are covered exactly; every theorem cites accepted interfaces; every + residual item is discharged. Two synthetic negative controls must be rejected. + MATH the reading-rule mathematics: erratum E1 versus the displayed factor; (5.3); (6.1) and (6.2), including + the extremal equality case; (7.3); the (7.5) split and its nonempty far branch; the cap constants and + kappa-scaling; the embedding radius; the radial ledger and |det T_r|; (11.1)-(11.3) and the difference + exponent; the section 12 integrals; (13.1); and (15.2), numerically. + +Not an analytic proof: the reviews C1, G1, G2, G4 and RECONCILIATION.md section 6 carry the arguments. +""" +import argparse +import hashlib +import json +import math +import random +import sys +from fractions import Fraction as F +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +MUTANTS = ("allow-author-review", "skip-coverage", "displayed-congruence", "drop-mixed-square", + "drop-far-branch", "embedding-radius", "difference-exponent", "gamma-24", "unbind-component") +GRAPH_PATH = ROOT / "frontiers" / "downstream_gate_20260925" / "GRAPH.json" +D1_NODE = "math.uniform-matrix-cap-lifetime" +RECORD_DIR = "reviews/d1_chain_reconciliation_20260928/" +# Ledger source key -> (component role, ledger interfaces the component node must carry). +COMPONENTS = {"E1": ("amendment", ["A3-E1"]), "E2": ("amendment", ["D1-B-E2"]), + "CAP": ("deterministic_support", ["CAP"])} +RECORD_ITEMS = ["S11", "S12", "R-W1", "R-embedding-radius"] + + +# --------------------------------------------------------------------------------------------------------------- +# Custody +# --------------------------------------------------------------------------------------------------------------- + +def git_blob(data): + return hashlib.sha1(b"blob %d\0" % len(data) + data).hexdigest() + + +def identity_ok(rec): + data = (ROOT / rec["path"]).read_bytes() + ok = (len(data) == rec["bytes"] and hashlib.sha256(data).hexdigest() == rec["sha256"] + and git_blob(data) == rec["git_blob"]) + if "lines" in rec: + ok &= data.decode("utf-8").count("\n") == rec["lines"] + return ok + + +def check_custody(ledger): + out = {} + for group in ("sources", "local_records"): + for key, rec in ledger[group].items(): + out[f"{group}.{key}"] = identity_ok(rec) + return out + + +# --------------------------------------------------------------------------------------------------------------- +# Ledger rules +# --------------------------------------------------------------------------------------------------------------- + +def discharging(ledger, iface, mut): + authors = set(ledger["author_providers"]) + provs = set() + for rv in iface["reviews"]: + prov = ledger["reviews"][rv["by"]]["provider"] + if rv["verdict"] != "ACCEPT" or rv["depth"] != "full": + continue + if prov in authors and mut != "allow-author-review": + continue + provs.add(prov) + return provs + + +def coverage_ok(ledger, mut): + if mut == "skip-coverage": + return True + for src in ("P", "CAP"): + n = ledger["sources"][src]["lines"] + hit = [0] * (n + 1) + for iface in ledger["interfaces"]: + if iface["source"] == src: + for a, b in iface["lines"]: + for i in range(a, b + 1): + hit[i] += 1 + for m in ledger["meta_ranges"].get(src, []): + a, b = m["lines"] + for i in range(a, b + 1): + hit[i] += 1 + if any(h != 1 for h in hit[1:]): + return False + return True + + +def ledger_rules(ledger, mut): + ids = {i["id"] for i in ledger["interfaces"]} + every_discharged = all(discharging(ledger, i, mut) for i in ledger["interfaces"]) + theorems_ok = all(set(v) <= ids for v in ledger["theorems"].values()) + residual_ok = all(r["status"] == "DISCHARGED" and r["discharged_by"] and + all(d in ids or d.startswith("RECONCILIATION.md") for d in r["discharged_by"]) + for r in ledger["residual_items"]) + reviews_known = all(rv["by"] in ledger["reviews"] for i in ledger["interfaces"] for rv in i["reviews"]) + return every_discharged, coverage_ok(ledger, mut), theorems_ok, residual_ok, reviews_known + + +def check_ledger(ledger, mut): + out = {} + d, c, t, r, k = ledger_rules(ledger, mut) + out["every_interface_has_nonauthor_full_accept"] = d + out["P_and_CAP_lines_covered_exactly_once"] = c + out["theorems_cite_known_interfaces"] = t + out["every_residual_item_discharged"] = r + out["every_review_is_registered"] = k + # Negative control 1: an interface whose only ACCEPT is by the author provider must not be discharged. + neg = json.loads(json.dumps(ledger)) + neg["interfaces"].append({"id": "NEG", "source": "E1", "lines": "all", "component": "x", "claim": "x", + "reviews": [{"by": "O1", "verdict": "ACCEPT", "depth": "full"}]}) + out["author_only_interface_rejected"] = not ledger_rules(neg, mut)[0] + # Negative control 2: removing the section 11 interface must break coverage. + neg2 = json.loads(json.dumps(ledger)) + neg2["interfaces"] = [i for i in neg2["interfaces"] if i["id"] != "S11"] + out["coverage_gap_rejected"] = not ledger_rules(neg2, mut)[1] + # Provider counts: the providers that discharge each interface (reported, not asserted beyond >= 1). + out["discharging_provider_counts"] = {i["id"]: len(discharging(ledger, i, None)) for i in ledger["interfaces"]} + return out + + +# --------------------------------------------------------------------------------------------------------------- +# Graph binding of the reading rule +# --------------------------------------------------------------------------------------------------------------- + +def graph_rules(graph, ledger, mut): + """(bound, reviewed): every reading-rule component is a D1 source node behind a required edge, and each + component node carries exactly the ledger reviews that its role needs.""" + nodes, edges = graph["nodes"], graph["edges"] + authors = set(ledger["author_providers"]) + ifaces = {i["id"]: i for i in ledger["interfaces"]} + residual = {r["id"]: r for r in ledger["residual_items"]} + required = {e["to"] for e in edges if e["from"] == D1_NODE and e["required"] is True} + if mut == "unbind-component": + required = set(nodes) + by_source = {n.get("source"): (nid, n) for nid, n in nodes.items()} + d1, P = nodes.get(D1_NODE, {}), ledger["sources"]["P"] + bound = (d1.get("source") == P["path"] and d1.get("fingerprint") == P["sha256"] + and d1.get("classification") == "PROVED_REVIEWED" and d1.get("controlling") is False) + reviewed = True + component_ids = [] + for key, (role, items) in COMPONENTS.items(): + src = ledger["sources"][key] + nid, node = by_source.get(src["path"], (None, {})) + component_ids.append(nid) + bound &= nid in required and node.get("fingerprint") == src["sha256"] and node.get("component_of") == D1_NODE + want = sorted((rv["by"], ledger["reviews"][rv["by"]]["provider"], rv["verdict"], rv["depth"]) + for it in items for rv in ifaces[it]["reviews"]) + have = sorted((b.get("review"), b.get("provider"), b.get("verdict"), b.get("depth")) + for b in node.get("review_basis", [])) + reviewed &= (node.get("classification") == "PROVED_REVIEWED" and node.get("controlling") is False + and node.get("component_role") == role and node.get("ledger_items") == items + and node.get("author_provider") in authors and want == have + and all(discharging(ledger, ifaces[it], mut) for it in items)) + nid, node = by_source.get(RECORD_DIR, (None, {})) + component_ids.append(nid) + bound &= nid in required and node.get("component_of") == D1_NODE + raised = [ledger["reviews"][residual[i]["raised_in"].split()[0]]["provider"] for i in RECORD_ITEMS if i in residual] + reviewed &= (node.get("classification") == "PROVED_REVIEWED" and node.get("controlling") is False + and node.get("component_role") == "reading_rule_record" and node.get("ledger_items") == RECORD_ITEMS + and node.get("author_provider") not in authors + and all(discharging(ledger, ifaces[i], mut) for i in RECORD_ITEMS if i in ifaces) + and all(residual[i]["status"] == "DISCHARGED" for i in RECORD_ITEMS if i in residual) + and len(raised) == 2 and not set(raised) & authors + and bool(node.get("technical_checks_non_discharge")) + and all(c.get("provider") in authors for c in node["technical_checks_non_discharge"]) + and not any({b.get("provider"), b.get("raised_by_provider")} & authors + for b in node.get("review_basis", []))) + bound &= sorted(d1.get("reading_rule", [])) == sorted(x for x in component_ids if x) + dependents = {e["from"] for e in edges if e["to"] == D1_NODE and e["required"] is True} + bound &= {"math.lifetime-remainder", "math.side24-coefficient"} <= dependents + return bound, reviewed + + +def check_graph(ledger, mut): + graph = json.loads(GRAPH_PATH.read_text()) + out = {} + b, r = graph_rules(graph, ledger, mut) + out["d1_components_bound_by_required_edges"] = b + out["d1_components_carry_ledger_reviews"] = r + e1_id = next(nid for nid, n in graph["nodes"].items() if n.get("source") == ledger["sources"]["E1"]["path"]) + # Negative control 3: without the required edge D1 -> erratum node, the binding must be rejected. + neg = json.loads(json.dumps(graph)) + neg["edges"] = [e for e in neg["edges"] if not (e["from"] == D1_NODE and e["to"] == e1_id)] + out["unbound_component_rejected"] = not graph_rules(neg, ledger, mut)[0] + # Negative control 4: an erratum node whose review basis is only the author provider's review must fail. + neg2 = json.loads(json.dumps(graph)) + neg2["nodes"][e1_id]["review_basis"] = [{"review": "O1", "provider": "OpenAI", "verdict": "ACCEPT", "depth": "full"}] + out["author_only_component_review_rejected"] = not graph_rules(neg2, ledger, mut)[1] + return out + + +# --------------------------------------------------------------------------------------------------------------- +# Exact linear algebra helpers +# --------------------------------------------------------------------------------------------------------------- + +def det(A): + n = len(A) + M = [list(r) for r in A] + d = F(1) + for c in range(n): + p = next((i for i in range(c, n) if M[i][c] != 0), None) + if p is None: + return F(0) + if p != c: + M[c], M[p] = M[p], M[c] + d = -d + d *= M[c][c] + for i in range(c + 1, n): + f = M[i][c] / M[c][c] + M[i] = [x - f * y for x, y in zip(M[i], M[c])] + return d + + +def adj(A): + n = len(A) + if n == 1: + return [[F(1)]] + C = [[F(0)] * n for _ in range(n)] + for i in range(n): + for j in range(n): + minor = [r[:j] + r[j + 1:] for k, r in enumerate(A) if k != i] + C[j][i] = (-1) ** (i + j) * det(minor) + return C + + +def matmul(A, B): + return [[sum(A[i][k] * B[k][j] for k in range(len(B))) for j in range(len(B[0]))] for i in range(len(A))] + + +def transpose(A): + return [list(r) for r in zip(*A)] + + +def solve_inv(A): + n = len(A) + M = [list(A[i]) + [F(int(i == j)) for j in range(n)] for i in range(n)] + for c in range(n): + p = next(i for i in range(c, n) if M[i][c] != 0) + M[c], M[p] = M[p], M[c] + pv = M[c][c] + M[c] = [x / pv for x in M[c]] + for i in range(n): + if i != c and M[i][c] != 0: + f = M[i][c] + M[i] = [x - f * y for x, y in zip(M[i], M[c])] + return [r[n:] for r in M] + + +def rational_orthogonal(rng, m): + """Cayley transform of a random rational skew matrix: an exactly orthogonal rational matrix.""" + S = [[F(0)] * m for _ in range(m)] + for i in range(m): + for j in range(i + 1, m): + v = F(rng.randrange(-5, 6), rng.randrange(1, 5)) + S[i][j], S[j][i] = v, -v + I = [[F(int(i == j)) for j in range(m)] for i in range(m)] + IminusS = [[I[i][j] - S[i][j] for j in range(m)] for i in range(m)] + IplusS = [[I[i][j] + S[i][j] for j in range(m)] for i in range(m)] + return matmul(solve_inv(IminusS), IplusS) + + +def block(alpha, beta, A): + m = len(A) + return [[alpha] + list(beta)] + [[beta[i]] + list(A[i]) for i in range(m)] + + +# --------------------------------------------------------------------------------------------------------------- +# Mathematics +# --------------------------------------------------------------------------------------------------------------- + +def check_math(mut): + rng = random.Random(63) + out = {} + # E1 and (5.3): H = [[r a, r b^T],[r b, A]], r = s^2. + ok_e1, ok_53, ok_old_singular = True, True, True + for _ in range(90): + m = rng.choice((1, 2, 3)) + s = F(rng.randrange(1, 30), 31) + r = s * s + a = F(rng.randrange(-9, 10), rng.randrange(1, 4)) + b = [F(rng.randrange(-9, 10), rng.randrange(1, 4)) for _ in range(m)] + A = [[F(0)] * m for _ in range(m)] + for i in range(m): + for j in range(i, m): + A[i][j] = A[j][i] = F(rng.randrange(-9, 10), rng.randrange(1, 4)) + H = block(r * a, [r * x for x in b], A) + d = F(1) / s if mut != "displayed-congruence" else s + D = [[d if (i == j == 0) else F(int(i == j)) for j in range(m + 1)] for i in range(m + 1)] + K = matmul(matmul(D, H), D) + ok_e1 &= K == block(a, [s * x for x in b], A) and det(K) == det(H) / r + adjA = adj(A) + quad = sum(b[i] * adjA[i][j] * b[j] for i in range(m) for j in range(m)) + ok_53 &= det(H) == r * (a * det(A) - r * quad) + Dold = [[s if (i == j == 0) else F(int(i == j)) for j in range(m + 1)] for i in range(m + 1)] + ok_old_singular &= matmul(matmul(Dold, H), Dold)[0][0] == r * r * a + out["E1_congruence_scaled_matrix_and_det"] = ok_e1 + out["block_determinant_5_3"] = ok_53 + out["displayed_factor_puts_r2_alpha_in_corner"] = ok_old_singular + # (6.1) and (6.2) on exact instances with rational spectra, plus the extremal equality case. + ok61, ok62, eq62 = True, True, True + c32 = F(1) if mut == "drop-mixed-square" else F(3, 2) + for trial in range(120): + m = rng.choice((1, 2, 3)) + Q = rational_orthogonal(rng, m) + lam = sorted(F(rng.randrange(1, 40), rng.randrange(1, 6)) for _ in range(m)) + B = matmul(matmul(Q, [[lam[i] if i == j else F(0) for j in range(m)] for i in range(m)]), transpose(Q)) + AM = [[-x for x in row] for row in B] + h = F(rng.randrange(1, 30), rng.randrange(1, 4)) + r = F(1, rng.randrange(2, 60)) + # maximum endpoint: alpha < 0, ||beta||^2 <= h^2/4, H_M < 0 + aM = -F(rng.randrange(1, 100), 100) * h / 2 + bM = [F(rng.randrange(-10, 11), 20) * h / 2 / m for _ in range(m)] + HM = block(r * aM, [r * x for x in bM], AM) + negdef = all(det([row[:k] for row in [[-x for x in rr] for rr in HM][:k]]) > 0 for k in range(1, m + 2)) + if negdef: + ok61 &= abs(det(HM)) <= r * (h / 2) * det(B) + # saddle endpoint: ||A_S - A_M||_F <= r h (Frobenius dominates the operator norm) + extremal = trial % 3 == 0 + if extremal: + AS = [[-(B[i][j] + (r * h if i == j else 0)) for j in range(m)] for i in range(m)] + aS = h / 2 + v1 = [Q[i][0] for i in range(m)] + bS = [h / 2 * x for x in v1] + else: + E = [[F(0)] * m for _ in range(m)] + for i in range(m): + for j in range(i, m): + E[i][j] = E[j][i] = F(rng.randrange(-10, 11), 10 * m * m) * r * h + AS = [[AM[i][j] + E[i][j] for j in range(m)] for i in range(m)] + aS = F(rng.randrange(-100, 101), 100) * h / 2 + bS = [F(rng.randrange(-10, 11), 20) * h / 2 / m for _ in range(m)] + HS = block(r * aS, [r * x for x in bS], AS) + bound = r * (h / 2) * (lam[0] + c32 * r * h) + for j in range(1, m): + bound *= lam[j] + r * h + ok62 &= abs(det(HS)) <= bound + if extremal: + eq62 &= abs(det(HS)) == r * (h / 2) * (lam[0] + F(3, 2) * r * h) * math.prod( + [lam[j] + r * h for j in range(1, m)], start=F(1)) + out["canceled_pivot_6_1"] = ok61 + out["two_soft_factors_6_2"] = ok62 + out["6_2_extremal_equality"] = eq62 + # (7.3) identity. + ok73 = True + for _ in range(40): + Dc, Ec, Uc, r = (F(rng.randrange(1, 20), rng.randrange(1, 5)) for _ in range(4)) + top = Dc * r * Uc ** 2 + lhs = top ** 3 / 3 + Ec * r * Uc * top ** 2 / 2 + ok73 &= lhs == r ** 3 * (Dc ** 3 / 3 * Uc ** 6 + Ec * Dc ** 2 / 2 * Uc ** 5) + out["depth_failure_integral_7_3"] = ok73 + # (7.5): majorant event {lam <= Dr (J+lam)^2} lies in {lam <= 4DrJ^2} or {lam > 1/(4Dr)}; far part nonempty. + ok75, far_nonempty = True, True + for _ in range(400): + Dr = F(1, rng.randrange(2, 400)) + J = F(rng.randrange(10, 60), 10) + lam = F(rng.randrange(1, 4000), rng.randrange(1, 40)) + if lam <= Dr * (J + lam) ** 2: + near = lam <= 4 * Dr * J ** 2 + far = lam > 1 / (4 * Dr) + ok75 &= near or (far and mut != "drop-far-branch") + big = 1 / Dr + F(rng.randrange(0, 100)) + far_nonempty &= big <= Dr * (J + big) ** 2 + out["m1_split_7_5"] = ok75 + out["m1_far_branch_nonempty_in_majorant"] = far_nonempty + # Cap constants and kappa-scaling (normalized kappa = 1/6: lambda > 8 r m^2, r n <= 1/20). + u = F(2, 11) + F(2, 121) + mu = F(48, 121) + out["cap_constants"] = (u == F(24, 121) and (1 + F(6, 11) + F(5, 121)) / 4 == mu + and mu * (3 + 3 * u + u * u) == F(2554128, 1771561) + and F(7, 4) - F(2554128, 1771561) == F(2184415, 7086244) > F(1, 4) + and F(9, 32) - F(1, 6) == F(11, 96) + and F(22, 2) * F(20, 11) ** 2 == F(4400, 121) > F(1, 6)) + kappa = F(1, 6) + out["cap_kappa_scaling"] = (8 * 6 * kappa / (36 * kappa ** 2) == F(4) / (3 * kappa) + and 6 * kappa / 20 == 3 * kappa / 10 == F(1, 20)) + # Exterior integral of (x-a)(x-c)/8 from -2r to a (r = 1): 9/32. + xs = lambda x: x ** 3 / 3 - x / 4 + out["cap_exterior_integral_9_32"] = (xs(F(-1, 2)) - xs(F(-2))) / 8 == F(9, 32) + # Embedding radius: D = [-2r,2r] x B(0,2r) has max squared norm 8 r^2; embedded iff 8 r^2 < L^2/4. + ok_emb = True + for L in (F(1), F(24), F(7, 3)): + for num in range(1, 60): + r = L * F(num, 200) + embedded = 8 * r * r < L * L / 4 + claimed = (r * r < L * L / 32) if mut != "embedding-radius" else (r < L / 4) + ok_emb &= embedded == claimed + out["embedding_radius_L_over_4_sqrt2"] = ok_emb + # Radial ledger: |det T_r| = 12 r^-(d+3) and exponent (d-1)+3-(d+3)+2 = 1. + ok_T = True + for r in (F(1, 3), F(2, 7), F(1, 11)): + a, c = -r / 2, r / 2 + # rows of U0..U3 on (f(a), f_x(a), f(c), f_x(c)) + T = [[F(1, 2), 0, F(1, 2), 0], [-1 / r, 0, 1 / r, 0], [0, -1 / r, 0, 1 / r], + [F(12) / r ** 3, 6 / r ** 2, -F(12) / r ** 3, 6 / r ** 2]] + T = [[F(x) for x in row] for row in T] + ok_T &= abs(det(T)) == 12 / r ** 4 and abs(det([[F(1, 2), F(1, 2)], [-1 / r, 1 / r]])) == 1 / r + out["contact_jacobian_12_r_minus_d_plus_3"] = ok_T and all((d - 1) + 3 - (d + 3) + 2 == 1 for d in range(2, 12)) + # (11.1): with k = a^3 and l = k r^3, r dr/dl = 1/(3 k r) = (1/3) k^(-2/3) l^(-1/3). + ok111 = True + for _ in range(40): + a = F(rng.randrange(1, 9), rng.randrange(1, 9)) + k, r = a ** 3, F(rng.randrange(1, 50), 100) + l13 = a * r # l^(1/3) + ok111 &= r / (3 * k * r * r) == F(1, 3) / (a * a) / l13 + out["pushforward_jacobian_11_1"] = ok111 + out["coefficient_factor_12_over_3_is_4"] = F(12, 3) == 4 + le, ke = F(-1, 3) + 1, F(-2, 3) - (0 if mut == "difference-exponent" else 1) + out["difference_exponent_l_2_3_k_minus_5_3"] = (le, ke) == (F(2, 3), F(-5, 3)) + # Section 12: integral_0^t l^p = t^(p+1)/(p+1) for p > -1. + out["section12_integrals"] = (1 / (F(-1, 3) + 1) == F(3, 2) and 1 / (F(2, 3) + 1) == F(3, 5) + and all(F(q) - F(1, 3) + 1 == F(q) + F(2, 3) for q in range(-0, 5)) + and all(F(q) + F(2, 3) + 1 == F(q) + F(5, 3) for q in range(0, 5))) + # (13.1): (b - k r^3/2)^2 + 144 k^2 >= (b^2 + k^2)/2 for 0 < r <= 1. + ok131 = True + for _ in range(500): + b = F(rng.randrange(-400, 401), rng.randrange(1, 9)) + k = F(rng.randrange(0, 400), rng.randrange(1, 9)) + r = F(rng.randrange(1, 101), 100) + ok131 &= (b - k * r ** 3 / 2) ** 2 + 144 * k * k >= (b * b + k * k) / 2 + out["target_coercivity_13_1"] = ok131 + # (15.2) gamma factor, numerical (float): 144 int_0^inf k^(4/3) phi_tau(12k) dk. + ok152 = True + for tau in (0.5, 1.0, 2.5): + # substitute t = 12k = u^3: integrand becomes 12^(-1/3) * 3 u^6 phi_tau(u^3), smooth at 0. + n, top = 20000, (12.0 * tau) ** (1.0 / 3.0) + hh = top / n + f = lambda uu: 3 * uu ** 6 * math.exp(-uu ** 6 / (2 * tau * tau)) / (tau * math.sqrt(2 * math.pi)) + simpson = f(0) + f(top) + sum((4 if i % 2 else 2) * f(i * hh) for i in range(1, n)) + val = 12 ** (-1.0 / 3.0) * simpson * hh / 3 + base = 12 if mut == "gamma-24" else 24 + closed = math.gamma(7 / 6) * tau ** (4 / 3) / (base ** (1 / 3) * math.sqrt(math.pi)) + ok152 &= abs(val - closed) <= 1e-9 * closed + out["gamma_factor_15_2_numerical_1e-9"] = ok152 + out["coefficient_power_bookkeeping"] = 4 * 36 == 144 and F(-2, 3) + 2 == F(4, 3) + return out + + +def flatten(d): + for k, v in d.items(): + if isinstance(v, dict): + if k != "discharging_provider_counts": + yield from flatten(v) + else: + yield v + + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument("--mutant", choices=MUTANTS) + mut = ap.parse_args().mutant + ledger = json.loads((HERE / "LEDGER.json").read_text()) + checks = {"CUSTODY": check_custody(ledger), "GRAPH": check_graph(ledger, mut), "LEDGER": check_ledger(ledger, mut), + "MATH": check_math(mut)} + passed = all(flatten(checks)) + print(json.dumps({"checks": checks, "object": ledger["object"], "passed": passed, + "scope": "custody, ledger rules and exact reading-rule identities; one numerical (15.2) check; " + "not an analytic proof"}, + indent=2, sort_keys=True)) + return 0 if passed else 1 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/tests/test_landing_claims_check.py b/tests/test_landing_claims_check.py index 8ade377dd..df095dae2 100644 --- a/tests/test_landing_claims_check.py +++ b/tests/test_landing_claims_check.py @@ -99,6 +99,20 @@ def test_closed_or_stale_queue_link_is_rejected(self): with self.assertRaisesRegex(check.ClaimManifestError, "Work queue"): check.validate_manifest(self.manifest(), (self.root / "README.md").read_text()) + def test_closed_queue_record_requires_matching_label(self): + manifest = self.manifest() + manifest["live_queue"]["required_state"] = "closed" + with self.assertRaisesRegex(check.ClaimManifestError, "closed-record label"): + check.validate_manifest(manifest, (self.root / "README.md").read_text()) + landing = (self.root / "README.md").read_text().replace( + f"[Work queue]({self.queue_url})", + f"[Work queue]({self.queue_url}) {check.CLOSED_QUEUE_LABEL}", + ) + report = check.validate_manifest(manifest, landing) + self.assertEqual(report["live_queue"]["required_state"], "closed") + with self.assertRaisesRegex(check.ClaimManifestError, "closed-record label"): + check.validate_manifest(self.manifest(), landing) + def test_unmanifested_landing_claim_is_rejected(self): (self.root / "frontiers" / "b").mkdir() (self.root / "frontiers" / "b" / "PROOF.md").write_text("# B\n") diff --git a/tools/landing_claims_check.py b/tools/landing_claims_check.py index 5accfba5d..c66fde7a5 100644 --- a/tools/landing_claims_check.py +++ b/tools/landing_claims_check.py @@ -112,6 +112,9 @@ def landing_result_paths(text: str) -> set[str]: } +CLOSED_QUEUE_LABEL = "*(closed downstream record; not a live queue)*" + + def landing_work_queue(text: str) -> str: match = re.search(r"\[Work queue\]\(([^)]+)\)", text) if not match: @@ -119,6 +122,11 @@ def landing_work_queue(text: str) -> str: return match.group(1) +def landing_queue_marked_closed(text: str) -> bool: + match = re.search(r"\[Work queue\]\([^)]+\)[ \t]*(\S.*)?$", text, re.MULTILINE) + return bool(match and match.group(1) and match.group(1).startswith(CLOSED_QUEUE_LABEL)) + + def _validate_review(review: dict) -> None: if not isinstance(review, dict) or review.get("kind") not in {"github_issue", "local_file"}: raise ClaimManifestError("review must be github_issue or local_file") @@ -230,10 +238,12 @@ def validate_manifest(manifest: dict, landing_text: str) -> dict: queue = manifest.get("live_queue") if not isinstance(queue, dict): raise ClaimManifestError("live_queue object required") - if type(queue.get("issue")) is not int or queue.get("required_state") != "open": - raise ClaimManifestError("live_queue requires integer issue and required_state=open") + if type(queue.get("issue")) is not int or queue.get("required_state") not in {"open", "closed"}: + raise ClaimManifestError("live_queue requires integer issue and required_state open or closed") if landing_work_queue(landing_text) != queue.get("url"): raise ClaimManifestError("README Work queue does not match manifest live_queue") + if (queue["required_state"] == "closed") != landing_queue_marked_closed(landing_text): + raise ClaimManifestError("README Work queue closed-record label does not match required_state") if unresolved_positive: raise ClaimManifestError( "positive disposition depends on unresolved external source: "