Theorem FL v1.1: Conjecture 6 of #242 through its soft model, identified with the failure law of #170/#175 (F = kA∗(α₁+α₂))

.github/workflows/soft-fold-limit.yml

@@ -0,0 +1,166 @@
+name: Soft fold limit exact controls
+
+'on':
+  pull_request:
+    paths:
+      - 'frontiers/soft_fold_limit_20261002/**'
+      - '.github/workflows/soft-fold-limit.yml'
+      # bound merged sources (consumed and cited in SOURCES.json); the cited unmerged sources are bound through the API
+      - 'frontiers/three_fronts_20260924/LIFETIME_REMAINDER.md'
+      - 'imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md'
+      - 'imports/lifetime_parent_20260925/MARKED_CYLINDER_CAP_PROOF.md'
+      - 'imports/lifetime_parent_20260925/ERRATUM_CONGRUENCE.md'
+      - 'reviews/d1_section9_borel_repair_20260925/REPAIR.md'
+      - 'reviews/d1_chain_reconciliation_20260928/RECONCILIATION.md'
+      - 'frontiers/cusp_second_order_20261001/PROOF.md'
+      - 'frontiers/c7_total_bounded_20260929/PROOF.md'
+      - 'frontiers/elder_dimension_lift_20260928/PROOF.md'
+      - 'frontiers/third_order_rate_20261001/PROOF.md'
+      - 'frontiers/local_elder_geometry_20260930/PROOF.md'
+      - 'frontiers/concave_fibre_elder_20260930/PROOF.md'
+      # the consumed unmerged #242 PROOF is bound through the API (recorded head, blob and the current PR head)
+      - 'frontiers/soft_rejected_pairs_20261002/PROOF.md'
+  workflow_dispatch:
+
+permissions:
+  contents: read
+  pull-requests: read
+
+jobs:
+  exact-controls:
+    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'
+          GH_TOKEN: ${{ github.token }}
+          GH_REPOSITORY: ${{ github.repository }}
+        run: |
+          set -euo pipefail
+          python -B -S - <<'PY'
+          import base64, hashlib, json, os, pathlib, subprocess, sys, urllib.parse, urllib.request
+          root = pathlib.Path('frontiers/soft_fold_limit_20261002').resolve()
+          manifest = json.loads((root / 'SOURCES.json').read_text())
+          present = sorted(p.name for p in root.iterdir())
+          expected_names = sorted([e['path'] for e in manifest['files']] + ['SOURCES.json'])
+          if present != expected_names:
+              raise ValueError('packet tree differs from manifest: ' + repr(present))
+          for entry in manifest['files']:
+              path = root / entry['path']
+              if path.is_symlink():
+                  raise ValueError('symlink: ' + entry['path'])
+              data = path.read_bytes()
+              if len(data) != entry['bytes'] or hashlib.sha256(data).hexdigest() != entry['sha256']:
+                  raise ValueError('packet file identity mismatch: ' + entry['path'])
+          def same(data, entry):
+              framed = b'blob ' + str(len(data)).encode() + b'\0' + data
+              return len(data) == entry['bytes'] and hashlib.sha256(data).hexdigest() == entry['sha256'] and hashlib.sha1(framed).hexdigest() == entry['git_blob']
+          def tree_entry(path):
+              # the checked-out commit's tree entry for path: (mode, type, blob) or None; symlinks have mode 120000
+              out = subprocess.run(['git', 'ls-tree', '-z', 'HEAD', '--', path], check=True, capture_output=True).stdout
+              if not out:
+                  return None
+              meta, name = out.rstrip(b'\0').split(b'\t', 1)
+              if name.decode() != path:
+                  raise ValueError('unexpected tree entry for ' + path)
+              mode, kind, sha = meta.decode().split()
+              return mode, kind, sha
+          def tree_bytes(entry):
+              # a source read from the checkout must be a regular file whose tree blob is the recorded one
+              te = tree_entry(entry['path'])
+              if te is None:
+                  return None
+              mode, kind, sha = te
+              if mode != '100644' or kind != 'blob' or sha != entry['git_blob']:
+                  raise ValueError('tree entry is not the recorded regular-file blob (mode/type/blob ' + ' '.join(te) + '): ' + entry['path'])
+              path = pathlib.Path(entry['path'])
+              if path.is_symlink() or not path.is_file():
+                  raise ValueError('checkout path is not a regular file: ' + entry['path'])
+              return path.read_bytes()
+          for entry in manifest['consumed'] + manifest['cited_only']:
+              data = tree_bytes(entry)
+              if data is None or not same(data, entry):
+                  raise ValueError('merged source drifted or absent: ' + entry['path'])
+          # unmerged sources are bound to their recorded commit, path and blob through the repository API: the head must
+          # resolve, the path in that head's tree must be a file with the recorded blob id and size, and the bytes must have
+          # the recorded sha256; a consumed dependency that has landed is instead read from the tree and must be identical
+          # to the pinned version (else this packet needs rebinding)
+          api = 'https://api.github.com/repos/' + os.environ['GH_REPOSITORY']
+          def get_json(url):
+              req = urllib.request.Request(url, headers={'Authorization': 'Bearer ' + os.environ['GH_TOKEN'],
+                                                         'Accept': 'application/vnd.github+json'})
+              with urllib.request.urlopen(req, timeout=60) as resp:
+                  return json.load(resp)
+          def bound(entry):
+              commit = get_json(api + '/commits/' + entry['head'])
+              if commit.get('sha') != entry['head']:
+                  raise ValueError('recorded head does not resolve: ' + entry['head'])
+              node = get_json(api + '/contents/' + urllib.parse.quote(entry['path']) + '?ref=' + entry['head'])
+              if (node.get('type') != 'file' or node.get('path') != entry['path'] or node.get('sha') != entry['git_blob']
+                      or node.get('size') != entry['bytes']):
+                  raise ValueError('recorded head/path does not map to the recorded blob: ' + entry['path'])
+              blob = get_json(api + '/git/blobs/' + entry['git_blob'])
+              if blob.get('encoding') != 'base64':
+                  raise ValueError('unexpected blob encoding for ' + entry['path'])
+              return base64.b64decode(blob['content'])
+          def current(entry):
+              # drift gate (as on #220, after Copilot's review there): the recorded head keeps resolving after a dependency PR advances, so
+              # also resolve the dependency PR now. Open: the file at its current head must be the pinned blob. Merged:
+              # the file at its merge commit must be the pinned blob. Closed unmerged: rebinding is required.
+              pr = get_json(api + '/pulls/' + entry['pr'].split('#', 1)[1])
+              merged = bool(pr.get('merged'))
+              if merged:
+                  ref = pr.get('merge_commit_sha')
+              elif pr.get('state') == 'open':
+                  ref = pr['head']['sha']
+              else:
+                  raise ValueError('dependency ' + entry['pr'] + ' closed without merge: rebind required')
+              node = get_json(api + '/contents/' + urllib.parse.quote(entry['path']) + '?ref=' + ref)
+              if node.get('type') != 'file' or node.get('sha') != entry['git_blob'] or node.get('size') != entry['bytes']:
+                  raise ValueError('dependency ' + entry['pr'] + ' advanced: ' + entry['path'] + ' at ' + ref
+                                   + ' is not the pinned blob (rebind required)')
+              return ref, merged
+          for kind in ('consumed_unmerged', 'cited_unmerged'):
+              for entry in manifest.get(kind, []):
+                  # a consumed dependency's PR is resolved first (Codex review 4167121714 on #244). Once it has merged,
+                  # its source must be the recorded regular-file blob in this tree: a deleted, renamed or changed landed
+                  # source fails, and there is no fallback to the historical head. While it is open, the source is bound
+                  # through the API. Cited sources are bound through the API.
+                  now, merged = current(entry) if kind == 'consumed_unmerged' else (None, False)
+                  landed = tree_bytes(entry) if kind == 'consumed_unmerged' else None
+                  if merged and landed is None:
+                      raise ValueError('dependency ' + entry['pr'] + ' has merged but its pinned source is absent from this '
+                                       'tree: ' + entry['path'])
+                  if landed is not None:
+                      data, where = landed, 'tree'
+                  else:
+                      if os.path.lexists(entry['path']) and kind == 'consumed_unmerged':
+                          raise ValueError('path present in the checkout but not as a tracked blob: ' + entry['path'])
+                      data, where = bound(entry), 'head/path/blob api'
+                  if not same(data, entry):
+                      raise ValueError(kind + ' source differs from its pinned blob (rebind required): ' + entry['path'] + ' via ' + where)
+                  print(json.dumps({kind + '_bound': entry['path'], 'git_blob': entry['git_blob'], 'head': entry['head'],
+                                    'via': where, 'current_ref_checked': now, 'dependency_merged': merged}))
+          script = str(root / 'fold_check.py')
+          expected = (root / 'RESULTS.json').read_bytes()
+          for flags in (['-B', '-S'], ['-B', '-O', '-S']):
+              out = subprocess.run([sys.executable, *flags, script], check=True, capture_output=True, timeout=600).stdout
+              if out != expected:
+                  raise RuntimeError('output differs from RESULTS.json under ' + ' '.join(flags))
+              for m in manifest['mutants']:
+                  rc = subprocess.run([sys.executable, *flags, script, '--mutant', m], capture_output=True, timeout=600).returncode
+                  if rc != 1:
+                      raise RuntimeError('mutant ' + m + ' not rejected')
+              rc = subprocess.run([sys.executable, *flags, script, '--mutant', 'M99'], capture_output=True, timeout=600).returncode
+              if rc != 2:
+                  raise RuntimeError('unknown mutant label not rejected with exit 2')
+          print(json.dumps({'scientific_effect': 'NONE', 'mathematical_acceptance': False}))
+          PY
+          git diff --exit-code