mutable struct Audit
    counts::Dict{String,Int}
end
Audit()=Audit(Dict{String,Int}())
function check!(audit::Audit, group::String, condition::Bool, detail::AbstractString="")
    condition || error("FAILED [$group] $detail")
    audit.counts[group]=get(audit.counts,group,0)+1
    nothing
end
function rejects!(audit,group,f)
    rejected=false
    try
        f()
    catch e
        (e isa DomainError || e isa ArgumentError || e isa DimensionMismatch) || rethrow()
        rejected=true
    end
    check!(audit,group,rejected,"invalid input was accepted")
end
rattext(x::Rational)="$(numerator(x))/$(denominator(x))"

function verify_inventory!(audit,root)
    ref=joinpath(root,"reference","Lean")
    count=0
    for line in eachline(joinpath(ref,"SHA256SUMS"))
        isempty(strip(line)) && continue
        fields=split(line;limit=2)
        expected=fields[1]; path=strip(fields[2])
        startswith(path,"*") && (path=path[2:end])
        actual=bytes2hex(sha256(read(joinpath(ref,path))))
        check!(audit,"source_inventory",actual==expected,path)
        count+=1
    end
    entries=TOML.parsefile(joinpath(root,"THEOREMS.toml"))["theorem"]
    expected=Dict{String,String}()
    for file in sort(readdir(joinpath(ref,"Omega")))
        endswith(file,".lean") || continue
        source=read(joinpath(ref,"Omega",file),String)
        prefix=file=="Ledger.lean" ? "Omega.Ledger." : "Omega."
        for m in eachmatch(r"(?ms)^theorem\s+([A-Za-z_][A-Za-z_0-9]*)(.*?)\s*:=",source)
            expected[prefix*m.captures[1]]=strip(first(split(m.match,":=";limit=2)))
        end
    end
    names=String[e["name"] for e in entries]
    check!(audit,"theorem_coverage",length(names)==147 && length(unique(names))==147,"147 unique mappings")
    check!(audit,"theorem_coverage",Set(names)==Set(keys(expected)),"source theorem-name equality")
    for e in entries
        check!(audit,"theorem_coverage",e["statement"]==expected[e["name"]],e["name"]*" declaration text")
        check!(audit,"theorem_coverage",haskey(PROOFS,e["chapter"]),e["name"]*" proof chapter")
        check!(audit,"theorem_coverage",!isempty(e["proof_step"]),e["name"]*" proof step")
    end
    (source_hash_entries=count,theorems=length(names))
end

