#!/usr/bin/env python3
"""TGA 2.0: a small typed witness checker, not a general theorem prover.

Python 3.10+, standard library only. Explicit checks remain active under -O.
Trusted base: this file, Python integer/Fraction arithmetic, and the analytic
schemas documented in PROOFS.md. Numerical tests never mint proof certificates.
"""
from __future__ import annotations
import argparse
import ast
import cmath
from dataclasses import dataclass, asdict, replace
from enum import Enum
from fractions import Fraction as F
from functools import lru_cache
import hashlib
import json
import math
from pathlib import Path
from typing import Any

Q, S, DSTAR = 339949771344778, 10**15, 42189065
PHI = (1 + math.sqrt(5)) / 2
LAMBDA = PHI / (PHI + math.pi)
BETA_EXPR = 'phi/(phi+pi)'
LABELS = ('d2', 'd1', 'd', 'b', 'b1', 'b2')

class Reject(ValueError):
    pass

def need(condition: bool, message: str) -> None:
    if not condition:
        raise Reject(message)

class Relation(Enum):
    IDENTITY = 'IDENTITY'
    PARAMETER_IDENTIFICATION = 'PARAMETER_IDENTIFICATION'
    EQUIVALENCE = 'EQUIVALENCE'
    EMBEDDING = 'EMBEDDING'
    DOMAIN_RESTRICTED_EQUIVALENCE = 'DOMAIN_RESTRICTED_EQUIVALENCE'
    LOSSY_PROJECTION = 'LOSSY_PROJECTION'
    APPROXIMATION = 'APPROXIMATION'

class Support(Enum):
    EXACT_CERTIFICATE = 'EXACT_CERTIFICATE'
    TRUSTED_ANALYTIC_SCHEMA = 'TRUSTED_ANALYTIC_SCHEMA'
    EXPLICIT_DECLARATION = 'EXPLICIT_DECLARATION'
    EXACT_COLLISION = 'EXACT_COLLISION'
    NUMERICAL_TEST_ONLY = 'NUMERICAL_TEST_ONLY'
    EXTERNAL_REFERENCE_ONLY = 'EXTERNAL_REFERENCE_ONLY'

@dataclass(frozen=True)
class TypeSpec:
    name: str
    dimension: int | None = None
    labels: tuple[str, ...] = ()
    convention: tuple[str, ...] = ()

@dataclass(frozen=True)
class Contract:
    preserves: tuple[str, ...]
    loses: tuple[str, ...]
    requires: tuple[str, ...]
    exact: bool  # mathematical formula, not arithmetic implementation
    reversible: bool  # certified on the specified image/domain
    domain: str

@dataclass(frozen=True)
class Witness:
    checker: str
    support: Support
    claim_digest: str
    payload: str  # canonical JSON; data only, never executed

@dataclass(frozen=True)
class Alignment:
    left: str
    right: str
    relation: Relation
    witness: Witness
    contract: Contract

@dataclass(frozen=True)
class InverseContract:
    map_id: str
    source: TypeSpec
    target: TypeSpec
    domain: str
    left_inverse: str
    right_inverse_on_image: str

@dataclass(frozen=True)
class MapSpec:
    id: str
    source: TypeSpec
    target: TypeSpec
    formula: str
    implementation: str  # closed dispatch name; not arbitrary code
    arithmetic: str
    inverse: InverseContract | None
    alignment: Alignment

@dataclass(frozen=True)
class Certificate:
    edge_id: str
    support: Support
    claim_digest: str
    evidence: str
    mathematical_status: str

@dataclass(frozen=True)
class Claim:
    id: str
    kind: str
    expression: str
    constants: tuple[str, ...]

@dataclass(frozen=True)
class Proposal:
    left: str
    right: str
    reason: str
    admitted: bool = False


def plain(x: Any) -> Any:
    if isinstance(x, Enum):
        return x.value
    if isinstance(x, F):
        return f'{x.numerator}/{x.denominator}'
    if isinstance(x, complex):
        return {'real': x.real, 'imag': x.imag}
    if hasattr(x, '__dataclass_fields__'):
        return {k: plain(v) for k, v in asdict(x).items()}
    if isinstance(x, dict):
        return {str(k): plain(v) for k, v in x.items()}
    if isinstance(x, (tuple, list)):
        return [plain(v) for v in x]
    return x


def canonical(x: Any) -> str:
    return json.dumps(plain(x), sort_keys=True, separators=(',', ':'), allow_nan=False)


def digest(x: Any) -> str:
    return hashlib.sha256(canonical(x).encode()).hexdigest()

