Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
116 commits
Select commit Hold shift + click to select a range
49cbb1d
Record exact kernel closure, federation discovery and recovery evidence
codex Oct 29, 2026
63df78d
Admit verified source census and exact kernel evidence bindings
codex Oct 29, 2026
9474766
Merge remote-tracking branch 'origin/main' into cbz/foundation-handof…
codex Oct 29, 2026
f36f355
fix(cbz): bind RF312 effective file hashes to checked Git source
codex Oct 29, 2026
70c5967
Record verified RF312 source-map repair and review disposition
codex Oct 29, 2026
8c94382
Preserve PR evidence with checked source identities and optimized val…
codex Oct 29, 2026
aecf894
feat(cbz): bind normalized replay observations to exact source and ra…
codex Oct 29, 2026
3faed44
Merge remote-tracking branch 'origin/main' into cbz/foundation-handof…
codex Oct 29, 2026
3ccd631
Index 367 context-bound kernel records and 184 exact quarantines
codex Oct 29, 2026
26ba25b
Merge branch 'cbz/foundation-handoff-20261029' into cbz/terminal-obli…
codex Oct 29, 2026
66c54f8
Remove superseded review gates from active agent instructions
codex Oct 29, 2026
a4a466c
Add failing cold-start Node fixture and execution contracts
d6g8k5htny-coder Oct 29, 2026
deba06f
Prepare exact historical Node fixtures and reject incomplete regressions
d6g8k5htny-coder Oct 29, 2026
b3eacf7
Bind Node source and mutation harness controls to real unsafe changes
d6g8k5htny-coder Oct 29, 2026
938c028
Document cold bootstrap and test hostile ambient Git and Node options
d6g8k5htny-coder Oct 29, 2026
6ee0918
Expose mutable Node fixtures and imported source custody defects
d6g8k5htny-coder Oct 29, 2026
c1d8b64
Bind imported Node helper code and verify complete fixture postflight
d6g8k5htny-coder Oct 29, 2026
5ea29f2
Run both Node auditor modes and prepared suite in one bounded job
d6g8k5htny-coder Oct 29, 2026
8cde04a
Use available ARM runner and record actual Node test runtime
d6g8k5htny-coder Oct 29, 2026
dba9a9e
Preserve bound original Node transcript through native console transport
d6g8k5htny-coder Oct 29, 2026
f2d242e
Preserve current cold-start Node observations and transcript
d6g8k5htny-coder Oct 29, 2026
cec14a7
State the remaining mutation-evidence limitation
d6g8k5htny-coder Oct 29, 2026
143736b
Capture reason-specific mutation assertion diagnostics
d6g8k5htny-coder Oct 29, 2026
ee5f03d
Bind Node source mutations to specific control observations
d6g8k5htny-coder Oct 29, 2026
f4ad0f4
Exercise mutation-receipt subject, nonce and event guards
d6g8k5htny-coder Oct 29, 2026
5bd0e97
Tighten control observations and run on standard hosted workers
d6g8k5htny-coder Oct 29, 2026
2db895e
Run strengthened controls on the observed hosted runner
d6g8k5htny-coder Oct 29, 2026
554c3fa
Preserve reason-bound Node regression evidence
d6g8k5htny-coder Oct 29, 2026
4f35e5b
Record stronger source-bound mutation and Node observations
d6g8k5htny-coder Oct 29, 2026
fc9e90d
Add reproducible pinned-fixture Node regression
d6g8k5htny-coder Oct 29, 2026
e77502d
Expose mixed expected and foreign mutation failures
d6g8k5htny-coder Oct 29, 2026
2620366
Retain additional abnormal-outcome mutation controls
d6g8k5htny-coder Oct 29, 2026
05343dc
Require coherent mutation failure counts
d6g8k5htny-coder Oct 29, 2026
db7d4a9
Reject mixed and incomplete mutation-test outcomes
d6g8k5htny-coder Oct 29, 2026
69413c7
Check fixture bypass receipts require a successful Node child
d6g8k5htny-coder Oct 29, 2026
f26e91b
Expose poisoned cached museum-module execution
d6g8k5htny-coder Oct 29, 2026
3598f41
Expose poisoned runner bytecode in the test loader
d6g8k5htny-coder Oct 29, 2026
8aa7d35
Bind mutation observations and execute museum source directly
d6g8k5htny-coder Oct 29, 2026
f1f2c79
Preserve the poisoned test-loader adverse observation
d6g8k5htny-coder Oct 29, 2026
dc49a74
Preserve the source-only regression qualification
d6g8k5htny-coder Oct 29, 2026
0a307e6
Test further Node mutation-observation boundaries
d6g8k5htny-coder Oct 29, 2026
1c776e6
Specify source-only child test process observation
d6g8k5htny-coder Oct 29, 2026
1033ea6
Specify poisoned outer-control import defenses
d6g8k5htny-coder Oct 29, 2026
23a7a5a
Specify nonempty exercised outer control suite
d6g8k5htny-coder Oct 29, 2026
3d7be90
Isolate Node controls and tighten mutation observations
d6g8k5htny-coder Oct 29, 2026
9651b9c
Keep poison fixtures valid under private cache prefixes
d6g8k5htny-coder Oct 29, 2026
15e8f68
cbz: add a mutation-tested federation drift crawler (CBZ-0 addendum, G7)
claude Oct 29, 2026
f2d2780
CBZ-0 G12: empirical statement check for core-Lean arithmetic skeleto…
claude Oct 29, 2026
0768d66
ci: run federation drift on every pull request
d6g8k5htny-coder Oct 30, 2026
fe676eb
fix(cbz): block missing declared canonical inputs
d6g8k5htny-coder Oct 30, 2026
4435db8
cbz_drift: close the repository graph and refresh tips (#712 R1, R4; R2)
claude Oct 30, 2026
e666f48
cbz_drift: block git lake packages without a usable revision or URL (…
claude Oct 30, 2026
9050366
cbz_drift: scope-aware Lean interfaces (#712 repair slice B, C1 to C4)
claude Oct 30, 2026
23aa521
cbz_drift: only a full commit id pins a lake package; unreadable pack…
claude Oct 31, 2026
e12ddf7
ci: run every drift test module in the hosted self-test (#723 requali…
claude Oct 31, 2026
da5ff07
cbz_drift: restore slice B's five evidence logs named by its README
claude Oct 31, 2026
fcbbd06
G12: Int / and % follow Lean core Int.ediv/Int.emod (Euclidean, total…
claude Oct 31, 2026
30fd5dc
Merge main 4712fc13 into the G12 branch (base refresh)
claude Oct 31, 2026
28e3629
G12 evidence: runs at main 4712fc13 and Math- 19a55750; README record…
claude Oct 31, 2026
b9f118c
fix(cbz): repair the node-regression test imports and nested-output k…
claude Oct 31, 2026
408abd9
ci(node-status): trigger the freshness checks on their remaining inputs
claude Oct 31, 2026
58099d2
Merge main (3dc63c7d) into #707 after applying the reviewed test patch
claude Oct 31, 2026
ce806f1
Integrate the drift crawler stack #712, #716, #723 and #725 (da5ff070)
claude Oct 31, 2026
5ec42c1
cbz(G12): infer a finite domain from a bound only for an explicit Nat…
claude Oct 31, 2026
fbd8409
G12 evidence: regenerate the three runs after the bound-domain follow…
claude Oct 31, 2026
d235607
G12 evidence: record the Math- package root as the archive cut, not a…
claude Oct 31, 2026
0985ed2
Integrate #715: per-PR federation drift, composed with the crawler stack
claude Oct 31, 2026
8e93ba9
Integrate CBZ-0 runbook batch 2: federation drift crawler (#712 stack…
d6g8k5htny-coder Oct 31, 2026
1e307de
Merge branch 'main' into claude/cbz0-g12-statement-fuzz-20261029
d6g8k5htny-coder Oct 31, 2026
d0d384b
Merge pull request #726 from d6g8k5htny-coder/claude/cbz0-g12-stateme…
d6g8k5htny-coder Oct 31, 2026
b0e0c6f
Tip-sync #707 onto main d0d384b1 (merge commit; prior head 58099d2c)
claude Oct 31, 2026
7500d43
Merge pull request #707: bind prepared Node regression to source byte…
d6g8k5htny-coder Oct 31, 2026
03a2eeb
cbz_drift: count Lean files under evidence directories, do not compar…
claude Oct 31, 2026
f3f1b51
Merge pull request #736 from d6g8k5htny-coder/claude/cbz0-drift-evide…
d6g8k5htny-coder Oct 31, 2026
7244c18
Add verified exact-module kernel replay adapter and project coverage …
d6g8k5htny-coder Oct 29, 2026
eb1aafa
Correct replay-tool notes to reuse completed Math core evidence
d6g8k5htny-coder Oct 29, 2026
9e2a5e7
Harden exact kernel replay resource bounds and abnormal child cleanup
d6g8k5htny-coder Oct 29, 2026
4c50b12
Require selected test-body lifecycle evidence for kernel mutation kills
d6g8k5htny-coder Oct 29, 2026
de5104c
Refuse unexecuted lazy bodies in kernel mutation grading
d6g8k5htny-coder Oct 29, 2026
0e685ca
Bind mutation grading to declared test-body identities
d6g8k5htny-coder Oct 29, 2026
994c121
fix(cbz): credit only test-oracle assertions as mutation kills (origi…
claude Oct 31, 2026
1c52543
refresh kernel_replay admission and Lean 4.34.1 receipts
cursoragent Oct 31, 2026
5c05957
refresh kernel_replay receipts on linear tip f3f1b517
cursoragent Nov 1, 2026
0445814
docs(agents): update active coordination board pointer from #619 to #738
d6g8k5htny-coder Nov 1, 2026
8485a7b
docs(research-index): update active board pointer from #619 to #738
d6g8k5htny-coder Nov 1, 2026
eaff683
docs(research-index): correct file and apply #738 updates
d6g8k5htny-coder Nov 1, 2026
84a0061
docs(research-index): restore the guide and pin the active board to #738
cursoragent Nov 1, 2026
c5232d1
docs(research-index): restore index + add #619 to historical boards (…
cursoragent Nov 1, 2026
ccefe6d
formal: recompose the 28 kernel-proved P15 targets of #358 onto the c…
claude Nov 1, 2026
01e99a9
Merge main into the P15 recomposition branch
claude Nov 1, 2026
43b10c6
formal: the pinned-Lean inventory specimen counts the recomposed pack…
claude Nov 1, 2026
8608f2a
docs(cbz): register the empirical statement check (main#726) under GO…
claude Nov 1, 2026
7c4a4e1
tests: freeze the historical formal bytes the Atlas bridge reproduces…
claude Nov 1, 2026
e075c6e
Merge pull request #741 from d6g8k5htny-coder/claude/cbz0-g12-registr…
d6g8k5htny-coder Nov 1, 2026
52cea4c
Merge main (e075c6e2) into claude/p15-formal-recomposition-20261029
claude Nov 1, 2026
ec6962f
Merge pull request #740 from d6g8k5htny-coder/claude/p15-formal-recom…
d6g8k5htny-coder Nov 1, 2026
cd4dbda
cbz/statement_fuzz: sample binders before the colon; exact real arith…
claude Nov 1, 2026
438b4e1
cbz/evidence(g12): r2 receipts for the real backend; README section a…
claude Nov 1, 2026
48f3a46
cbz/statement_fuzz: review pass — type tokens in binder types, bare s…
claude Nov 1, 2026
d479620
Merge pull request #742 from d6g8k5htny-coder/claude/cbz0-g12-real-ba…
d6g8k5htny-coder Nov 1, 2026
1349a47
cbz/statement_fuzz: finite discrete models for measure-theoretic stat…
claude Nov 1, 2026
891e7f0
cbz/statement_fuzz: sampling totals in the report (a8 nit); exact fac…
claude Nov 1, 2026
01e40f0
cbz/statement_fuzz: IsFiniteMeasure decided exactly; no structural as…
claude Nov 1, 2026
fe327e0
Merge pull request #743 from d6g8k5htny-coder/claude/cbz0-g12-finite-…
d6g8k5htny-coder Nov 1, 2026
b6b2380
Merge branch 'main' into routing-update-agents-738-h01
d6g8k5htny-coder Nov 1, 2026
c0bb095
Merge pull request #739 from d6g8k5htny-coder/routing-update-agents-7…
d6g8k5htny-coder Nov 1, 2026
43390b4
Merge branch 'main' into cursor/integrate-696-p696v2-onto-7500d43f-366a
d6g8k5htny-coder Nov 1, 2026
265a841
docs(status): record PR 713 landing without widening qualification
d6g8k5htny-coder Nov 1, 2026
10cd80c
docs(decisions): record source-bound status correction
d6g8k5htny-coder Nov 1, 2026
bf0ca96
Merge pull request #737 from d6g8k5htny-coder/cursor/integrate-696-p6…
d6g8k5htny-coder Nov 1, 2026
2957c71
Merge branch 'main' into dot/status-713-landed-20261101
d6g8k5htny-coder Nov 1, 2026
fe8c0fb
Merge pull request #744 from d6g8k5htny-coder/dot/status-713-landed-2…
d6g8k5htny-coder Nov 1, 2026
065a367
docs: bind empirical coverage observation to registration 741
d6g8k5htny-coder Nov 1, 2026
c1f807e
Merge pull request #746 from d6g8k5htny-coder/dot/status-coverage-sou…
d6g8k5htny-coder Nov 2, 2026
d2b0216
docs: correct lifetime-tail exponential moment threshold (#747)
d6g8k5htny-coder Nov 2, 2026
5d6efa8
Merge current main into #730 for fresh protected qualification
d6g8k5htny-coder Nov 5, 2026
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
The table of contents is too big for display.
Diff view
Diff view
  •  
  •  
  •  
80 changes: 80 additions & 0 deletions .github/workflows/cbz-cold-start-node.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,80 @@
name: cbz-cold-start-node
on:
push:
branches: [cbz/cold-start-node-20261029]
paths:
- 'tools/cbz_node_regression.py'
- 'tools/cbz_node_controls.py'
- 'tests/test_cbz_node_regression.py'
- '.github/workflows/cbz-cold-start-node.yml'
pull_request:
paths:
- 'tools/cbz_node_regression.py'
- 'tools/cbz_node_controls.py'
- 'tests/test_cbz_node_regression.py'
- '.github/workflows/cbz-cold-start-node.yml'
permissions:
contents: read
jobs:
controls-and-prepared:
runs-on: ubuntu-24.04-arm
timeout-minutes: 15
steps:
- uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1
with:
persist-credentials: false
fetch-depth: 0
- uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97
with:
python-version: '3.11'
- name: Ordinary controls and intended source/harness mutations
run: python -I -B -S tools/cbz_node_controls.py
- name: Optimized controls and intended source/harness mutations
if: always()
run: python -I -B -O -S tools/cbz_node_controls.py
- name: Fetch immutable historical fixture objects
if: always()
run: |
git clone --no-checkout https://github.com/d6g8k5htny-coder/Math-.git "$RUNNER_TEMP/Math-"
git clone --no-checkout https://github.com/d6g8k5htny-coder/query-.git "$RUNNER_TEMP/query-"
- name: Every tracked mjs test with verified fixtures
if: always()
env:
NODE_OPTIONS: --require=/definitely-missing-cbz-node-preload.cjs
NODE_PATH: /untrusted/cbz-node-path
run: python -I -B -S tools/cbz_node_regression.py --math-root "$RUNNER_TEMP/Math-" --query-root "$RUNNER_TEMP/query-" --output "$RUNNER_TEMP/cbz-node-result"
- name: Print actual result for independent readback
if: always()
run: |
python -I -B -S - <<'PY'
import hashlib, json, os
from pathlib import Path
root = Path(os.environ["RUNNER_TEMP"]) / "cbz-node-result"
record = json.loads((root / "result.json").read_text())
print("CBZ_NODE_RESULT_JSON " + json.dumps(record, sort_keys=True))
raw = (root / "node.tap").read_bytes()
def verify_log(value):
if hashlib.sha256(value).hexdigest() != record["log_sha256"]:
raise ValueError("Node transcript no longer matches executed report")
verify_log(raw)
try:
verify_log(raw + b"\0")
except ValueError:
print("CBZ_NODE_TRANSPORT_ADVERSE_PASS")
else:
raise SystemExit("modified transcript was admitted")
text = raw.decode("utf-8")
chunks = [text[i:i+4096] for i in range(0, len(text), 4096)]
print("CBZ_NODE_TAP_TOTAL " + str(len(chunks)))
print("CBZ_NODE_TAP_GIT_BLOB " + hashlib.sha1(
b"blob " + str(len(raw)).encode("ascii") + b"\0" + raw).hexdigest())
for number, chunk in enumerate(chunks):
print("CBZ_NODE_TAP_JSON " + str(number) + " " + json.dumps(chunk))
PY
- name: Preserve actual result and transcript
if: always()
uses: actions/upload-artifact@cf430e030ddbb5b0abf93d22962f4752f3646cd9
with:
name: cbz-node-result
path: ${{ runner.temp }}/cbz-node-result
if-no-files-found: error
71 changes: 71 additions & 0 deletions .github/workflows/cbz-federation-drift.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,71 @@
name: CBZ federation drift
'on':
pull_request:
push:
branches: [main]
schedule:
- cron: '41 4 * * *'
workflow_dispatch:
permissions:
contents: read
jobs:
self-test:
name: drift-crawler-self-test
runs-on: ubuntu-latest
timeout-minutes: 20
steps:
- uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1
with:
persist-credentials: false
- uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97
with:
python-version: '3.11'
- name: Behaviour and mutation tests in both interpreter modes
env:
PYTHONDONTWRITEBYTECODE: '1'
run: |
set -euo pipefail
cd tests
for mode in normal optimized; do
flag=""; [ "$mode" = optimized ] && flag="-O"
python -B $flag -m unittest test_cbz_drift test_cbz_drift_adversarial_01a103c8 test_cbz_drift_canonical_input test_cbz_drift_pr_trigger_01a11c48 -v 2>&1 | tee "$RUNNER_TEMP/drift-$mode.log"
grep -Eq '^Ran [1-9][0-9]* tests? in ' "$RUNNER_TEMP/drift-$mode.log" || { echo "::error::drift $mode run collected 0 tests"; exit 1; }
done
crawl:
name: federation-drift
needs: self-test
runs-on: ubuntu-latest
timeout-minutes: 30
steps:
- uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1
with:
persist-credentials: false
fetch-depth: 0
path: fed/main
- uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97
with:
python-version: '3.11'
- name: Crawl the federation from its workspace seed
env:
PYTHONDONTWRITEBYTECODE: '1'
run: |
set -euo pipefail
# Only the seed is named here. Every other repository, and its ref, is discovered
# from the seed's pins, submodules, repository list, registry and lake manifests.
git clone -q https://github.com/d6g8k5htny-coder/Universal-Law-Workspace.git fed/Universal-Law-Workspace
head=$(git -C fed/main rev-parse HEAD)
status=0
for at in pins tips; do
python -B -S fed/main/tools/cbz_drift/crawl.py --seed d6g8k5htny-coder/Universal-Law-Workspace \
--search fed --clone-into fed --fetch --at "$at" \
--override "d6g8k5htny-coder/main=$head" \
--json "$RUNNER_TEMP/drift-$at.json" || status=$?
[ "$status" -le 1 ] || { echo "::error::drift crawler error (exit $status)"; exit "$status"; }
done
exit "$status"
- if: always()
uses: actions/upload-artifact@cf430e030ddbb5b0abf93d22962f4752f3646cd9
with:
name: federation-drift-reports
path: ${{ runner.temp }}/drift-*.json
if-no-files-found: warn
4 changes: 4 additions & 0 deletions .github/workflows/current-site.yml
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,10 @@ name: Current research site
- 'tests/test_node_status_refresh.py'
- 'tests/test_node_status_freshness.py'
- 'cbz/evidence/node-status-freshness/run_mutations.py'
# inputs of the freshness suite and its mutation runner
- 'tools/validate_node_status.py'
- 'records/node_status/**'
- 'architecture/node-status.schema.json'
- 'tests/fixtures/node_status_refresh/**'
- '.github/workflows/current-site.yml'
schedule:
Expand Down
2 changes: 1 addition & 1 deletion AGENTS.md
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,7 @@ wait for peer or human approval. No shared `/root` alias is an exclusive
canonical-file owner. Prepare reversible edits in isolated branches and
use fresh expected-head guards when changing refs; preserve recovery paths.

The active coordination board remains [Agent Message Board #619](https://github.com/d6g8k5htny-coder/main/issues/619).
The active coordination board remains [Agent Message Board #738](https://github.com/d6g8k5htny-coder/main/issues/738).
[#684](https://github.com/d6g8k5htny-coder/main/issues/684) is the CBZ task-local
record; [#686](https://github.com/d6g8k5htny-coder/main/issues/686) records owner
source. No board rollover or foreign release is inferred from those links.
Expand Down
4 changes: 4 additions & 0 deletions DECISIONS.md
Original file line number Diff line number Diff line change
Expand Up @@ -34,3 +34,7 @@ Append-only. Historical source outcomes remain in their original records.
| 2026-10-30 00:36:59 | 3 | C/runtime | Clarified Atlas control runtime in its existing guide: CPython3.9.6 yields9 preserved assertion/subtest failures across2 grader methods because callbacks arrive after teardown; currentMain11e288 hosted3.12.15 run40976675758/attempt1/job123806316839 passed31controls and2required browser methods in each mode. Preserve failures and historical30/45 counts; update the old exclusive-writer guidance to current fluid roles. No grader, test, workflow or browser policy changed. | Yes | [Actual hosted run](https://github.com/d6g8k5htny-coder/main/actions/runs/40976675758); exact source/decoded-log diagnosis; docs/cbz/ATLAS_BROWSER_REGRESSIONS.md |
| 2026-10-30 00:36:59 | 2 | C/composition | Ruling: prepare this four-document contribution as an isolated successor of713/62292ad6 and a stacked PR, without changing the existing713 branch or resetting its current checks. Retarget to Main after that base actually lands and recheck the resulting composition. Source guards prevent overwrites; the pending base is an integration dependency, not an exclusive coordinator lock. | Yes | Original713 source and parent; current team Master; guarded source/readback records |
| 2026-10-30 00:40:56 | 2 | C/source | Guard observed713 advance62292ad6 toaf3996f5. Recompose this same bounded registration on freshaf3996f5, preserving its strict replay-qualifier GOVERNANCE section and complete prior ledger. Original author corrected review finding: GOV and STATUS now print all6 actual reproduction commands, including unchanged MomentTail unittest discovery normal/optimized, rather than only4. Private prior proposal retained; no old result rebound to new code. | Yes | Current713 source; bounded documentation review; exact command-to-native-CI comparison |
| 2026-10-30 00:01 | 2 | C | Removed the federation crawler's PR path filter so new topology/registry inputs reach discovery. Added a restricted subscription guard to its self-test; preserved the original failed check and the independently found comment-hidden-filter defect before fixing it. Local 55-test populations passed in both parent modes. The complete owner team reissue supersedes exclusive B-003 locks; this is an isolated compatible patch on Claude017's source, with no crawler/parser or mathematical change and no final tool/G7 admission. | Yes | [Pickup](https://github.com/d6g8k5htny-coder/main/pull/712#issuecomment-6511287308); [repair evidence](cbz/evidence/pr-trigger-01a11c48-20261029/README.md); [complete owner directive](https://github.com/d6g8k5htny-coder/main/issues/686#issuecomment-6511339492) |
| 2026-11-01 14:40 | 2 | B/tooling | Registered the empirical statement check (main#726, merged d0d384b1; tool blob 020cb194) under GOVERNANCE and STATUS with its exact commands, the hosted navigation run 41242533228 / job 124659189973 (35 tests ok on CPython 3.11.17 at the merge commit) and the three-class mutation contract; coverage recorded honestly: main formal 31/31 PASS, #740 formal 59/59 PASS, Math- formal 63/63 UNSUPPORTED (exact-rational interval backend is the recorded gap). No global CLOSED guard installed; the final G0-G11 run remains required. Actor: Anthropic Claude session 01NMeK (tool author); reviews of record 01DKKe (same family, P1 fixed by follow-on) and Grok Bot agent 12 (different family). | Yes | [registration](GOVERNANCE.md#empirical-statement-check-for-core-lean-arithmetic-skeletons-bounded-registration); [#726](https://github.com/d6g8k5htny-coder/main/pull/726) |

[2026-11-01 22:05 UTC] [Phase 3] [Layer C / G8] Correct the stale current-navigation statement that PR #713 is pending integration. Native PR metadata records merge 9abd2c100ae105103945073a7fa6c47b15679269 at 2026-10-31 10:18:44 UTC. Preserve the former 11e28815 source as pre-integration history, all scientific snapshot bytes and all qualification limits. This documentation correction neither replays checks nor establishes current-composition, theorem or CBZ-0 acceptance. Reversible: isolated commit; previous text retained in Git history. Evidence: https://github.com/d6g8k5htny-coder/main/pull/713 and https://github.com/d6g8k5htny-coder/main/commit/9abd2c100ae105103945073a7fa6c47b15679269 .
75 changes: 75 additions & 0 deletions GOVERNANCE.md
Original file line number Diff line number Diff line change
Expand Up @@ -122,6 +122,81 @@ Mission tools must be finished, documented with exact usage and verification,
and registered here and in `TOOLING.md` before final admission. Tools are a
means to closure, never a reason to open a general infrastructure project.

### Empirical statement check for core-Lean arithmetic skeletons: bounded registration

**Registered 2026-11-01 14:40 UTC; global admission of the empirical layer remains pending.**
[main PR #726](https://github.com/d6g8k5htny-coder/main/pull/726), merged as
`d0d384b18a409ed51061458287dde22816782210`, supplies `tools/cbz/statement_fuzz.py`
(blob `020cb194c206d268972fcc9f50dd0707b21819d0`, SHA-256
`1bd0f4a3059d6f040cb978691d2954deecf9a84287ce2272e48fe9ae93bdd7a7`),
`tests/test_cbz_statement_fuzz.py` (blob `723bbd306c70f0ea66b2c461ea40da9df4d923b6`)
and the run records under `cbz/evidence/g12-statement-fuzz-01n/`.

Purpose: the addendum's empirical layer for *statements*. Kernel verification is not
strengthened by sampling, so for every theorem registered in a formal package's
`manifest.json` the tool parses the Lean statement and the package's own `def`s in an
exact-arithmetic interpreter for the core-Lean subset these skeletons use, evaluates it
independently of Lean (Python integers and `Fraction`; a float anywhere is an assertion
failure), enumerates finite quantifier domains exhaustively (list membership, or an upper
bound on an explicit `Nat`/`ℕ` binder only), probes just outside each domain for tightness
and vacuity as information, and reports PASS / FAIL / UNSUPPORTED per target. Lean core
semantics are implemented where they differ from naive arithmetic: `Nat` truncated
subtraction, totalized division (`x / 0 = 0`, `x % 0 = x`), `Nat` floor division,
Euclidean `Int` `/` and `%` (`Int.ediv`/`Int.emod`), numeral typing by the `binop%`
maximal-type rule. A FAIL is a misstatement or transcription defect in the Lean text,
never kernel evidence; UNSUPPORTED is fail-closed and makes the exit code non-zero.

From a checkout of this repository, run:

```
python3 -B -S -m unittest tests.test_cbz_statement_fuzz -v
python3 -B -O -S -m unittest tests.test_cbz_statement_fuzz -v
python3 -B -S tools/cbz/statement_fuzz.py --package formal --selftest --json <report.json>
```

Self-verification: the 35 tests (tokenizer, Lean semantics including the six Euclidean
division goldens of main#684/6511137449, definitions, folds, pairs, quantifiers, vacuity
and tightness probes, fail-closed behaviour, the mutation contract, the real package) ran
on the merge commit in the hosted `navigation` job
([run 41242533228](https://github.com/d6g8k5htny-coder/main/actions/runs/41242533228),
job `124659189973`, CPython 3.11.17, artifact `research-navigation-41242533228` whose
`commit.txt` is `d0d384b1…` and whose `tests-normal.log` shows the 35
`test_cbz_statement_fuzz` cases `ok` among 1,892) and locally in both modes with
`-W error`. `--selftest` grades every module by a three-class mutation contract:
guaranteed-false mutants must FAIL (each comparison replaced by its negation one conjunct
at a time, the right-hand literal of an equality shifted by one — never `<`→`≤`),
truth-preserving weakenings (`<`→`≤`, `>`→`≥`) must PASS, and the manifest's declared
negative controls that change a statement must FAIL; an UNSUPPORTED or errored mutant is
a survivor, never a kill, and a stubbed evaluator fails the unmutated control. Reviews of
record: same-family 01DKKe
([726/6547986788](https://github.com/d6g8k5htny-coder/main/pull/726#issuecomment-6547986788);
one P1 fail-open domain inference found and fixed by its follow-on, tree `198c1f97`) and
different-family Grok Bot agent 12
([726/6548050253](https://github.com/d6g8k5htny-coder/main/pull/726#issuecomment-6548050253),
PASS with the follow-on); Codex 01a103c8 supplied the division-semantics controls.

Coverage actually observed, per package and cut:

| Package | Cut | Targets | PASS | UNSUPPORTED | Mutation contract |
|---|---|---:|---:|---:|---|
| main `formal/` (SIDE24 skeleton) | `4712fc13` (`formal/` unchanged since) | 31 | 31 | 0 | 98/98 killed, 12 weakenings kept, 7 declared controls FAIL |
| main #740 `formal/` (SIDE24 + P15 skeletons, candidate) | `43b10c6f` | 59 | 59 | 0 | 184/184 killed, 14 declared controls FAIL |
| Math- `formal/` (`ResearchFormalCoreR1`, Mathlib real analysis) | `19a55750` | 63 | 0 | **63** | — |

Gate mapping: G0/G5/G6 use the documented tests and the mutation contract; G8/G9/G11
require this exact scope, runnable commands and self-verification record. For a new
CLOSED claim on a core-Lean arithmetic statement, a PASS at the same source cut as the
kernel receipt is the applicable empirical validation this registry recognises, recorded
with the report file's SHA-256 and the `manifest_sha256` it binds; it adds nothing to and
takes nothing from G2–G4. The tool does not cover Mathlib real analysis, binders before
the colon or unbounded quantifiers, so the Math- core's 63 statements remain explicitly
unsupported by the empirical layer; an exact-rational interval backend for
`Real.exp`/`log`/`sqrt` (offered by Claude017, main#684/6532742483) is the recorded gap.
This component installs no global CLOSED guard and does not complete the common final
G0–G11 run. Maintenance owner: none; stdlib only, self-contained. Actual executor:
Anthropic Claude, Claude Code session `session_01NMeKEismAyeqgdB4sy2NJU`; scientific
effect NONE.

### Finite MomentTail empirical component: bounded registration

**Registered 2026-10-30 00:36:59 UTC; global admission remains pending.**
Expand Down
25 changes: 22 additions & 3 deletions STATUS.md
Original file line number Diff line number Diff line change
Expand Up @@ -15,9 +15,10 @@ cross-repository synchronization and final common G0-G11 pass remain unfinished.
Source-only checks and individual successful jobs do not complete the twelve
baseline criteria. The [foundation candidate #695](https://github.com/d6g8k5htny-coder/main/pull/695)
is a candidate handoff, not the current default-branch baseline.
At this observation, current Main is `11e28815163e15223e8827fe6ff47a1faaf36ebd`.
PR #713 is pending integration; its replay sources, controls and this documentation
must be qualified at their final composed source. The proof catalogue and other
The pre-integration Main source was `11e28815163e15223e8827fe6ff47a1faaf36ebd`.
[PR #713](https://github.com/d6g8k5htny-coder/main/pull/713) merged on 2026-10-31 at 10:18:44 UTC
as `9abd2c100ae105103945073a7fa6c47b15679269`; its qualification evidence
remains bound to the sources actually checked, not automatically to later compositions. The proof catalogue and other
foundation material in #695 are pending, not an admitted default-branch baseline.
This intermediate entry is not a completed cold-start acceptance test.

Expand Down Expand Up @@ -45,6 +46,24 @@ not full AST/type/theorem synchronization. New gating tools require documented
commands and self-verification before admission; unavailable or unsupported
coverage remains explicit. No documented command here runs all G0-G11 yet.

The empirical statement check for core-Lean arithmetic skeletons is a registered
bounded component on `main` ([PR #726](https://github.com/d6g8k5htny-coder/main/pull/726),
merged `d0d384b18a409ed51061458287dde22816782210`). From a checkout, run:

```
python3 -B -S -m unittest tests.test_cbz_statement_fuzz -v
python3 -B -O -S -m unittest tests.test_cbz_statement_fuzz -v
python3 -B -S tools/cbz/statement_fuzz.py --package formal --selftest --json report.json
```

It evaluates every registered Lean statement of a formal package independently in exact
arithmetic with Lean-core semantics and grades itself by a mutation contract; the
[registration](GOVERNANCE.md#empirical-statement-check-for-core-lean-arithmetic-skeletons-bounded-registration)
records commands, hosted self-verification and limits. At [registration #741](https://github.com/d6g8k5htny-coder/main/pull/741): main `formal/` 31/31
PASS; the Math- core's 63 real-analysis statements are UNSUPPORTED, which is the honest
coverage at that source cut, not a pass. A PASS is statement-level evidence
only: not kernel evidence, not scientific acceptance, not the common G0-G11 run.

The finite MomentTail component is a registered bounded candidate in
[Math PR #545](https://github.com/d6g8k5htny-coder/Math-/pull/545), exact source
`e1cf617b6bc979b75d420f28df17ddad59426522`. In an isolated checkout of that Math
Expand Down
Loading
Loading