function verify_constants!(audit,outdir)
    cs=constants_enclosure(;digits=100)
    den=big(10)^20
    pl=rational(big"161803398874989484820",den)
    pu=rational(big"161803398874989484821",den)
    pil=rational(big"314159265358979323846",den)
    piu=rational(big"314159265358979323847",den)
    check!(audit,"rational_enclosures",pl^2-pl-1<0<pu^2-pu-1,"golden quadratic endpoint signs")
    check!(audit,"rational_enclosures",pl<cs.phi.lo<cs.phi.hi<pu,"phi 20-decimal enclosure")
    check!(audit,"rational_enclosures",pil<cs.pi.lo<cs.pi.hi<piu,"pi 20-decimal enclosure")
    check!(audit,"rational_enclosures",cs.root.lo^2<=5<cs.root.hi^2,"isqrt endpoints")
    check!(audit,"rational_enclosures",0<q<cs.lam.lo<cs.lam.hi<q+1//S<1,"strict lambda enclosure")
    check!(audit,"rational_enclosures",LOWER<q<UPPER && LOWER<cs.lam.lo<cs.lam.hi<UPPER,"parameter interval")
    check!(audit,"rational_enclosures",0<cs.delta.lo<cs.delta.hi<cs.pi.lo/2,"seed interval")
    check!(audit,"rational_enclosures",0<cs.s.lo<=cs.s.hi<1 && 0<cs.c.lo<=cs.c.hi<=1,"Taylor sign enclosures")
    check!(audit,"rational_enclosures",rational(648000)*cs.epsilon.lo==cs.pi.lo,"arcsecond definition")
    tan2=2*rational(1,5)/(1-rational(1,5)^2)
    tan4=2*tan2/(1-tan2^2)
    check!(audit,"rational_enclosures",tan2==5//12 && tan4==120//119,"Machin tangent doubling")
    check!(audit,"rational_enclosures",(tan4-1//239)/(1+tan4/239)==1,"Machin tangent subtraction")
    check!(audit,"rational_enclosures",0<4*rational(1,5)/(1+rational(1,5)^2)-1//239<4//5<cs.pi.lo/2,"Machin branch inequalities")
    # Coarsen the proven interval outward, reducing the cost of the full census.
    M=big(10)^36
    lam=Interval(floor_rat(cs.lam.lo*M)//M,ceil_rat(cs.lam.hi*M)//M)
    check!(audit,"rational_enclosures",lam.lo<=cs.lam.lo<=cs.lam.hi<=lam.hi,"outward rational coarsening")
    check!(audit,"rational_enclosures",q<lam.lo<lam.hi<q+1//S && LOWER<lam.lo<lam.hi<UPPER,"coarsened margins")
    open(joinpath(outdir,"rational_enclosures.tsv"),"w") do io
        println(io,"constant\tlower_exact\tupper_exact")
        for name in (:root,:phi,:pi,:lam,:mu,:epsilon,:delta,:s,:c)
            v=getproperty(cs,name)
            println(io,"$name\t$(rattext(v.lo))\t$(rattext(v.hi))")
        end
        println(io,"lambda_for_census\t$(rattext(lam.lo))\t$(rattext(lam.hi))")
    end
    (constants=cs,lambda=lam)
end

function verify_polynomials!(audit,outdir)
    phi=variable(:phi);s=variable(:s);c=variable(:c);x=variable(:x);z=variable(:z)
    check!(audit,"normalizer_controls",iszero(phi^2-phi-1) && iszero(s^2+c^2-1),"defining substitutions")
    check!(audit,"normalizer_controls",!iszero(phi^2-phi) && !iszero(c^2+s^2),"nonzero controls")
    check!(audit,"normalizer_controls",(x+z)^3==x^3+3*x^2*z+3*x*z^2+z^3,"independent expansion")
    check!(audit,"normalizer_controls",!iszero(x-z),"independent variables")
    certs=polynomial_certificates()
    check!(audit,"normalizer_controls",length(unique(first.(certs)))==length(certs),"unique certificate labels")
    open(joinpath(outdir,"polynomial_certificates.tsv"),"w") do io
        println(io,"certificate\tnormal_form\tevidence")
        for (name,residual) in certs
            check!(audit,"symbolic_polynomials",iszero(residual),name)
            println(io,"$name\t$residual\texact polynomial reduction; side conditions in analytic proof")
        end
    end
    length(certs)
end

function verify_finite_domain!(audit,lam,outdir)
    successors=BigInt[F(d) for d in 0:DOMAIN_SIZE-1]
    remainders=BigInt[rho(d) for d in 0:DOMAIN_SIZE-1]
    lower=maximum(successors[d+1]//big(d) for d in 1:DOMAIN_SIZE-1)
    upper=minimum((successors[d+1]+1)//big(d) for d in 1:DOMAIN_SIZE-1)
    check!(audit,"exact_interval",lower==LOWER && upper==UPPER,"intersection of every floor constraint")
    check!(audit,"exact_interval",7039*12343-4196*20706==1,"Farey determinant")
    check!(audit,"exact_interval",20706+12343==33049 && 33049>DOMAIN_SIZE-1,"forbidden-boundary bound")
    check!(audit,"exact_interval",F(12343)==4196 && F(20706)==7038,"necessity witnesses")
    check!(audit,"modular_inverse",gcd(Q,S)==2,"gcd")
    check!(audit,"modular_inverse",div(Q,2)*MODULAR_INVERSE==1+big(95668581631527)*PERIOD,"integer inverse identity")
    check!(audit,"modular_inverse",length(unique(remainders))==DOMAIN_SIZE,"distinct first remainders")
    ts=extinction_thresholds(10)
    check!(audit,"extinction",ts==BigInt[1,3,9,27,80,236,695,2045,6016,17697,52058],"threshold recurrence")
    depths=zeros(Int,DOMAIN_SIZE); transitions=0;positive=0;zero=0
    open(joinpath(outdir,"state_certificate.csv"),"w") do io
        println(io,"seed,successor,remainder,gap,extinction_depth,recovered_23_step_seed")
        for d in 0:DOMAIN_SIZE-1
            f=successors[d+1];r=remainders[d+1]
            check!(audit,"finite_floor",Q*d==S*f+r && 0<=r<S,"Euclidean division at $d")
            check!(audit,"finite_floor",floor_rat(lam.lo*d)==f && floor_rat(lam.hi*d)==f,"enclosed real floor at $d")
            check!(audit,"finite_floor",floor_rat(LOWER*d)==f,"included lower endpoint at $d")
            check!(audit,"finite_floor",d==0 || ceil_rat(UPPER*d)-1==f,"excluded upper endpoint constraint at $d")
            check!(audit,"finite_floor",0<=f<=d && (d==0 || f<d),"invariance and contraction at $d")
            check!(audit,"finite_gap",S-r>=big(34535026732) && S*(lam.hi-q)*d<S-r,"gap at $d")
            check!(audit,"modular_inverse",iseven(r) && div(r,2)==mod(div(Q,2)*d,PERIOD),"halved remainder")
            check!(audit,"modular_inverse",seed_from_remainder(r)==d,"single-remainder decoding at $d")
            check!(audit,"scalar_external",scalar_encode(S,Q*d)==(integer=f,residual=r//big(1)),"external factorization")
            check!(audit,"residual_types",q*d-f==r//S,"rational residual")
            check!(audit,"residual_types",d==0 || (lam.lo-q)*d>0,"positive real correction")
            rec=encode(Q,S,23,d)
            restored=recover(Q,S,rec.terminal,rec.remainders)
            check!(audit,"canonical_ledger",restored==d && rec.terminal==0 && length(rec.remainders)==23,"23-step roundtrip")
            check!(audit,"canonical_ledger",admissible(Q,S,rec.terminal,rec.remainders),"generated record admissibility")
            check!(audit,"canonical_ledger",Q^23*d==S^23*rec.terminal+ledger_value(Q,S,rec.remainders),"ordered polynomial identity")
            # Reconstruct every retained state backwards, and compare with the
            # actual forward record. This checks the complete state trajectory.
            back=Vector{BigInt}(undef,24);back[24]=rec.terminal
            for j in 23:-1:1
                numerator=S*back[j+1]+rec.remainders[j]
                check!(audit,"canonical_trajectory",mod(numerator,Q)==0,"reverse divisibility")
                back[j]=div(numerator,Q)
            end
            x=big(d);depth=0
            for j in 1:23
                transitions+=1
                x>0 ? (positive+=1;depth+=1) : (zero+=1)
                check!(audit,"canonical_trajectory",x==back[j] && rho(x)==rec.remainders[j],"state/remainder equality")
                x=F(x)
            end
            check!(audit,"canonical_trajectory",x==back[24]==0,"terminal equality")
            depths[d+1]=depth
            for n in 0:10
                # Once extinct, every further iterate is zero. The complete
                # recorded trajectory makes this an exact state comparison.
                check!(audit,"extinction",(back[n+1]==0)==(d<ts[n+1]),"threshold at state $d, depth $n")
            end
            println(io,"$d,$f,$r,$(S-r),$depth,$restored")
        end
    end
    gap=minimum(S .- remainders)
    check!(audit,"finite_gap",gap==34535026732 && S-rho(20706)==gap,"minimum and witness")
    check!(audit,"finite_gap",32767<gap,"finite certificate margin")
    open(joinpath(outdir,"gap_blocks.csv"),"w") do io
        println(io,"block,first_seed,last_seed,minimum_gap,minimum_seed")
        for b in 0:127
            inds=256*b+1:256*b+256
            g=S .- remainders[inds];j=argmin(g)
            check!(audit,"finite_blocks",minimum(g)>=gap,"block $b")
            println(io,"$b,$(first(inds)-1),$(last(inds)-1),$(g[j]),$(first(inds)+j-2)")
        end
    end
    check!(audit,"census",transitions==753664 && positive==300871 && zero==452793,"transition totals")
    check!(audit,"census",maximum(depths)==10 && sum(depths)==300871,"extinction totals")
    check!(audit,"census",findall(==(10),depths).-1==collect(17697:32767),"deepest seeds")
    check!(audit,"census",length(unique(successors))==11140,"distinct successors")
    (states=DOMAIN_SIZE,transitions=transitions,positive_transitions=positive,zero_transitions=zero,
     maximum_depth=maximum(depths),sum_depths=sum(depths),minimum_gap=string(gap),
     mean_depth="300871/32768",gap_blocks=128)
end

function verify_precision!(audit,lam,outdir)
    mismatch=Int[];lastq=rational(-1)
    open(joinpath(outdir,"precision_sweep.csv"),"w") do io
        println(io,"decimal_places,numerator,denominator,mismatching_states")
        for p in 0:18
            qp=certified_truncation(p)
            check!(audit,"precision",lastq<=qp<=lam.hi && qp<UPPER,"truncation monotonicity/bounds")
            m=count(d->floor_rat(qp*d)!=F(d),0:DOMAIN_SIZE-1)
            check!(audit,"precision",(m==0)==(p>=8),"finite sweep precision $p")
            p==6 && check!(audit,"precision",m==414,"six-place count")
            p==7 && check!(audit,"precision",m==39 && qp==3399497//big(10)^7 && qp<LOWER,"seven-place threshold")
            p==8 && check!(audit,"precision",qp==33994977//big(10)^8 && LOWER<=qp,"eight-place threshold")
            push!(mismatch,m);lastq=qp
            println(io,"$p,$(numerator(qp)),$(denominator(qp)),$m")
        end
    end
    square=26*lam^2
    check!(audit,"rounding_counterexample",F(26)==8 && F(F(26))==2 && 3<square.lo<=square.hi<4,"d=26")
    mismatch
end

function verify_generic_ledgers!(audit)
    cases=0
    for A in -7:7,B in -5:5,d in -30:30
        step=ledger_step(A,B,d);r=ledger_remainder(A,B,d)
        check!(audit,"signed_division",big(B)*step+r==big(A)*d,"all divisor signs")
        B!=0 && check!(audit,"signed_division",0<=r<abs(B),"absolute-divisor remainder bound")
        for n in 0:5
            cases+=1;rec=encode(A,B,n,d)
            check!(audit,"generic_ledger",length(rec.remainders)==n,"length")
            A!=0 && check!(audit,"generic_ledger",recover(A,B,rec.terminal,rec.remainders)==d,"nonzero A, arbitrary B")
            if B>0
                hv=admissible(A,B,rec.terminal,rec.remainders)
                A!=0 && check!(audit,"generic_ledger",hv,"generated admissibility")
                if hv
                    restored=recover(A,B,rec.terminal,rec.remainders)
                    check!(audit,"generic_ledger",encode(A,B,n,restored)==rec,"admissible recovery including A=0")
                    check!(audit,"generic_ledger",big(A)^n*restored==big(B)^n*rec.terminal+ledger_value(A,B,rec.remainders),"weighted identity")
                end
            end
        end
    end
    # Independently enumerate image records on a provably sufficient seed range.
    # For |t|<=3, every valid reverse step has |d| <= (B|t|+B-1)/|A|.
    # Recursing this bound includes every possible admissible preimage below.
    candidate_count=0;valid_count=0
    for A in [-3,-2,-1,1,2,3],B in 1:4,n in 0:3
        bound=big(3)
        for _ in 1:n;bound=cld(B*bound+B-1,abs(A));end
        images=Dict{Tuple{BigInt,Tuple},Int}()
        for d in -bound:bound
            rec=encode(A,B,n,d);key=(rec.terminal,Tuple(rec.remainders))
            images[key]=get(images,key,0)+1
        end
        for t in -3:3, tup in Iterators.product(ntuple(_->(-1:B),n)...)
            candidate_count+=1;rs=BigInt[tup...]
            hv=admissible(A,B,t,rs)
            multiplicity=get(images,(big(t),Tuple(rs)),0)
            check!(audit,"admissible_candidates",hv==(multiplicity==1),"admissibility iff unique bounded preimage")
            check!(audit,"admissible_candidates",multiplicity<=1,"unique encoding")
            if hv
                valid_count+=1;x=decode_checked(A,B,t,rs)
                check!(audit,"admissible_candidates",encode(A,B,n,x)==(terminal=big(t),remainders=rs),"candidate re-encoding")
            end
        end
    end
    # B>0 alone is enough for the source's admissible_roundtrip, including A=0.
    for B in 1:4,t in -3:3,n in 0:3,tup in Iterators.product(ntuple(_->(-1:B),n)...)
        rs=BigInt[tup...]
        if admissible(0,B,t,rs)
            check!(audit,"zero_multiplier_admissibility",encode(0,B,n,recover(0,B,t,rs))==(terminal=big(t),remainders=rs),"A=0 weaker hypothesis")
        end
    end
    for A in -5:5,B in 1:5,d in -15:15,e in -8:8
        check!(audit,"predecessor_inequalities",(ledger_step(A,B,d)==e)==(B*e<=A*d<B*(e+1)),"signed predecessor inequalities")
    end
    rec=encode(2,3,3,17)
    check!(audit,"ordered_data",rec.remainders!=reverse(rec.remainders),"order witness has distinct order")
    check!(audit,"ordered_data",!admissible(2,3,rec.terminal,reverse(rec.remainders)) ||
        recover(2,3,rec.terminal,reverse(rec.remainders))!=17,"reordering is not a lossless operation")
    rejects!(audit,"input_validation",()->decode_checked(0,3,0,BigInt[]))
    rejects!(audit,"input_validation",()->decode_checked(2,0,0,BigInt[]))
    rejects!(audit,"input_validation",()->decode_checked(2,3,0,BigInt[1]))
    rejects!(audit,"input_validation",()->seed_from_remainder(1))
    rejects!(audit,"input_validation",()->F(-1))
    # Exact probes beyond D exercise the full-period formula, without being
    # mislabeled as exhaustive enumeration of 500 trillion seeds.
    probes=BigInt[0,1,32767,32768,PERIOD-2,PERIOD-1]
    for d in probes
        check!(audit,"full_period_probes",seed_from_remainder(rho(d))==d,"full-period endpoint probe")
        check!(audit,"full_period_probes",rho(d+PERIOD)==rho(d),"periodicity")
    end
    (generated_cases=cases,candidate_records=candidate_count,admissible_candidates=valid_count,full_period_probes=length(probes))
end

function verify_realization!(audit)
    scalars=0;grids=0;placements=0
    for h in [rational(-3,2),rational(0),rational(1,8),rational(7,3)],y in [rational(i,7) for i in -21:21]
        er=scalar_encode_total(h,y);scalars+=1
        check!(audit,"scalar_coordinates",scalar_decode(h,er.integer,er.residual)==y,"total scalar roundtrip")
        if h>0
            check!(audit,"scalar_coordinates",0<=er.residual<h,"canonical residual bounds")
            check!(audit,"scalar_coordinates",scalar_encode(h,scalar_decode(h,er.integer,er.residual))==er,"two-way coordinate change")
        end
    end
    for h in [rational(1,8),rational(7,3)],e in -10:10,frac in [rational(0),rational(1,3),rational(999,1000)]
        check!(audit,"scalar_coordinates",scalar_encode(h,h*e+h*frac)==(integer=big(e),residual=h*frac),"arbitrary canonical pairs")
    end
    for k in -15:15
        h=k>=0 ? rational(big(2)^k) : rational(1,big(2)^(-k))
        for d in [0,1,2,26,12343,17697,20706,32767]
            y=h*d
            for n in 0:23
                grids+=1
                check!(audit,"grid_realization",y==h*iterate_state(d,n),"retained grid scale and depth")
                check!(audit,"grid_realization",certified_lambda_grid_step(h,y)==rational_grid_step(h,y),"certified grid interface")
                y=certified_lambda_grid_step(h,y)
            end
        end
    end
    frames=[ExactPlacement([0,0],[1 0;0 1]),
            ExactPlacement([2,-3,5],[3//5 0;4//5 0;0 1]),
            ExactPlacement([1,2,3,4],[0 0;1 0;0 -1;0 0])]
    c=variable(:c);levels=symbolic_heights()
    for p in frames,a in [rational(1,32768),rational(3,2),rational(32768)]
        marks=placed_marks(a,p);placements+=1
        for i in 1:6,j in 1:6
            dotp=sum((marks[i][k]-p.center[k])*(marks[j][k]-p.center[k]) for k in eachindex(p.center))
            dist2=sum((marks[i][k]-marks[j][k])^2 for k in eachindex(p.center))
            check!(audit,"placement_polynomials",dotp==a^2*(c^2+levels[i]*levels[j]),"placed dot product")
            check!(audit,"placement_polynomials",dist2==a^2*(levels[i]-levels[j])^2,"placed distance squared")
        end
        for d in [0,26,32767]
            rec=encode(Q,S,23,d)
            check!(audit,"outline_reconstruction",reconstruct_outline(a,p,rec.terminal,rec.remainders)==outline_spec(a*d,p),"retained center/frame/radius")
        end
    end
    rejects!(audit,"input_validation",()->ExactPlacement([0,0],[1 1;0 1]))
    rejects!(audit,"input_validation",()->scalar_encode(0,1))
    rejects!(audit,"input_validation",()->certified_lambda_grid_step(1,1//2))
    rejects!(audit,"input_validation",()->certified_lambda_grid_step(1,32768))
    (scalar_examples=scalars,grid_states_at_scales=grids,placements=placements)
end

function verify_numerical_examples!(audit)
    # These are expressly illustrations, never premises of any exact certificate.
    count=0
    setprecision(BigFloat,256) do
        tol=BigFloat(2)^(-180)
        for k in -15:15
            a=k>=0 ? rational(big(2)^k) : rational(1,big(2)^(-k))
            g=numerical_geometry(a);av=BigFloat(a);count+=1
            check!(audit,"numerical_illustration",abs(g.G/(av*g.phi)-1)<tol,"outer metric numerical example")
            check!(audit,"numerical_illustration",abs(g.C/(av*g.pi)-1)<tol,"semicircle numerical example")
            check!(audit,"numerical_illustration",abs(g.lambda-g.phi/(g.phi+g.pi))<tol,"normalized example")
            check!(audit,"numerical_illustration",abs(abs(g.marks[4]-g.marks[3])/(2*av*g.s)-1)<tol,"seed chord example")
        end
    end
    count
end

function run_all(output_dir::AbstractString=joinpath(@__DIR__,"..","evidence","fresh"))
    root=normpath(joinpath(@__DIR__,".."));mkpath(output_dir);audit=Audit()
    println("OMEGA NAUGHT Julia proof companion v0.1")
    println("Julia ",VERSION," | ",Sys.KERNEL," ",Sys.ARCH," | ",Sys.MACHINE)
    println("Exact certificates use BigInt/Rational arithmetic; analytic proofs are literate text.")
    inventory=verify_inventory!(audit,root);println("Source inventory and 147 theorem mappings verified.")
    enclosures=verify_constants!(audit,output_dir);println("Exact rational enclosures verified (Machin identity and integer square root).")
    polys=verify_polynomials!(audit,output_dir);println("Exact polynomial certificates: ",polys)
    census=verify_finite_domain!(audit,enclosures.lambda,output_dir);println("Full domain: ",census.states," seeds; ",census.transitions," transitions; all records reconstructed.")
    precision=verify_precision!(audit,enclosures.lambda,output_dir);println("Precision sweep 0:18 verified; universal threshold proof is P08.")
    ledger=verify_generic_ledgers!(audit);println("Generic signed ledgers: ",ledger.generated_cases," generated cases; ",ledger.candidate_records," candidate records.")
    realization=verify_realization!(audit);println("Exact scalar, grid, frame, and outline realization checks completed.")
    numerical=verify_numerical_examples!(audit);println("Separate BigFloat illustrations: ",numerical)
    result=Dict{String,Any}(
        "status"=>"all configured checks completed",
        "julia_version"=>string(VERSION),"kernel"=>string(Sys.KERNEL),"architecture"=>string(Sys.ARCH),
        "machine"=>Sys.MACHINE,"word_size"=>Sys.WORD_SIZE,"threads"=>Threads.nthreads(),
        "proof_boundary"=>"Julia exact/symbolic/finite certificates plus analytic proof text; not a Lean kernel proof",
        "source_inventory"=>Dict(string(k)=>v for (k,v) in pairs(inventory)),
        "census"=>Dict(string(k)=>v for (k,v) in pairs(census)),
        "generic_ledgers"=>Dict(string(k)=>v for (k,v) in pairs(ledger)),
        "realization"=>Dict(string(k)=>v for (k,v) in pairs(realization)),
        "polynomial_certificates"=>polys,"precision_mismatch_counts_p0_to_p18"=>precision,
        "checks_by_evidence_group"=>audit.counts,"numerical_example_count"=>numerical)
    open(joinpath(output_dir,"results.toml"),"w") do io; TOML.print(io,result;sorted=true);end
    println("Completed checks by group:")
    for group in sort(collect(keys(audit.counts)));println("  ",group,": ",audit.counts[group]);end
    println("No Julia check failed. Universal analytic inferences are documented, not kernel-checked by Julia.")
    result
end