d6g8k5htny-coder · Oct 14, 2026 · Oct 13, 2026 · Oct 13, 2026 · Oct 13, 2026 · Oct 13, 2026
@@ -149,3 +149,28 @@ The pin checks the reported compiler identity; it is not executable-byte
 authentication or independent source alignment. New current-commit
 kernel receipts and hosted checks are still required after publication.
 Alignment remains PENDING_INDEPENDENT_REVIEW; scientific effect NONE.
+
+## Uniform runtime guard successor — 2026-10-13
+
+The tool/version adoption guard ([main#275 6154089628](https://github.com/d6g8k5htny-coder/main/issues/275#issuecomment-6154089628))
+requires the exact runtime and clean locked dependencies to be observed
+before the first and after the last Lean execution of every path. This
+companion's own Lean runs follow the core gate, so the core receipt's
+observations do not cover them. `replay.sh` now writes `toolchain-final.log`
+and `packages-final.log` (name, HEAD and clean/dirty for each dependency)
+after the companion's last Lean execution. `check.py finish` requires both
+toolchain lines to equal the core receipt's exact release, every final
+dependency to equal the formal lock and be clean, and the core receipt to
+carry equal preflight and final observations. The companion receipt records
+the final observation.
+
+This consumer now pins whole formal tree `fc0b11706d064b9de42331ee0a2464865107b87b`,
+manifest SHA256 `7149915669414e22f593ce2c6540c5e10d922eb758c7464794fc64764e679778`,
+and gate SHA256 `25e08d9054b929dd657668e4ee4a3524688dc476e5af958f950de3b919f04e9a`.
+
+All earlier document text is preserved as the historical prefix. Proofs,
+imports, toolchain/dependency locks, workflows and contracts keep their
+bytes. The new tests are synthetic and do not execute Lean. New
+current-commit kernel receipts and hosted checks are still required after
+publication. Alignment remains PENDING_INDEPENDENT_REVIEW; scientific
+effect NONE.
@@ -1,5 +1,5 @@
 {
-  "core_tree": "38b6d1a7746075b560349d184a461933745c11ce",
+  "core_tree": "fc0b11706d064b9de42331ee0a2464865107b87b",
   "files": {
     ".github/workflows/d2-atom-integral.yml": {
       "bytes": 1942,
@@ -17,24 +17,24 @@
       "sha256": "247507c4b7aeaccc033cd4d648442172d61227bb27239a7dacccd0f2fa1ba6c3"
     },
     "companions/d2_atom_integral_20261006/SCOPE.md": {
-      "bytes": 9439,
-      "git_blob": "fa50a4dbae2f95ce337d7f022faed05d686f942e",
-      "sha256": "e52b047f49475e8e1bdf83333d55be8f207345e40fbca123800d55ae98426ce3"
+      "bytes": 10928,
+      "git_blob": "71008894a5a3aa01da18163afbce1903dabe51df",
+      "sha256": "90f12484ead012929ce0664ed0d4ef90f40c2d75d39d2d8580115f19b2db40ec"
     },
     "companions/d2_atom_integral_20261006/check.py": {
-      "bytes": 7852,
-      "git_blob": "d7e7df7dfc49de50596059db3d11dd3f552cb0c0",
-      "sha256": "5686c2d1914061ff01c0faa2409e19398be81207b1899448854bdd87569768e7"
+      "bytes": 10044,
+      "git_blob": "eb918b7ee775c0bb61a9ffff2cadba0b76e40673",
+      "sha256": "df3f8aec73478b74d0d0f2f06d2655097f80b9d9ebbb4c720d6a63076493315d"
     },
     "companions/d2_atom_integral_20261006/replay.sh": {
-      "bytes": 2879,
-      "git_blob": "a4247be9ff3eff0229fef62c9b4a6b792159a6c7",
-      "sha256": "66387fcea3e2795fbe69856b0b0c37013f3b0540c2fe2e11dc2a97b373285bcf"
+      "bytes": 3471,
+      "git_blob": "7dcfcf055f01a973e9e934abe0d732a580685568",
+      "sha256": "89d9a0c64fd88aa8cf8c6614df84b3f543c3d4ecc87ad2e529feffda90091c75"
     },
     "companions/d2_atom_integral_20261006/test_check.py": {
-      "bytes": 5418,
-      "git_blob": "cd9a642876878d1f18b494f5bee2cf30a6da3f83",
-      "sha256": "b6448618b35e44a2181a12703a7ec464409a1b35ea641b95c690a60c6184247d"
+      "bytes": 8946,
+      "git_blob": "efa3793f8ffeecc3e504b559601d52c6e68008f0",
+      "sha256": "83750832498ac74f96297174c494262537069c9c82eacb7aa2315f39a77ad454"
     }
   },
   "scientific_effect": "NONE",

@@ -18,9 +18,9 @@
 PACKAGE='companions/d2_atom_integral_20261006'
 WORKFLOW='.github/workflows/d2-atom-integral.yml'
 REPO='d6g8k5htny-coder/Math-'
-CORE_TREE='38b6d1a7746075b560349d184a461933745c11ce'
-CORE_MANIFEST='40cb6ffc6776717a26d2a0a66815aeef508b0c8411588fff06ff2cec43a752a1'
-CORE_GATE='278989bbba7e1f90870ea0d197a996bc0a65b2a4b217e2eb284accb1282356c1'
+CORE_TREE='fc0b11706d064b9de42331ee0a2464865107b87b'
+CORE_MANIFEST='7149915669414e22f593ce2c6540c5e10d922eb758c7464794fc64764e679778'
+CORE_GATE='25e08d9054b929dd657668e4ee4a3524688dc476e5af958f950de3b919f04e9a'
 CONSUMED={
  'companions/d2_moment_bridge_20261006/D2MomentBridge.lean':'b3184107e290189b91e3e18fd2aa1cb631bb9bde',
  'companions/d2_square_schur_20261006/D2SquareSchur.lean':'4855c92d55254969e1de7f8cf8dec2bdc027cf69'}
@@ -110,6 +110,35 @@ def emit(out):
     for label,statement in FALSE_STATEMENTS.items():
         (out/(label+'.lean')).write_text('import D2AtomIntegral\nexample : '+statement+' := by\n  norm_num\n')
 
+LEAN_VERSION=re.compile(r'Lean \(version 4\.34\.1, [^()\r\n]+, commit 5045d0056413266e57c625dcd7c365b10e377c52, Release\)')
+
+
+def final_runtime(out,core,lock):
+    """The companion's own Lean runs follow the core gate, so the core's observations do not cover them.
+    replay.sh observes the runtime and the dependencies again after the companion's last Lean execution;
+    both must equal the core gate's equal preflight and final observations, the exact release and the lock."""
+    version=core.get('lean_version')
+    require(isinstance(version,str) and LEAN_VERSION.fullmatch(version) is not None,'core receipt runtime is not the pinned release')
+    obs=core.get('observations')
+    require(isinstance(obs,dict) and set(obs)=={'preflight','final'} and isinstance(obs['final'],dict) and obs['final']==obs['preflight'],
+            'core receipt lacks equal preflight and final observations')
+    require(obs['final'].get('lean_version')==version and obs['final'].get('dependency_revisions')==lock
+            and obs['final'].get('dependency_worktrees')=='CLEAN','core final observation differs from the lock')
+    for name in ('toolchain.log','toolchain-final.log'):
+        require((out/name).is_file() and (out/name).read_text()==version+'\n','companion runtime differs from the core gate: '+name)
+    require((out/'packages-final.log').is_file(),'missing final dependency observation')
+    seen={}
+    for line in (out/'packages-final.log').read_text().splitlines():
+        parts=line.split(' ')
+        require(len(parts)==3 and parts[0] not in seen,'malformed final dependency record')
+        seen[parts[0]]=(parts[1],parts[2])
+    require(set(seen)==set(lock),'final dependency set differs from the lock')
+    for name,(head,state) in sorted(seen.items()):
+        require(head==lock[name],'final dependency HEAD differs from the lock: '+name)
+        require(state=='clean','final dependency worktree is not clean: '+name)
+    return {'lean_version':version,'dependency_revisions':dict(sorted(lock.items())),'dependency_worktrees':'CLEAN'}
+
+
 def finish(out):
     current=source();require(strict((out/'source.json').read_bytes())==current,'source changed during execution')
     ax=core_gate().audit_axioms((out/'axioms.log').read_text(),list(TARGETS))
@@ -122,7 +151,8 @@ def finish(out):
     raw=(ROOT/'formal/.lake/formal-evidence/receipt.json').read_bytes();core=strict(raw)
     require(core['checked_commit']==current['checked_commit'] and core['manifest_sha256']==CORE_MANIFEST,'core identity')
     require(core['formalization_status']=='kernel-checked','no core kernel receipt')
-    result={**current,'axioms':ax,'theorem_count':6,'definition_count':0,'core_receipt_sha256':sha(raw),
+    final=final_runtime(out,core,strict((ROOT/'formal/manifest.json').read_bytes())['dependency_revisions'])
+    result={**current,'axioms':ax,'theorem_count':6,'definition_count':0,'core_receipt_sha256':sha(raw),'final_observation':final,
        'formalization_status':'kernel-checked','alignment_status':'PENDING_INDEPENDENT_REVIEW',
        'scientific_acceptance':False,'log_sha256':{p.name:sha(p.read_bytes()) for p in sorted(out.iterdir()) if p.is_file()}}
     (out/'receipt.json').write_text(json.dumps(result,sort_keys=True,indent=2)+'\n')

@@ -46,6 +46,16 @@ for control in RejectOverlappingEvents RejectNonProbabilityGap RejectZeroRadiusS
   printf '%s\n' "$code" >"$ATOM_OUT/$control.status"
   python3 -B -S "$ATOM_SIDE/check.py" negative "$ATOM_OUT/$control.log" --control "$control" --status "$code"
 done
+# Final observation after the companion's last Lean execution: the core gate observed the runtime
+# before these runs, so it is observed again here, and `check.py finish` requires it unchanged.
+lean --version > "$ATOM_OUT/toolchain-final.log"
+: > "$ATOM_OUT/packages-final.log"
+for pkg in "$PWD"/.lake/packages/*/; do
+  head="$(git -C "$pkg" rev-parse HEAD)"
+  status="$(git -C "$pkg" status --porcelain --untracked-files=normal)"
+  if [ -z "$status" ]; then state=clean; else state=dirty; fi
+  printf '%s %s %s\n' "$(basename "$pkg")" "$head" "$state" >> "$ATOM_OUT/packages-final.log"
+done
 INNER
 cd "$ROOT"
 python3 -B -S "$SIDE/check.py" finish "$OUT"

@@ -98,4 +98,56 @@ def test_workflow_preserves_history_and_execution(self):
         self.assertNotIn('continue-on-error',workflow)
         self.assertNotIn('linter.unnecessarySeqFocus false',shell)
 
+
+class FinalRuntimeTests(unittest.TestCase):
+    """The companion's runtime is re-observed after its own last Lean run; earlier core evidence does not cover it."""
+    RELEASE='Lean (version 4.34.1, x86_64-unknown-linux-gnu, commit 5045d0056413266e57c625dcd7c365b10e377c52, Release)'
+
+    def setUp(self):
+        spec=importlib.util.spec_from_file_location('final_runtime_check_d2_atom_i',SIDE/'check.py')
+        self.c=importlib.util.module_from_spec(spec);spec.loader.exec_module(self.c)
+        tmp=tempfile.TemporaryDirectory();self.addCleanup(tmp.cleanup);self.out=Path(tmp.name)
+        self.lock={'mathlib':'d'*40,'batteries':'e'*40}
+        observed={'lean_version':self.RELEASE,'dependency_revisions':dict(self.lock),'dependency_worktrees':'CLEAN','manifest_sha256':'a'*64}
+        self.core={'lean_version':self.RELEASE,'observations':{'preflight':dict(observed),'final':dict(observed)}}
+        for name in ('toolchain.log','toolchain-final.log'):(self.out/name).write_text(self.RELEASE+'\n')
+        self.packages({n:(h,'clean') for n,h in self.lock.items()})
+
+    def packages(self,rows):
+        (self.out/'packages-final.log').write_text(''.join(n+' '+h+' '+s+'\n' for n,(h,s) in rows.items()))
+
+    def refuse(self,message):
+        with self.assertRaisesRegex(ValueError,message):self.c.final_runtime(self.out,self.core,self.lock)
+
+    def test_final_observation_equal_to_core_passes(self):
+        self.assertEqual(self.c.final_runtime(self.out,self.core,self.lock)['dependency_worktrees'],'CLEAN')
+
+    def test_same_semver_other_commit_or_build_refused(self):
+        for text in (self.RELEASE.replace('5045d0056413266e57c625dcd7c365b10e377c52','0'*40),self.RELEASE.replace(', Release)',', Debug)')):
+            with self.subTest(text=text):
+                (self.out/'toolchain-final.log').write_text(text+'\n');self.refuse('differs from the core gate')
+
+    def test_runtime_changed_after_core_gate_refused(self):
+        other=self.RELEASE.replace('x86_64-unknown-linux-gnu','aarch64-unknown-linux-gnu')
+        (self.out/'toolchain-final.log').write_text(other+'\n');self.refuse('differs from the core gate: toolchain-final.log')
+
+    def test_dependency_moved_or_dirtied_after_core_gate_refused(self):
+        self.packages({'mathlib':('f'*40,'clean'),'batteries':('e'*40,'clean')});self.refuse('HEAD differs')
+        self.packages({'mathlib':('d'*40,'dirty'),'batteries':('e'*40,'clean')});self.refuse('not clean')
+        self.packages({'mathlib':('d'*40,'clean')});self.refuse('set differs')
+
+    def test_missing_final_observation_refused(self):
+        (self.out/'packages-final.log').unlink();self.refuse('missing final dependency observation')
+        self.packages({n:(h,'clean') for n,h in self.lock.items()});(self.out/'toolchain-final.log').unlink();self.refuse('toolchain-final.log')
+
+    def test_core_receipt_without_equal_observations_refused(self):
+        self.core.pop('observations');self.refuse('lacks equal preflight and final')
+
+    def test_replay_observes_after_the_last_lean_run_and_finish_requires_it(self):
+        replay=(SIDE/'replay.sh').read_text();inner=replay[:replay.index('\nINNER\n')]
+        self.assertGreater(inner.index('toolchain-final.log'),inner.rindex('lean -DwarningAsError=true'))
+        self.assertGreater(inner.index('packages-final.log'),inner.rindex('lean -DwarningAsError=true'))
+        source=(SIDE/'check.py').read_text();body=source[source.index('def finish(out):'):source.index('def main(')]
+        self.assertIn('final_runtime(out,',body)
+
 if __name__=='__main__':unittest.main(verbosity=2)
@@ -175,3 +175,28 @@ The pin checks the reported compiler identity; it is not executable-byte
 authentication or independent source alignment. New current-commit
 kernel receipts and hosted checks are still required after publication.
 Alignment remains PENDING_INDEPENDENT_REVIEW; scientific effect NONE.
+
+## Uniform runtime guard successor — 2026-10-13
+
+The tool/version adoption guard ([main#275 6154089628](https://github.com/d6g8k5htny-coder/main/issues/275#issuecomment-6154089628))
+requires the exact runtime and clean locked dependencies to be observed
+before the first and after the last Lean execution of every path. This
+companion's own Lean runs follow the core gate, so the core receipt's
+observations do not cover them. `replay.sh` now writes `toolchain-final.log`
+and `packages-final.log` (name, HEAD and clean/dirty for each dependency)
+after the companion's last Lean execution. `check.py finish` requires both
+toolchain lines to equal the core receipt's exact release, every final
+dependency to equal the formal lock and be clean, and the core receipt to
+carry equal preflight and final observations. The companion receipt records
+the final observation.
+
+This consumer now pins whole formal tree `fc0b11706d064b9de42331ee0a2464865107b87b`,
+manifest SHA256 `7149915669414e22f593ce2c6540c5e10d922eb758c7464794fc64764e679778`,
+and gate SHA256 `25e08d9054b929dd657668e4ee4a3524688dc476e5af958f950de3b919f04e9a`.
+
+All earlier document text is preserved as the historical prefix. Proofs,
+imports, toolchain/dependency locks, workflows and contracts keep their
+bytes. The new tests are synthetic and do not execute Lean. New
+current-commit kernel receipts and hosted checks are still required after
+publication. Alignment remains PENDING_INDEPENDENT_REVIEW; scientific
+effect NONE.
@@ -1,5 +1,5 @@
 {
-  "core_tree": "38b6d1a7746075b560349d184a461933745c11ce",
+  "core_tree": "fc0b11706d064b9de42331ee0a2464865107b87b",
   "definitions": [
     "moment",
     "cubicResidual"
@@ -16,24 +16,24 @@
       "sha256": "cde3bbd96eb29eb9ab7ff1448ffab1f794fb2b80355ac618800155eea6ccc42f"
     },
     "companions/d2_moment_bridge_20261006/README.md": {
-      "bytes": 10788,
-      "git_blob": "5b948caaeef3abaf990c66581bfc8194506dde2d",
-      "sha256": "a5fc959720d65590f682956244a61bd9bb4d7f4426d8b82bf401cc07f5a4408e"
+      "bytes": 12277,
+      "git_blob": "005796b5527601c1156d2deaa9c950adf253faf3",
+      "sha256": "16b5b7e07eaa2a047160c2a295333eea370644d8343b635d6d92a4556a33eff6"
     },
     "companions/d2_moment_bridge_20261006/check.py": {
-      "bytes": 8037,
-      "git_blob": "882130d0a5428799c654b60c3ba01903df970d7d",
-      "sha256": "d51bcdf964c1c4655602fcbd0b852da1dd3683d04a377842eb23a20f3e9e6727"
+      "bytes": 10232,
+      "git_blob": "867324d3829e35d503df993f1a69a159c4a664c0",
+      "sha256": "04310a141a4c042eb8d255bba2c073b9ec348460e6dc522b6d7189285acd2730"
     },
     "companions/d2_moment_bridge_20261006/replay.sh": {
-      "bytes": 2195,
-      "git_blob": "85c0de87f883386a8a36f5db79c51391313f09c9",
-      "sha256": "9df04dab884e78d8404334724dc62bf4f3e4c44248cbd5968225885af388f303"
+      "bytes": 2793,
+      "git_blob": "8661a6c998fc2900c7a6dba66c548341887999ee",
+      "sha256": "1e50e7ffc5c68b3771e32f2574d709d055a9b5b43ef1fa74bcaccfc14e912a68"
     },
     "companions/d2_moment_bridge_20261006/test_bridge.py": {
-      "bytes": 7607,
-      "git_blob": "2f6ab4e8cc5d0202320045a41f90966f3cecd6f5",
-      "sha256": "31a071461dc0d38093f075c8772c20c3a8ad902d6e53cb78878940176a048059"
+      "bytes": 11134,
+      "git_blob": "5bcc4628bf61f035f96f7a4faf6c796a38e05fe9",
+      "sha256": "cf257c0dd750c5cc108d5af5d61129531d7f57e2ed03c6a5ab8261964fb25469"
     }
   },
   "schema": 1,