#!/usr/bin/env python3 """Audit the supplied OMEGA Word transcription and Julia companion. Requires Python 3.11+ and SymPy 1.14.0. No Lean or Julia build is performed. Usage: python audit_omega_sources.py LEAN_ARCHIVE.docx JULIA_ARCHIVE.zip Version 3.0: closed inventories, declaration binding, exact-expression parsing, and recorded-value checks. Restricted to the supplied v0.1 release. Checks are explicit exceptions and remain active under python -O. """ import argparse from pathlib import Path from tempfile import TemporaryDirectory from zipfile import ZipFile import ast import csv import hashlib import re import sympy as sp def need(condition, message): if not condition: raise ValueError(message) # This is a fixed-release auditor, not a general Julia/Lean interpreter. # Inventories are independently frozen; unsupported source constructs fail closed. EXPECTED_FILES = ['DEPENDENCIES.md', 'PROOFS.md', 'Project.toml', 'README.md', 'REPRODUCTION.md', 'SHA256SUMS', 'THEOREMS.toml', 'THEOREM_GUIDE.md', 'TRANSLATION.md', 'evidence/O0.log', 'evidence/O0/gap_blocks.csv', 'evidence/O0/polynomial_certificates.tsv', 'evidence/O0/precision_sweep.csv', 'evidence/O0/rational_enclosures.tsv', 'evidence/O0/results.toml', 'evidence/O0/state_certificate.csv', 'evidence/O3.log', 'evidence/O3/gap_blocks.csv', 'evidence/O3/polynomial_certificates.tsv', 'evidence/O3/precision_sweep.csv', 'evidence/O3/rational_enclosures.tsv', 'evidence/O3/results.toml', 'evidence/O3/state_certificate.csv', 'evidence/optimization_comparison.tsv', 'evidence/run_manifest.toml', 'evidence/source_and_environment.json', 'examples/reconstruction.jl', 'julia-version', 'reference/Lean/Omega.lean', 'reference/Lean/Omega/Affine.lean', 'reference/Lean/Omega/AxiomAudit.lean', 'reference/Lean/Omega/Constants.lean', 'reference/Lean/Omega/Dimension.lean', 'reference/Lean/Omega/Extinction.lean', 'reference/Lean/Omega/Finite.lean', 'reference/Lean/Omega/Floor.lean', 'reference/Lean/Omega/Geometry.lean', 'reference/Lean/Omega/Interface.lean', 'reference/Lean/Omega/Ledger.lean', 'reference/Lean/Omega/Main.lean', 'reference/Lean/Omega/Metrics.lean', 'reference/Lean/Omega/Placement.lean', 'reference/Lean/PROOF_GUIDE.md', 'reference/Lean/README.md', 'reference/Lean/REPRODUCTION.md', 'reference/Lean/SHA256SUMS', 'reference/Lean/SOURCE_MAPPING.md', 'reference/Lean/evidence/axioms.log', 'reference/Lean/evidence/build.log', 'reference/Lean/evidence/setup_lake_update.log', 'reference/Lean/lake-manifest.json', 'reference/Lean/lakefile.lean', 'reference/Lean/lean-toolchain', 'reference/Lean/scripts/check_axioms.py', 'reference/Lean/scripts/lean_local.sh', 'reference/Lean/scripts/self_exe.c', 'reference/Lean/scripts/verify.sh', 'run_proofs.jl', 'scripts/check_inventory.jl', 'scripts/export_guides.jl', 'scripts/reproduce.jl', 'src/Dynamics.jl', 'src/ExactArithmetic.jl', 'src/Geometry.jl', 'src/OmegaNaughtProofs.jl', 'src/PolynomialCertificates.jl', 'src/ProofGuide.jl', 'src/Verification.jl'] EXPECTED_LABELS = ['phi_sq', 'sc_identity', 'one_arcsecond_cleared', 'shares_sum_cleared', 'mu_eq_one_sub_cleared', 'weighted_mean_cleared', 'displacement_conjugacy', 'affine_iterate_base', 'affine_iterate_step', 'homothety_comp', 'homothety_one', 'observation_commutes_after_linearity', 'arbitrary_intercept_defect', 'grid_interface_cleared', 'mark_distance_squared', 'inner_extension_offset', 'outer_extension_offset', 'negative_outer_extension_offset', 'total_extension_offset', 'chord_offset', 'sequential_upper_inner', 'sequential_upper_outer', 'sequential_lower_inner', 'sequential_lower_outer', 'G_eq', 'C_eq', 'W_eq', 'geometric_share_G_cleared', 'geometric_share_C_cleared', 'outline_length', 'reference_not_outline_positive_factor', 'marks_collinear_x', 'seeds_distinct_difference', 'seed_linear_combination_re_cleared', 'seed_linear_combination_im_cleared', 'seed_minor', 'moment_11', 'moment_12', 'moment_22', 'gram_entry_1_1', 'gram_entry_1_2', 'gram_entry_1_3', 'gram_entry_1_4', 'gram_entry_1_5', 'gram_entry_1_6', 'gram_entry_2_1', 'gram_entry_2_2', 'gram_entry_2_3', 'gram_entry_2_4', 'gram_entry_2_5', 'gram_entry_2_6', 'gram_entry_3_1', 'gram_entry_3_2', 'gram_entry_3_3', 'gram_entry_3_4', 'gram_entry_3_5', 'gram_entry_3_6', 'gram_entry_4_1', 'gram_entry_4_2', 'gram_entry_4_3', 'gram_entry_4_4', 'gram_entry_4_5', 'gram_entry_4_6', 'gram_entry_5_1', 'gram_entry_5_2', 'gram_entry_5_3', 'gram_entry_5_4', 'gram_entry_5_5', 'gram_entry_5_6', 'gram_entry_6_1', 'gram_entry_6_2', 'gram_entry_6_3', 'gram_entry_6_4', 'gram_entry_6_5', 'gram_entry_6_6', 'mark_dot', 'mark_radius_squared', 'seed_angle_cosine', 'triangle_area_signed_determinant', 'circle_speed_squared', 'arc_antiderivative_endpoints', 'mark_scale_re', 'mark_scale_im', 'circle_scale_re', 'circle_scale_im', 'placed_homothety_after_linearity', 'readout_scale_G', 'readout_scale_C', 'farey_determinant_identity', 'rational_residual_cleared', 'real_residual_after_euclidean', 'scalar_roundtrip', 'scalar_canonical_residual', 'ledger_one_step_cleared', 'ledger_weighted_induction', 'ledger_step_distribute', 'point_reconstruction_substitution'] POLY_PREFIX_SHA256 = '0e86d006d962623330153c14d179e02d7485e5824866a866670f0a1c59e58129' ARITHMETIC_SHA256 = 'dcadae591fd616aca154c834a584109c038fc0bd27b38e2a1a2244a62af6b380' def table(pkg, name, fields, keys, delimiter=','): with (pkg/'evidence/O3'/name).open(newline='') as stream: reader = csv.DictReader(stream, delimiter=delimiter) need(reader.fieldnames == fields, 'table schema: '+name) rows = list(reader) need(all(set(r) == set(fields) and all(v is not None for v in r.values()) for r in rows), 'malformed table: '+name) observed = [r[fields[0]] for r in rows] need(observed == [str(k) for k in keys], 'table coverage/order/duplicates: '+name) return rows def preflight(pkg): actual = sorted(str(p.relative_to(pkg)) for p in pkg.rglob('*') if p.is_file()) need(actual == EXPECTED_FILES, 'archive closed file inventory') table(pkg, 'state_certificate.csv', ['seed','successor','remainder','gap','extinction_depth','recovered_23_step_seed'], range(32768)) table(pkg, 'rational_enclosures.tsv', ['constant','lower_exact','upper_exact'], ['root','phi','pi','lam','mu','epsilon','delta','s','c','lambda_for_census'], '\t') table(pkg, 'precision_sweep.csv', ['decimal_places','numerator','denominator','mismatching_states'], range(19)) gaps = table(pkg, 'gap_blocks.csv', ['block','first_seed','last_seed','minimum_gap','minimum_seed'], range(128)) for i, row in enumerate(gaps): need(int(row['first_seed']) == 256*i and int(row['last_seed']) == 256*i+255, 'gap block interval: '+str(i)) table(pkg, 'polynomial_certificates.tsv', ['certificate','normal_form','evidence'], EXPECTED_LABELS, '\t') def expression(text, context): """Evaluate only exact arithmetic AST nodes from the specified Julia subset. No eval, exec, or sympify(string). List indexing explicitly uses Julia's one-based convention. Unsupported calls, attributes and comprehensions fail. """ tree = ast.parse(text.replace('^', '**'), mode='eval') def walk(node, env): if isinstance(node, ast.Constant) and type(node.value) is int: return sp.Integer(node.value) if isinstance(node, ast.Name): need(node.id in env, 'unknown expression name: '+node.id) return env[node.id] if isinstance(node, ast.UnaryOp) and isinstance(node.op, (ast.UAdd, ast.USub)): v = walk(node.operand, env) return v if isinstance(node.op, ast.UAdd) else -v if isinstance(node, ast.BinOp): a,b = walk(node.left, env),walk(node.right, env) if isinstance(node.op, ast.Add): return a+b if isinstance(node.op, ast.Sub): return a-b if isinstance(node.op, ast.Mult): return a*b if isinstance(node.op, ast.Div): need(isinstance(b, sp.Rational) and b != 0, 'nonconstant/zero denominator') return a/b if isinstance(node.op, ast.Pow): need(isinstance(b, sp.Integer) and 0 <= b <= 20, 'unsupported exponent') return a**b if isinstance(node, ast.List): return [walk(n,env) for n in node.elts] if isinstance(node, ast.Subscript): values, index = walk(node.value,env),walk(node.slice,env) need(isinstance(values,list) and isinstance(index,sp.Integer) and 1 <= index <= len(values), 'invalid one-based subscript') return values[int(index)-1] if isinstance(node, ast.ListComp): need(len(node.generators)==1, 'unsupported comprehension') g=node.generators[0] need(isinstance(g.target,ast.Name) and not g.ifs and not g.is_async, 'unsupported generator') values=walk(g.iter,env) need(isinstance(values,list), 'comprehension domain') return [walk(node.elt,dict(env,**{g.target.id:v})) for v in values] if isinstance(node, ast.Call) and isinstance(node.func,ast.Name) and not node.keywords: args=[walk(a,env) for a in node.args] if node.func.id=='sum': need(len(args)==1 and isinstance(args[0],list), 'sum arguments') return sum(args[0], sp.Integer(0)) need(node.func.id in ('Tk','H') and node.func.id in env, 'unsupported function') parameters, body=env[node.func.id] need(len(args)==len(parameters), 'function arity') return expression(body,dict(env,**dict(zip(parameters,args)))) raise ValueError('unsupported expression: '+ast.dump(node)) return walk(tree.body,context) def polynomial_expressions(pkg, Q, S): source=(pkg/'src/PolynomialCertificates.jl').read_text() need(source.count('function polynomial_certificates()')==1, 'polynomial entry point') prefix,body=source.split('function polynomial_certificates()',1) need(hashlib.sha256(prefix.encode()).hexdigest()==POLY_PREFIX_SHA256, 'unsupported polynomial prelude change') need(hashlib.sha256((pkg/'src/ExactArithmetic.jl').read_bytes()).hexdigest()==ARITHMETIC_SHA256, 'unsupported arithmetic dependency change') varnames='a phi pi s c z w x k l alpha b u v d f r h e A B t V An Bn ell'.split() ctx=dict(zip(varnames,sp.symbols(' '.join(varnames)))) ctx['q']=sp.Rational(Q,S) lines=[line.strip() for line in body.splitlines() if line.strip() and not line.strip().startswith('#')] declarations=[','.join(varnames)+' = variable.(POLY_VARS)', 'out=Pair{String,Poly}[]','put(name,p)=push!(out,name=>p)'] need(lines[:3]==declarations and lines[-2:]==['out','end'], 'polynomial scaffold') out={};seen=[];in_loop=False;loop_used=False for line in lines[3:-2]: if line=='for i in 1:6, j in 1:6': need(not in_loop and not loop_used, 'duplicate/nested polynomial loop') in_loop=True;loop_used=True;continue if line=='end': need(in_loop,'unexpected polynomial end');in_loop=False;continue m=re.fullmatch(r'put\("([^"\n]+)",(.*)\)',line) if m: name,body_expr=m.groups() pairs=[(i,j) for i in range(1,7) for j in range(1,7)] if in_loop else [(None,None)] need(('$' in name)==in_loop,'polynomial interpolation context') if in_loop: need(name=='gram_entry_$(i)_$(j)','unsupported interpolation') for i,j in pairs: key=name.replace('$(i)',str(i)).replace('$(j)',str(j)) need(key not in out,'duplicate polynomial certificate: '+key) local=ctx if i is None else dict(ctx,i=sp.Integer(i),j=sp.Integer(j)) out[key]=expression(body_expr,local) continue need(not in_loop,'unsupported loop body') m=re.fullmatch(r'(Tk|H)\(k,x\)=(.*)',line) if m: name,body_expr=m.groups();need(name not in ctx,'duplicate helper') ctx[name]=(('k','x'),body_expr) need(not any(isinstance(n,ast.Call) for n in ast.walk(ast.parse(body_expr.replace('^','**'),mode='eval'))), 'unsupported helper call') expression(body_expr,ctx) # Also validate unused helper definitions. seen.append(name);continue for part in line.split(';'): m=re.fullmatch(r'\s*(eps|delta|heights)=(.*)',part) need(m is not None,'unsupported polynomial source line: '+line) name,body_expr=m.groups();need(name not in ctx,'duplicate polynomial assignment') ctx[name]=expression(body_expr,ctx);seen.append(name) need(not in_loop and loop_used and seen==['eps','delta','Tk','H','heights'], 'polynomial dependency inventory') need(isinstance(ctx['heights'],list) and len(ctx['heights'])==6, 'height inventory') need(list(out)==EXPECTED_LABELS,'polynomial source inventory/order') return out,ctx def lean_without_comments(text): # Preserve line numbers; reject nested/unclosed unsupported lexemes rather # than accepting declarations accidentally found inside a comment. out=[];i=0;depth=0;quoted=False while i> 16) & 0o170000 == 0o120000, 'ZIP symlink') need(info.filename.startswith('OMEGA_NAUGHT_Julia_Proof_v0.1/'), 'unexpected ZIP root') target=(root/'julia'/info.filename).resolve() if not target.is_relative_to((root/'julia').resolve()): raise ValueError('Archive path escapes temporary directory') if not info.is_dir(): target.parent.mkdir(parents=True,exist_ok=True) target.write_bytes(archive.read(info)) pkg=root/'julia/OMEGA_NAUGHT_Julia_Proof_v0.1' preflight(pkg) _check(docx_path,pkg) def _check(docx_path,pkg): from pathlib import Path from zipfile import ZipFile import xml.etree.ElementTree as etree import re,hashlib,tomllib,csv,json,sys from fractions import Fraction as F ns={'w':'http://schemas.openxmlformats.org/wordprocessingml/2006/main'} with ZipFile(docx_path) as z: tree=etree.fromstring(z.read('word/document.xml')) blocks={}; current=None for el in tree.findall('.//w:p',ns): style_node=el.find('./w:pPr/w:pStyle',ns);style=style_node.get('{'+ns['w']+'}val','') if style_node is not None else '' text=''.join(t.text or '' for t in el.findall('.//w:t',ns)) if style=='ArchivePath' and text.startswith('OMEGA_NAUGHT_Lean_Proof_v0.1/'): current=text.split('/',1)[1] need(current not in blocks, 'duplicate DOCX source block: '+current) blocks[current]=[] elif style=='ArchiveText': need(current is not None, 'orphan DOCX source text') blocks[current].append(text) required={str(p.relative_to(pkg/'reference/Lean')) for p in (pkg/'reference/Lean').rglob('*') if p.is_file()} need(set(blocks)==required and len(blocks)==29, 'DOCX source block inventory') for name,lines in blocks.items(): original=(pkg/'reference/Lean'/name).read_bytes() got='\n'.join(lines).encode() if got!=original:raise ValueError(('DOCX bytes differ',name,len(got),len(original),repr(got[-30:]),repr(original[-30:]))) print('DOCX exact recovered files',len(blocks),'bytes',sum((pkg/'reference/Lean'/n).stat().st_size for n in blocks)) def manifests(base): listed=[] for line in (base/'SHA256SUMS').read_text().splitlines(): need(re.fullmatch(r'[0-9a-f]{64} [^\n]+',line) is not None, 'manifest line syntax') digest,name=line.split(maxsplit=1) need(name not in listed, 'duplicate manifest entry: '+name) need(name in {str(p.relative_to(base)) for p in base.rglob('*') if p.is_file() and p!=base/'SHA256SUMS'}, 'unexpected manifest path') listed.append(name) need(hashlib.sha256((base/name).read_bytes()).hexdigest()==digest, 'manifest hash: '+name) expected={str(p.relative_to(base)) for p in base.rglob('*') if p.is_file() and p!=base/'SHA256SUMS'} need(set(listed)==expected,'manifest closed inventory') return len(listed) print('Julia hash entries',manifests(pkg));print('Lean hash entries',manifests(pkg/'reference/Lean')) inv=tomllib.loads((pkg/'THEOREMS.toml').read_text()) declarations=theorem_declarations(pkg) names=set(declarations) entries=inv['theorem'];mapped={r['name'] for r in entries} need(inv['format_version']==1 and inv['theorem_count']==147 and len(entries)==147 and mapped==names, 'theorem inventory') for e in entries: need((e['source'],e['module'],e['line'],e['statement'],e['section_context'])==declarations[e['name']], 'theorem statement/name/source binding: '+e['name']) print('Theorem declarations and mappings',len(mapped)) for name in ['gap_blocks.csv','polynomial_certificates.tsv','precision_sweep.csv','rational_enclosures.tsv','results.toml','state_certificate.csv']: if (pkg/'evidence/O0'/name).read_bytes()!=(pkg/'evidence/O3'/name).read_bytes():raise ValueError(('optimization differs',name)) print('Archived O0/O3 outputs agree',6) Q,S=339949771344778,10**15 rows=list(csv.DictReader((pkg/'evidence/O3/state_certificate.csv').open())) depths=[];positive=0 for i,row in enumerate(rows): vals={k:int(v) for k,v in row.items()};n,r=divmod(Q*i,S);d=i;rs=[];depth=0 for _ in range(23): if d:depth+=1;positive+=1 d,rho=divmod(Q*d,S);rs.append(rho) recovered=d for rho in reversed(rs): recovered,rem=divmod(S*recovered+rho,Q) if rem:raise ValueError('reverse divisibility') expected={'seed':i,'successor':n,'remainder':r,'gap':S-r,'extinction_depth':depth,'recovered_23_step_seed':recovered} if vals!=expected or recovered!=i or d!=0:raise ValueError(('row',i)) depths.append(depth) if len(rows)!=32768:raise ValueError('rows') print('Fresh Python integer replay',len(rows),'states',len(rows)*23,'transitions','depth',max(depths),'sum',sum(depths),'positive',positive) print('Minimum gap',min(int(r['gap']) for r in rows)) from pathlib import Path from fractions import Fraction as F from math import isqrt,factorial import csv,re,sys sys.set_int_max_str_digits(100000) import sympy as sp def atan(b,digits): x=F(1,b);power=x;total=F(0);j=0;target=F(1,10**(digits+3)) while True: total+=(-1)**j*power/(2*j+1);j+=1;power*=x*x;nxt=(-1)**j*power/(2*j+1) if abs(nxt)