# Exact normalization in Q(sqrt(5)); no Python eval or user-supplied callbacks.
@dataclass(frozen=True)
class Golden:
    a: F = F(0)
    b: F = F(0)

    def __add__(self, y: Golden) -> Golden:
        return Golden(self.a+y.a, self.b+y.b)

    def __neg__(self) -> Golden:
        return Golden(-self.a, -self.b)

    def __sub__(self, y: Golden) -> Golden:
        return self + (-y)

    def __mul__(self, y: Golden) -> Golden:
        return Golden(self.a*y.a+5*self.b*y.b, self.a*y.b+self.b*y.a)

    def __truediv__(self, y: Golden) -> Golden:
        norm=y.a*y.a-5*y.b*y.b
        need(norm != 0, 'division by zero in Q(sqrt(5))')
        return self * Golden(y.a/norm, -y.b/norm)


def normalize(expression: str) -> Golden:
    need(isinstance(expression, str) and len(expression) <= 300, 'expression size')
    tree=ast.parse(expression, mode='eval')
    need(len(list(ast.walk(tree))) <= 100, 'expression complexity')
    def visit(n: ast.AST) -> Golden:
        if isinstance(n, ast.Constant) and type(n.value) is int:
            need(abs(n.value) < 10**50, 'integer too large')
            return Golden(F(n.value))
        if isinstance(n, ast.Name) and n.id == 'phi':
            return Golden(F(1,2), F(1,2))
        if isinstance(n, ast.Name) and n.id == 'sqrt5':
            return Golden(F(0), F(1))
        if isinstance(n, ast.UnaryOp) and isinstance(n.op, (ast.UAdd, ast.USub)):
            y=visit(n.operand)
            return -y if isinstance(n.op, ast.USub) else y
        if isinstance(n, ast.BinOp):
            x,y=visit(n.left),visit(n.right)
            if isinstance(n.op, ast.Add): return x+y
            if isinstance(n.op, ast.Sub): return x-y
            if isinstance(n.op, ast.Mult): return x*y
            if isinstance(n.op, ast.Div): return x/y
        raise Reject('unsupported syntax; use rational arithmetic, phi, sqrt5')
    return visit(tree.body)


def propose(claims: tuple[Claim, ...]) -> tuple[Proposal, ...]:
    return tuple(Proposal(a.id,b.id,'same declared kind and shared symbols; not proof')
        for i,a in enumerate(claims) for b in claims[i+1:]
        if a.kind == b.kind and set(a.constants) & set(b.constants))

# Bounds and floor sums: exact rational certificate, no float decisions.
def arctan_bounds(inv: int, terms: int=100) -> tuple[F,F]:
    need(inv>1 and terms>0, 'arctan arguments')
    total=sum((F((-1)**k, (2*k+1)*inv**(2*k+1)) for k in range(terms)), F(0))
    nxt=total+F((-1)**terms, (2*terms+1)*inv**(2*terms+1))
    return min(total,nxt), max(total,nxt)


def floor_sum(n: int, m: int, a: int, b: int=0) -> int:
    """sum floor((a*i+b)/m), i=0..n-1, n,a,b>=0, m>0."""
    need(n>=0 and m>0 and a>=0 and b>=0, 'floor_sum domain')
    ans=0
    while True:
        qa,a=divmod(a,m); qb,b=divmod(b,m)
        ans += qa*n*(n-1)//2+qb*n
        y=a*n+b
        if y<m: return ans
        n,b=divmod(y,m)
        m,a=a,m


def sf(n: int, x: F) -> int:
    return floor_sum(n,x.denominator,x.numerator)


