# TGA 2.0: witness rules, derivations, and trust boundary

TGA verifies a closed collection of supported claims and certificate schemas. It does not decide arbitrary mathematical truth. An admitted edge retains its evidence category. A trusted analytic schema is an explicitly stated rule with a derivation here; the Python program checks that the edge is an instance of that rule, not a formal proof of the rule in Lean or another foundational calculus.

## What an edge means

| Relation | Required meaning |
|---|---|
| IDENTITY | The two expressions denote the same object on the named domain. |
| PARAMETER_IDENTIFICATION | A parameter is explicitly assigned a value. This is a declaration, not a theorem deriving that choice. |
| EQUIVALENCE | The stated correspondence is valid under its domain and inverse contracts. |
| EMBEDDING | The forward map is injective; its inverse applies to the specified image. |
| DOMAIN_RESTRICTED_EQUIVALENCE | Equality/correspondence is certified only on an explicit domain. |
| LOSSY_PROJECTION | Distinct inputs can have the same output; an explicit collision supports noninjectivity. |
| APPROXIMATION | An explicit error statement replaces equality. |

Every map specification binds source and target types, labels, conventions, formula, implementation dispatch, domain, relation, preservation/loss metadata, witness and inverse contract. The verifier rejects a specification that differs from a supported schema. Changing just a boolean is insufficient to change the mathematics. Unknown schemas fail closed.

The graph contains three different activities: expression alignments, state maps, and the guarded certified floor rewrite. Only state maps are composable as runtime chains. A theorem relating two maps is not silently treated as a map on their states.

## golden-identity

Represent a+b√5 by the rational pair (a,b). Multiplication is

(a,b)(c,d)=(ac+5bd,ad+bc).

The inverse of a nonzero pair is (a,−b)/(a²−5b²). Since √5 is irrational, the denominator vanishes for a rational pair only when both coefficients are zero. The restricted expression parser uses these exact operations; no evaluation of Python code is permitted. It proves the two supplied formulas for φ equal and φ²−φ−1=0 by zero rational residuals. A shared symbol does not establish equality: 1+√5 is twice φ.

## parameter-choice

The declaration β:=λ sets a parameter in an example. It does not assert an optimizer was derived from geometry, an optimization method is equivalent to the contraction, or λ is optimal. The graph registers this as EXPLICIT_DECLARATION. It is not a runtime state-map edge.

For a constant forcing target g, an additional recurrence could later be specified as m′=βm+(1−β)g. Setting g=1 and β=λ reproduces T_aff, but varying gradients require a different state space and contract. This release deliberately does not infer that unprovided recurrence.

## floor-prefix and lambda-approx

Let Q=339949771344778, S=10¹⁵, q=Q/S, φ=(1+√5)/2, and λ=φ/(φ+π). All certificate decisions are rational or integer.

### Enclosing π and √5

For 0<x<1, the alternating series for atan(x) has its value strictly between a partial sum and the next partial sum. The code uses 100 terms for x=1/5 and x=1/239.

Machin's identity is π=16 atan(1/5)−4 atan(1/239). One justification: if a=atan(1/5), then tan(2a)=5/12 and tan(4a)=120/119. If b=atan(1/239), the tangent subtraction formula gives tan(4a−b)=1. The elementary bounds x−x³/3<atan(x)<x put 4a−b in (0,π/2), so it equals π/4. The program trusts the stated elementary real-analysis identities; it does not formalize analysis axioms.

At scale H=10⁸⁰, let r=isqrt(5H²). The checked rational inequalities (r/H)²<5<((r+1)/H)² enclose √5. They give φ₋<φ<φ₊. If π₋<π<π₊, monotonicity in the two positive arguments gives

L=φ₋/(φ₋+π₊) < λ < U=φ₊/(φ₊+π₋).

The program checks q<L<U and U−q<10⁻¹⁵. This gives the approximation edge its actual error bound; it does not call q equal to λ.

### Exact floor sums