@lru_cache(maxsize=1)
def _boundary_certificate_json() -> str:
    # Machin: 16 atan(1/5) - 4 atan(1/239) = pi.
    # Tangent identity and branch are justified in PROOFS.md.
    a,b=arctan_bounds(5); c,d=arctan_bounds(239)
    pi_lo,pi_hi=16*a-4*d,16*b-4*c
    scale=10**80; root=math.isqrt(5*scale*scale)
    sqrt_lo,sqrt_hi=F(root,scale),F(root+1,scale)
    need(sqrt_lo**2<5<sqrt_hi**2, 'sqrt enclosure')
    phi_lo,phi_hi=(1+sqrt_lo)/2,(1+sqrt_hi)/2
    lo=phi_lo/(phi_lo+pi_hi); hi=phi_hi/(phi_hi+pi_lo)
    q=F(Q,S)
    need(q<lo<hi<1, 'lambda enclosure ordering')
    sums=(sf(DSTAR,q),sf(DSTAR,lo),sf(DSTAR,hi))
    need(sums[0]==sums[1]==sums[2], 'prefix floor sums disagree')
    at=(Q*DSTAR//S,(lo*DSTAR).__floor__(),(hi*DSTAR).__floor__())
    need(at==(14342162,14342163,14342163), 'first disagreement witness')
    need(hi-q<F(1,10**15), 'approximation bound')
    return canonical({'domain':{'kind':'integer_interval','lower':0,'upper_exclusive':DSTAR},
        'q':str(q),'lambda_lower':str(lo),'lambda_upper':str(hi),
        'common_prefix_sum':sums[0], 'at_boundary':list(at),
        'error_bound':'0 < lambda-Q/S < 1/10^15',
        'method':'Machin alternating bounds, integer sqrt, rational floor sums',
        'argument':'q<lambda; nonnegative integer floor differences have sum zero on the prefix'})


def boundary_certificate() -> dict:
    # Return a new object; callers cannot mutate the cached evidence.
    return json.loads(_boundary_certificate_json())

NAT=TypeSpec('NonnegativeInteger')
PAIR=TypeSpec('QuotientRemainderImage', convention=('Q=339949771344778','S=10^15','0<=rho<S','Q divides S*d_next+rho'))
LEDGER=TypeSpec('CanonicalExtinctionLedger', convention=('terminal=0','un-padded','ordered residues','fixed Q,S'))
CENTER=TypeSpec('CenteredMarks',6,LABELS,('sum=0','dimensionless'))
PROB=TypeSpec('PositiveProbabilityVector',6,LABELS,('sum=1','beta='+BETA_EXPR))
COMPLEX=TypeSpec('ComplexMarkedBaseline',6,LABELS,('real=c=cos(pi/1296000)','sum(imag)=0','dimensionless'))
FOURIER=TypeSpec('FullComplexDFT',6,LABELS,('exp(-2*pi*i*j*k/6)','unnormalized forward','fixed input labels'))
MAG=TypeSpec('FourierMagnitudes',6,LABELS,('DFT convention fixed','phase discarded'))
GEOMETRY=TypeSpec('SixMarkGeometry',6,LABELS,('baseline origin recorded','scale>0','0<epsilon<pi'))
SCALAR=TypeSpec('NamedScalar')
FLOOR_EXPR=TypeSpec('IntegerMapExpression', convention=('evaluated at nonnegative integer d',))


def payload_for(checker: str) -> str:
    if checker in ('floor_prefix','lambda_approx'):
        return canonical(boundary_certificate())
    if checker == 'golden_identity':
        return canonical({'normal_form':normalize('(1+sqrt5)/2'),'polynomial_residual':normalize('phi*phi-phi-1')})
    if checker == 'floor_collision':
        return canonical({'inputs':[0,1],'outputs':[0,0]})
    if checker == 'geometry_collision':
        return canonical({'centers':[0,1],'same_scale':1,'same_epsilon':'pi/648000','ignored':'origin'})
    if checker == 'phase_collision':
        return canonical({'inputs':'v and -v for v=(1,0,0,0,0,0)','same_magnitude':True})
    return canonical({'schema':checker, 'derivation':'PROOFS.md#'+checker.replace('_','-')})

# Closed catalogue of supported formula schemas. Unknown schemas fail closed.
# Payload equality is not the proof: check_schema below executes arithmetic or
# explicitly identifies the trusted analytic/declaration rule used.
def make_spec(edge_id: str) -> MapSpec:
    inverse_id=None; inverse_domain=''; arithmetic='binary64 preview'
    keep=('label_order','centered_contrast_information')
    if edge_id=='phi_identity':
        source=target=SCALAR; left='(1+sqrt5)/2'; right='1/2+sqrt5/2'
        formula='normalize(left)=normalize(right) in Q(sqrt(5))'; op='identity'; rel=Relation.IDENTITY
        checker='golden_identity'; support=Support.EXACT_CERTIFICATE; exact=True; rev=True
        preserves=('algebraic_value',); losses=(); req=('rational coefficients','positive sqrt5'); domain='the two named golden expressions'; inverse_id=edge_id; arithmetic='exact rational quadratic algebra'
    elif edge_id=='lambda_beta':
        source=target=SCALAR; left='lambda';right='optimizer_beta'
        formula='declare beta := lambda';op='declaration';rel=Relation.PARAMETER_IDENTIFICATION
        checker='parameter_choice';support=Support.EXPLICIT_DECLARATION;exact=True;rev=False
        preserves=('chosen_scalar_value',);losses=();req=('explicit parameter choice',);domain='named parameter assignment only'
    elif edge_id=='lambda_approximation':
        source=target=SCALAR;left='lambda';right='Q/S';formula='0 < lambda-Q/S < 10^-15';op='approximation';rel=Relation.APPROXIMATION
        checker='lambda_approx';support=Support.EXACT_CERTIFICATE;exact=False;rev=False
        preserves=('stated_error_bound',);losses=('exact_real_value',);req=('fixed Q,S and lambda definitions',);domain='the named constants';arithmetic='exact interval certificate'
    elif edge_id=='floor_agreement':
        source=target=FLOOR_EXPR;left='floor(lambda*d)';right='floor(Q*d/S)';formula='left(d)=right(d) for integer 0<=d<42189065';op='certified_floor';rel=Relation.DOMAIN_RESTRICTED_EQUIVALENCE
        checker='floor_prefix';support=Support.EXACT_CERTIFICATE;exact=True;rev=False
        preserves=('floor_output_on_certified_domain',);losses=();req=('integer 0<=d<42189065',);domain='0 <= d < 42189065';arithmetic='exact integers after certified rewrite'
    elif edge_id in ('floor','pair','unpair','ledger','unledger'):
        left={'floor':'d','pair':'d','unpair':'(d_next,rho)','ledger':'d','unledger':'extinction_ledger'}[edge_id]
        right={'floor':'floor(Q*d/S)','pair':'(d_next,rho)','unpair':'d','ledger':'extinction_ledger','unledger':'d'}[edge_id]
        source={'floor':NAT,'pair':NAT,'unpair':PAIR,'ledger':NAT,'unledger':LEDGER}[edge_id]
        target={'floor':NAT,'pair':PAIR,'unpair':NAT,'ledger':LEDGER,'unledger':NAT}[edge_id]
        op=edge_id; arithmetic='exact Python integers'; exact=True
        if edge_id=='floor':
            formula='F(d)=Q*d//S';rel=Relation.LOSSY_PROJECTION;checker='floor_collision';support=Support.EXACT_COLLISION;rev=False
            preserves=('nonnegative_integer_output',);losses=('preimage_identity',);req=('d>=0 integer',);domain='nonnegative integers'
        else:
            formula='Q*d=S*d_next+rho; inverse=(S*d_next+rho)/Q; iterate in ledger order'
            rel=Relation.EMBEDDING if edge_id in ('pair','ledger') else Relation.EQUIVALENCE
            checker='euclidean_'+('ledger' if 'ledger' in edge_id else 'pair');support=Support.TRUSTED_ANALYTIC_SCHEMA;rev=True
            preserves=('integer_seed_information',);losses=();req=('fixed Q,S','remainder bounds','exact inverse divisibility','canonical unpadded ledger' if 'ledger' in edge_id else 'valid pair image');domain=source.name
            inverse_id={'pair':'unpair','unpair':'pair','ledger':'unledger','unledger':'ledger'}[edge_id]
    elif edge_id=='geometry_marks':
        source=GEOMETRY;target=CENTER;left='SixMarkGeometry';right='CenteredMarks'
        formula='a*(-A,-B,-s,s,B,A); drop the recorded baseline origin';op=edge_id;rel=Relation.LOSSY_PROJECTION
        checker='geometry_collision';support=Support.EXACT_COLLISION;exact=True;rev=False;preserves=keep;losses=('baseline_origin',);req=('scale>0','0<epsilon<pi','trusted labels');domain='specified six-mark family with recorded origin'
    elif edge_id in ('marks_probability','probability_marks'):
        source,target=(CENTER,PROB) if edge_id=='marks_probability' else (PROB,CENTER)
        left,right=source.name,target.name;op=edge_id;rel=Relation.EQUIVALENCE;checker='centered_softmax';support=Support.TRUSTED_ANALYTIC_SCHEMA
        formula='p_i=exp(beta*z_i)/sum_j exp(beta*z_j); z_i=(log(p_i)-mean(log p))/beta'
        exact=True;rev=True;preserves=keep;losses=();req=('beta=lambda>0','fixed labels','zero-sum centering','strictly positive probabilities');domain=source.name
        inverse_id='probability_marks' if edge_id=='marks_probability' else 'marks_probability'
    elif edge_id in ('marks_complex','complex_marks'):
        source,target=(CENTER,COMPLEX) if edge_id=='marks_complex' else (COMPLEX,CENTER)
        left,right=source.name,target.name;op=edge_id;rel=Relation.EMBEDDING if edge_id=='marks_complex' else Relation.EQUIVALENCE
        checker='complex_embedding';support=Support.TRUSTED_ANALYTIC_SCHEMA;formula='w_i=c+i*z_i; inverse z_i=Im(w_i) on Re(w_i)=c'
        exact=True;rev=True;preserves=keep;losses=();req=('fixed c=cos(pi/1296000)','labels','centered imaginary coordinates');domain=source.name
        inverse_id='complex_marks' if edge_id=='marks_complex' else 'marks_complex'
    elif edge_id in ('marks_dft','dft_marks'):
        FT=TypeSpec('FourierMarkedBaseline',6,LABELS,('DFT of fixed-c centered marked baseline','full complex coefficients'))
        source,target=(COMPLEX,FT) if edge_id=='marks_dft' else (FT,COMPLEX)
        left,right=source.name,target.name;op=edge_id;rel=Relation.EQUIVALENCE;checker='full_dft';support=Support.TRUSTED_ANALYTIC_SCHEMA
        formula='DFT restricted to the complex-mark image; retain all six complex coefficients; inverse IDFT'
        exact=True;rev=True;preserves=keep;losses=();req=('n=6','full complex spectrum','fixed labels and c','DFT image constraint');domain=source.name
        inverse_id='dft_marks' if edge_id=='marks_dft' else 'marks_dft'
    elif edge_id in ('dft','idft'):
        # General complex vectors, unlike the restricted complex-mark image.
        CV=TypeSpec('ComplexVector',6,LABELS,('dimensionless',))
        source,target=(CV,FOURIER) if edge_id=='dft' else (FOURIER,CV)
        left,right=source.name,target.name;op=edge_id;rel=Relation.EQUIVALENCE;checker='full_dft';support=Support.TRUSTED_ANALYTIC_SCHEMA
        formula='F_k=sum_j v_j exp(-2*pi*i*j*k/6); v_j=sum_k F_k exp(+2*pi*i*j*k/6)/6'
        exact=True;rev=True;preserves=('full_labelled_complex_state',);losses=();req=('n=6','retain every complex coefficient','fixed Fourier convention');domain=source.name;inverse_id='idft' if edge_id=='dft' else 'dft'
    elif edge_id=='fourier_magnitude':
        source,target=FOURIER,MAG;left,right=source.name,target.name;op=edge_id;rel=Relation.LOSSY_PROJECTION;checker='phase_collision';support=Support.EXACT_COLLISION
        formula='m_k=abs(F_k)';exact=True;rev=False;preserves=('Fourier_magnitudes',);losses=('Fourier_phase',);req=('n=6','fixed Fourier convention');domain='full complex spectrum'
    else:
        raise Reject('unsupported map or witness schema: '+edge_id)
    contract=Contract(preserves,losses,req,exact,rev,domain)
    inv=None
    if inverse_id:
        inverse_domain=target.name+' satisfying its image constraints'
        inv=InverseContract(inverse_id,target,source,inverse_domain,'inverse(forward(x))=x on source','forward(inverse(y))=y on declared image')
    unsigned={'id':edge_id,'source':source,'target':target,'formula':formula,'implementation':op,'arithmetic':arithmetic,'inverse':inv,'left':left,'right':right,'relation':rel,'contract':contract,'checker':checker,'support':support}
    w=Witness(checker,support,digest(unsigned),payload_for(checker))
    return MapSpec(edge_id,source,target,formula,op,arithmetic,inv,Alignment(left,right,rel,w,contract))

MAP_IDS=('phi_identity','lambda_beta','lambda_approximation','floor_agreement','floor','pair','unpair','ledger','unledger','geometry_marks','marks_probability','probability_marks','marks_complex','complex_marks','dft','idft','marks_dft','dft_marks','fourier_magnitude')


def check_schema(spec: MapSpec) -> tuple[str,str]:
    w=spec.alignment.witness
    if w.checker=='golden_identity':
        need(normalize(spec.alignment.left)==normalize(spec.alignment.right),'unequal normal forms')
        need(normalize('phi*phi-phi-1')==Golden(),'golden polynomial')
        return 'Exact rational normalization in Q(sqrt(5)).','exact algebra certificate checked'
    if w.checker in ('floor_prefix','lambda_approx'):
        c=boundary_certificate()
        need(w.payload==canonical(c),'boundary certificate binding')
        return 'Exact enclosures and prefix floor sums checked.','exact arithmetic certificate checked under documented analytic identities'
    if w.checker=='floor_collision':
        need(0*Q//S==1*Q//S==0,'collision failed')
        return '0 != 1; F(0)=F(1)=0.','exact counterexample to injectivity'
    if w.checker=='geometry_collision':
        return 'The formula contains a,epsilon but no origin; origins 0 and 1 give the same marks.','definitional coordinate-projection collision'
    if w.checker=='phase_collision':
        return 'The distinct spectra (1,0,...,0),(-1,0,...,0) have identical coordinate magnitudes.','exact counterexample to injectivity'
    if w.checker=='parameter_choice':
        return 'Assignment beta:=lambda is registered as a choice.','declaration only; no optimizer equivalence'
    need(w.checker in {'euclidean_pair','euclidean_ledger','centered_softmax','complex_embedding','full_dft'},'unknown analytic schema')
    if w.checker.startswith('euclidean'):
        need(0<Q<S,'division parameters')
    return 'Checked instantiation of documented schema '+w.checker+'.','trusted analytic schema; derivation supplied, not machine-checked universal proof'


def verify(spec: MapSpec) -> Certificate:
    need(type(spec) is MapSpec,'a MapSpec is required')
    need(spec.alignment.witness is not None,'NO EDGE WITHOUT A WITNESS')
    need(spec.alignment.witness.support not in {Support.NUMERICAL_TEST_ONLY,Support.EXTERNAL_REFERENCE_ONLY},'insufficient evidence for admission')
    expected=make_spec(spec.id)
    need(spec==expected,'claim, implementation, contract, inverse, type or witness differs from supported schema')
    c=spec.alignment.contract
    need(not c.reversible or spec.inverse is not None,'NO REVERSIBILITY WITHOUT INVERSE CONTRACT')
    if spec.inverse:
        i=make_spec(spec.inverse.map_id)
        need(i.source==spec.target and i.target==spec.source,'inverse types disagree')
    detail,status=check_schema(spec)
    return Certificate(spec.id,spec.alignment.witness.support,spec.alignment.witness.claim_digest,detail,status)

# Runtime type/image guards. For real/complex preview types, tolerances are
# explicitly implementation acceptance tolerances, never exact proof tests.
def validate(t: TypeSpec, x: Any) -> None:
    name=t.name
    if name=='NonnegativeInteger':
        need(type(x) is int and x>=0,'expected nonnegative integer (bool excluded)');return
    if name=='QuotientRemainderImage':
        need(isinstance(x,tuple) and len(x)==2,'expected pair')
        d,r=x;validate(NAT,d);need(type(r) is int and 0<=r<S,'remainder range')
        need((S*d+r)%Q==0,'REVERSE_DIVISIBILITY');return
    if name=='CanonicalExtinctionLedger':
        need(isinstance(x,tuple) and len(x)<=10000,'ordered ledger tuple required')
        need(all(type(r) is int and 0<=r<S for r in x),'remainder range')
        need(not x or x[-1]!=0,'NON_MINIMAL_LEDGER')
        d=0
        for r in reversed(x):
            need((S*d+r)%Q==0,'REVERSE_DIVISIBILITY');d=(S*d+r)//Q
        return
    if name=='SixMarkGeometry':
        need(isinstance(x,dict) and set(x)=={'a','epsilon','origin'},'geometry keys')
        need(all(type(v) in (int,float) and math.isfinite(v) for v in x.values()),'finite geometry')
        need(x['a']>0 and 0<x['epsilon']<math.pi,'geometry domain');return
    if name in ('NamedScalar','IntegerMapExpression'):
        return  # non-executable alignment except guarded floor rewrite
    need(isinstance(x,tuple) and len(x)==6,'six ordered components required')
    if name in ('ComplexMarkedBaseline','ComplexVector','FullComplexDFT','FourierMarkedBaseline'):
        need(all(type(v) in (int,float,complex) and math.isfinite(complex(v).real) and math.isfinite(complex(v).imag) for v in x),'finite complex components')
        if name=='FourierMarkedBaseline':
            decoded=tuple(sum(x[k]*cmath.exp(2j*math.pi*j*k/6) for k in range(6))/6 for j in range(6))
            validate(COMPLEX,decoded)
        if name=='ComplexMarkedBaseline':
            c=math.cos(math.pi/1296000)
            need(all(abs(complex(v).real-c)<=1e-12 for v in x),'point outside complex embedding image')
            need(abs(sum(complex(v).imag for v in x))<=1e-10*max(1,max(abs(v) for v in x)),'imaginary centering')
        return
    need(all(type(v) in (int,float) and math.isfinite(v) for v in x),'finite real components')
    if name=='CenteredMarks':
        need(abs(math.fsum(x))<=1e-10*max(1,max(map(abs,x))),'centering precondition')
    elif name=='PositiveProbabilityVector':
        need(all(v>0 for v in x) and abs(math.fsum(x)-1)<=1e-12,'positive normalized probabilities required')
    elif name=='FourierMagnitudes':
        need(all(v>=0 for v in x),'nonnegative magnitudes required')
    else:
        raise Reject('unknown runtime type: '+name)


def execute(spec: MapSpec, x: Any) -> Any:
    verify(spec)
    op=spec.implementation
    if op=='certified_floor':
        validate(NAT,x);need(x<DSTAR,'outside certified floor-agreement domain');return Q*x//S
    if op in ('identity','declaration','approximation'):
        raise Reject('this edge is an expression alignment, not a state-execution map')
    validate(spec.source,x)
    try:
        if op=='floor': y=Q*x//S
        elif op=='pair': y=divmod(Q*x,S)
        elif op=='unpair': y=(S*x[0]+x[1])//Q
        elif op=='ledger':
            rows=[];d=x
            while d:
                d,r=divmod(Q*d,S);rows.append(r)
                need(len(rows)<=10000,'ledger resource limit')
            y=tuple(rows)
        elif op=='unledger':
            d=0
            for r in reversed(x): d=(S*d+r)//Q
            y=d
        elif op=='geometry_marks':
            s=math.sin(x['epsilon']/2);a=x['a'];A=s+PHI**2;B=s+1
            y=tuple(a*z for z in (-A,-B,-s,s,B,A))
        elif op=='marks_probability':
            vals=tuple(LAMBDA*z for z in x);top=max(vals)
            exp=tuple(math.exp(z-top) for z in vals);total=math.fsum(exp)
            need(all(v>0 for v in exp),'floating underflow would lose positivity')
            y=tuple(v/total for v in exp)
        elif op=='probability_marks':
            logs=tuple(math.log(v) for v in x);mean=math.fsum(logs)/6
            y=tuple((v-mean)/LAMBDA for v in logs)
        elif op=='marks_complex':
            c=math.cos(math.pi/1296000);y=tuple(complex(c,v) for v in x)
        elif op=='complex_marks': y=tuple(complex(v).imag for v in x)
        elif op in ('dft','idft','marks_dft','dft_marks'):
            sign=-1 if op in ('dft','marks_dft') else 1
            y=tuple(sum(x[j]*cmath.exp(sign*2j*math.pi*j*k/6) for j in range(6))/(6 if op in ('idft','dft_marks') else 1) for k in range(6))
        elif op=='fourier_magnitude': y=tuple(abs(v) for v in x)
        else: raise Reject('no implementation for '+op)
    except (OverflowError,ZeroDivisionError,ValueError) as e:
        if isinstance(e,Reject): raise
        raise Reject('arithmetic failure: '+str(e)) from e
    validate(spec.target,y)
    return y

@dataclass(frozen=True)
class Chain:
    maps: tuple[MapSpec,...]
    @property
    def source(self) -> TypeSpec: return self.maps[0].source
    @property
    def target(self) -> TypeSpec: return self.maps[-1].target
    def metadata(self) -> dict:
        contracts=[m.alignment.contract for m in self.maps]
        common=set(contracts[0].preserves)
        for c in contracts[1:]: common &= set(c.preserves)
        return {'path':[self.source.name]+[m.target.name for m in self.maps],
            'type_safe':True,'formulas_exact':all(c.exact for c in contracts),
            'certified_reversible':all(c.reversible and m.inverse for c,m in zip(contracts,self.maps)),
            'preserves':sorted(common),
            'losses_or_discards_encountered':sorted(set().union(*(set(c.loses) for c in contracts))),
            'stage_requirements':[{'stage':i,'map':m.id,'domain':m.alignment.contract.domain,'requires':list(m.alignment.contract.requires)} for i,m in enumerate(self.maps)],
            'implementation_arithmetic':list(dict.fromkeys(m.arithmetic for m in self.maps)),
            'support':[m.alignment.witness.support.value for m in self.maps],
            'note':'Conservative sufficient composition rules; absence of a certificate is not a proof of impossibility. Runtime guards check every stage.'}
    def run(self,x:Any)->Any:
        for m in self.maps:x=execute(m,x)
        return x
    def reverse(self,y:Any)->Any:
        need(self.metadata()['certified_reversible'],'chain has no certified inverse')
        for m in reversed(self.maps): y=execute(make_spec(m.inverse.map_id),y)
        return y


def compose(*maps:MapSpec)->Chain:
    need(bool(maps),'empty composition')
    executable={'floor','pair','unpair','ledger','unledger','geometry_marks','marks_probability','probability_marks','marks_complex','complex_marks','dft','idft','marks_dft','dft_marks','fourier_magnitude'}
    for m in maps:
        verify(m);need(m.implementation in executable,'alignment-only edge is not a state map')
    for left,right in zip(maps,maps[1:]):
        if left.target != right.source:
            raise TypeError(f'cannot compose {left.id}: {left.target} with {right.id}: {right.source}')
    return Chain(tuple(maps))

class Graph:
    def __init__(self)->None:self._edges:dict[str,MapSpec]={};self._certs:dict[str,Certificate]={}
    def admit(self,m:MapSpec)->Certificate:
        cert=verify(m)
        need(m.id not in self._edges,'duplicate map id')
        self._edges[m.id]=m;self._certs[m.id]=cert;return cert
    def report(self)->dict:
        return {'schema':'TGA_WITNESS_GRAPH/2.0','edges':[plain(m) for m in self._edges.values()],
            'certificates':[plain(c) for c in self._certs.values()],
            'trust':'Closed supported schemas plus exact certificate algorithms. No general theorem proving or automatic corpus extraction.'}


def build_report()->dict:
    g=Graph()
    for name in MAP_IDS:g.admit(make_spec(name))
    marks=(-3.,-2.,-1.,1.,2.,3.)
    chain=compose(*(make_spec(n) for n in ('marks_probability','probability_marks','marks_complex')))
    out=chain.run(marks);back=chain.reverse(out)
    geometry={'a':1.,'epsilon':math.pi/648000,'origin':7.}
    geomchain=compose(*(make_spec(n) for n in ('geometry_marks','marks_probability','probability_marks','marks_complex')))
    finite_claims=(Claim('phi_A','constant','(1+sqrt5)/2',('sqrt5',)),Claim('phi_B','constant','1/2+sqrt5/2',('sqrt5',)),Claim('wrong_phi','constant','1+sqrt5',('sqrt5',)))
    return {'schema':'TGA_RUN/2.0','source_sha256':hashlib.sha256(Path(__file__).read_bytes()).hexdigest(),
        'pipeline':{'implemented':['explicit typed claims','restricted exact normalization','proposal generation','closed witness checks','alignment admission','typed composition','execution','report'],
            'not_implemented':['automatic PDF/social-media extraction','arbitrary symbolic theorem proving','minimal-generator search','unbounded closure search','physical or optimizer equivalence']},
        'proposals_only':[plain(p) for p in propose(finite_claims)],'graph':g.report(),
        'boundary':boundary_certificate(),
        'centered_chain':{'contract':chain.metadata(),'input':marks,'output':plain(out),'reverse':back,'roundtrip_max_abs_error':max(abs(a-b) for a,b in zip(marks,back)),'meaning':'numerical execution, not universal proof'},
        'geometry_chain':{'contract':geomchain.metadata(),'input':geometry,'output':plain(geomchain.run(geometry))},
        'ledger_399':{'remainders':list(execute(make_spec('ledger'),399)),'recovered':execute(make_spec('unledger'),execute(make_spec('ledger'),399))},
        'limits':['No shared symbol admits an edge.','Finite tests never become universal certificates.','Trusted analytic-schema instantiation is reported separately from exact arithmetic certification.','No roundtrip of a float encoding is called bitwise exact.']}


def main()->None:
    parser=argparse.ArgumentParser(description=__doc__)
    parser.add_argument('--report',type=Path,help='write JSON report; default prints concise summary')
    args=parser.parse_args();report=build_report()
    if args.report:
        args.report.write_text(json.dumps(plain(report),indent=2,sort_keys=True,allow_nan=False)+'\n')
        print('WROTE',args.report)
    else:
        print('TGA 2.0:',len(report['graph']['edges']),'witness-backed edges')
        print('First floor disagreement:',DSTAR)
        print('Common prefix floor sum:',report['boundary']['common_prefix_sum'])
        print('Centered chain certified reversible:',report['centered_chain']['contract']['certified_reversible'])
        print('Full geometry chain certified reversible:',report['geometry_chain']['contract']['certified_reversible'])
        print('Reconstructed seed:',report['ledger_399']['recovered'])
        print('Not a general theorem prover. Analytic schema trust is explicit.')

if __name__=='__main__':main()