Define B(n,m,a,b)=Σ_{i=0}^{n−1} floor((ai+b)/m) for n,a,b≥0 and m>0. Strip integer parts a=qₐm+a₀ and b=q_bm+b₀. Their contributions are qₐn(n−1)/2+q_bn.

For 0≤a,b<m, if an+b<m the remaining sum is zero. Otherwise a>0. Set n′=floor((an+b)/m) and b′=(an+b) mod m. Count lattice points by levels j=1,…,n′:

B(n,m,a,b)=Σ_{j=1}^{n′}[n−ceil((mj−b)/a)]
             =Σ_{k=0}^{n′−1}floor((mk+b′)/a)
             =B(n′,a,m,b′).

These are the loop's transformations. After the next integer-part reduction, the modulus decreases, so the algorithm terminates. The independent small-domain brute sums in the tests corroborate its implementation; the counting identity is its proof.

### Entire prefix and first failure

Let D=42,189,065. Exact floor-sum calculations yield

Σ_{d=0}^{D−1}floor(qd)=Σfloor(Ld)=Σfloor(Ud)=302,541,195,258,184.

Because q<λ<U, each difference floor(Ud)−floor(qd) is a nonnegative integer. Their sum is zero, so each is zero. By sandwiching,

floor(λd)=floor(qd) for every integer 0≤d<D.

At d=D the checked values are

floor(qD)=14,342,162,
floor(LD)=floor(UD)=14,342,163.

Thus D is the first nonnegative disagreement. This proves the whole finite prefix by a rational certificate rather than by checking only a few examples or trusting the endpoint's printed value. The exclusive upper bound is enforced when the certified rewrite is executed.

## euclidean-pair

For d≥0, Qd=Sd′+ρ has the unique quotient d′=floor(Qd/S) and remainder 0≤ρ<S. Therefore

d=(Sd′+ρ)/Q.

The pair image consists precisely of nonnegative integer d′ and 0≤ρ<S such that Q divides Sd′+ρ. The inverse rejects other pairs. Both identities follow directly from division with remainder. This is an embedding into valid pairs and a bijection to that image.

The quotient alone is not injective: F(0)=F(1)=0 because 0<Q<S. The pair distinguishes them by remainders 0 and Q.

## euclidean-ledger

For every positive integer d, 0≤F(d)<d, so iteration reaches zero in finitely many steps. Retain exactly the ordered remainders up to that first zero. A zero seed has an empty ledger. A nonempty canonical ledger cannot have a last zero remainder: a transition from positive d to zero has remainder Qd>0.

Starting at zero and reversing every exact Euclidean split reconstructs the seed. The runtime checks remainder bounds and divisibility at each step. An appended terminal-zero row is refused as nonminimal. A valid shorter suffix can identify a different seed; this is reconstruction, not authentication.

The inverse and arithmetic are exact Python-integer operations. A 10,000-entry cap is an implementation resource limit. The underlying theorem holds for every finite nonnegative integer; exceptionally large inputs may be refused by the implementation.

## geometry-collision

This release's geometry object is deliberately explicit and limited: scale a>0, seed angle 0<ε<π, and a recorded baseline origin o. It is not the archive's full 3D pose record. Its map returns the centered dimensionless ordinate tuple a(−A,−B,−s,s,B,A), where s=sin(ε/2), A=s+φ², B=s+1.

The origin is absent from this output. For example, origins o=0 and o=1 with equal a,ε have identical images. The map is therefore lossy. Pairwise ordinate differences and labels survive, but the discarded origin cannot be recovered by inverting a later softmax. Preserving origin would require carrying it as explicit side information or restricting it in the source type.

## centered-softmax

Fix β=λ>0 and a fixed six-label order. Define

C={z∈ℝ⁶: Σzᵢ=0},
P={p∈ℝ⁶: pᵢ>0, Σpᵢ=1}.

Sβ(z)ᵢ=exp(βzᵢ)/Σⱼexp(βzⱼ),
Lβ(p)ᵢ=[log pᵢ−(1/6)Σⱼlog pⱼ]/β.

For centered z, log(Sβ(z)ᵢ)=βzᵢ−log Z; averaging removes log Z. Thus Lβ(Sβ(z))=z. Conversely, exp(βLβ(p)ᵢ)=pᵢ/exp(mean(log p)); normalization recovers p. Hence Sβ and Lβ are inverse bijections between C and P.

Log ratios encode differences: log(pᵢ/pⱼ)=β(zᵢ−zⱼ). Without centering, adding any common constant to z leaves p unchanged. Without retaining or fixing β, scale is ambiguous. Zero probabilities lie outside the inverse domain.

The implementation subtracts the largest exponent before exponentiation. It refuses underflow that would turn a positive probability into zero. Rounding remains possible; reported round-trip residuals are numerical tests. It never calls the binary64 representation bitwise reversible.

## complex-embedding

Fix c=cos(π/1296000). Map centered z to the ordered complex tuple wᵢ=c+izᵢ. Its image has every real part c and centered imaginary parts. Im(wᵢ) is the inverse on this image. The inverse rejects a general complex tuple outside those constraints.

This complex representation is a specified coordinate embedding, not evidence that the original geometry is a physical wave. The label order and the fixed real coordinate are part of its type.

## full-dft

For n=6, define Fₖ=Σⱼvⱼexp(−2πijk/n). Its inverse is vⱼ=(1/n)ΣₖFₖexp(2πijk/n).

The finite geometric-series identity Σ_{k=0}^{n−1}exp(2πi(j−ℓ)k/n)=n if j=ℓ and 0 otherwise proves the inverse. It requires all complex coefficients and the normalization/sign convention. Binary64 evaluation corroborates this exact formula numerically.

The general DFT type and the DFT of the restricted complex-mark image are distinct. The specialized `marks_dft`/`dft_marks` pair carries the image constraints so the centered-mark chain can remain reversible. A general spectrum is not silently reinterpreted as a marked baseline.

Discarding phase is lossy: the distinct spectra (1,0,…,0) and (−1,0,…,0) have the same coordinate magnitudes. Magnitudes alone do not inherit the full DFT inverse contract.

## Composition rules

1. Every edge must first pass its witness check. A proposal is never sufficient.
2. Adjacent structural types must agree, including labels, dimensions, coordinate conventions, and the declared β. Matching names alone is insufficient.
3. Each runtime input and output is checked against its type/image predicate. Requirements and domains are retained per stage, not incorrectly treated as one unqualified requirement on the original input.
4. Formula exactness is the conjunction of the admitted contracts' exactness flags. Arithmetic mode is separate.
5. A constructive chain inverse is supplied only if every stage has an admitted inverse contract. It applies the inverse maps in reverse order. This is a sufficient certificate rule, not a theorem that all other chains are noninjective. Domain restrictions can sometimes make a composition injective even when a broader component map is not.
6. Losses/discards encountered are retained. Preservation claims use the intersection of common semantic property identifiers already justified by each schema. This is conservative: a more powerful proof can later establish additional end-to-end invariants. Merely taking a union is unsound.
7. Even a mathematically exact, reversible chain can use floating-point implementations. The report states that fact explicitly.

## What the verification does and does not establish

`EXACT_CERTIFICATE` means the particular exact algorithm checked the stated algebraic or interval certificate. It still trusts its arithmetic implementation and the documented elementary identities.

`TRUSTED_ANALYTIC_SCHEMA` means a supported instance of one of the derivations above was accepted; the universal analytic theorem is not internally reproved by the Python program. This label is retained on every edge and chain.

`EXPLICIT_DECLARATION` and `EXACT_COLLISION` retain their distinct meanings. `NUMERICAL_TEST_ONLY` and `EXTERNAL_REFERENCE_ONLY` are rejected as sufficient admission evidence by this release. Numerical execution remains available after admission, as a separate layer.

The closed registry and its implementation dispatch are the trusted code base. A claim digest binds data fields and a file hash identifies source bytes; neither hash proves the program itself correct or authenticates an author. Changing the trusted Python source changes the trust base and requires review. No edge means optimizer equivalence, physical equivalence, or identity of entire theories.