# TGA 2.1 proofs

Supplementary to TGA 2.0. These derivations are the written basis of the trusted analytic schemas in this release. The program checks that a path-equality certificate names one implemented schema, that the written heading is present, and that both paths meet their contracts. A numerical sample is not a proof. Binary64 agreement is recorded separately and is not an exact membership certificate.

The general equivalence between centered coordinates and positive probabilities is not membership in the six-mark family. Centered log-ratio coordinates and Aitchison powering are the established framework for the general equivalence. The six-mark family is the subset cut out by the gap conditions below.

## normalization-policy

A positive probability vector, in this release, is six ordered values labeled d2, d1, d, b, b1, b2. Each entry must be finite and strictly positive. The sum is the accurately summed binary64 total. The vector is accepted only when the absolute difference between that sum and 1 is at most 1e-12. This is the same numerical acceptance predicate as TGA 2.0's positive probability vector.

The implementation does not rescale a vector that fails the test. That failure is malformed normalization. It is not a probability vector and it is not a six-mark probability. Booleans, nonnumeric entries, the wrong length, zeros, negatives, and nonfinite values are rejected before any power, gap, or certificate is considered.

Every probability vector that represents the six-mark family is a positive probability vector. The converse is false.

## centered-log-ratio

For β > 0 and a real six-vector z with coordinate sum zero,

S_β(z)_i = exp(β z_i) / Σ_j exp(β z_j).

On the positive simplex the inverse is the centered log-ratio map

L_β(p)_i = (log p_i − mean_j log p_j) / β.

These two maps invert one another between the centered hyperplane and the strictly positive simplex. TGA 2.0 records that fact for the declared value β = λ. This release keeps the same identity for every finite β > 0. The default remains the declaration β = λ = φ / (φ + π). The configuration retains that declaration, or the supplied numeric value, together with the dimensionless coordinate units and the fixed label order. A binary64 preview of λ is not the exact real number.

Aitchison powering on the simplex is, for r > 0,

P_r(p)_i = p_i^r / Σ_j p_j^r.

In centered log-ratio coordinates this is scalar multiplication: L_β(P_r(p)) = r L_β(p). Label order is part of the coordinate convention. These maps do not permute it.

## softmax-scale-power

Let M_r(z) = r z for r > 0, on centered real six-vectors. On that domain

S_β ∘ M_r = P_r ∘ S_β.

Proof. Let Z = Σ_j exp(β z_j). For finite z this Z is finite and positive, and S_β(z)_i = exp(β z_i) / Z. Then

(P_r(S_β(z)))_i = (exp(β z_i) / Z)^r / Σ_k (exp(β z_k) / Z)^r.

The common positive factor Z^r cancels, which leaves

exp(β r z_i) / Σ_k exp(β r z_k) = S_β(r z)_i = (S_β ∘ M_r)(z)_i.

The cancellation is the common softmax denominator after exponentiation. It requires every coordinate to stay strictly positive. If binary64 underflow produces a zero, the numerical result has left the supported positive domain. The implementation rejects that result. It does not clip the zero to a small positive number, and it does not keep a reversibility badge on a clipped vector.

The same style of cancellation gives the power laws on the positive simplex.

P_r ∘ P_t = P_{r t} for r > 0 and t > 0.

P_1 is the identity.

The inverse of P_r is P_{1/r}.

Proof of composition. Let q = P_t(p), so q_i = p_i^t / Σ_j p_j^t. Then

P_r(q)_i = q_i^r / Σ_k q_k^r = p_i^{r t} / Σ_k p_k^{r t},

because (Σ_j p_j^t)^r cancels. Thus P_r(P_t(p)) = P_{r t}(p). Setting the product of the exponents equal to 1 gives the inverse. Setting r = 1 leaves p_i / Σ_j p_j, which equals p_i when the coordinates already sum to 1.

These power laws are checked identities of P_r. The path-equality certificate object initially admits only two schemas: S_β ∘ M_r = P_r ∘ S_β, and F ∘ M_r = D_r ∘ F. A request for any other schema, including a bare residual comparison, does not receive that certificate.

## fourier-mark-scale

Keep the TGA 2.0 convention. Let c_0 = cos(π/1296000). For a centered real six-vector z define

w_j = c_0 + i z_j, W = DFT(w), F(z) = W,

with the unnormalized forward transform

W_k = Σ_j w_j exp(−2π i j k / 6).

Define D_r on this marked Fourier image by leaving W_0 unchanged and multiplying W_1 through W_5 by r > 0. Complex phase is part of the coefficient. D_r does not replace a coefficient by its modulus.

For centered real z, the coordinate sum is zero, so

W_0 = Σ_j (c_0 + i z_j) = 6 c_0.

For k ≠ 0 the transform of a constant vector vanishes, so W_k = i Σ_j z_j exp(−2π i j k / 6). Therefore F(r z)_0 = 6 c_0 = W_0 and F(r z)_k = r W_k for k = 1,…,5. That is

F ∘ M_r = D_r ∘ F.

Because z is real and the constant sits only in the DC bin,

W_{6−k} = −conjugate(W_k) for k = 1,…,5.

The implementation requires W_0 = 6 c_0 and that conjugate relation before D_r runs. Scaling by a positive real r preserves the relation. It also preserves the argument of every nonzero coefficient. A zero coefficient remains zero; its phase is undefined and is not invented.

The six-mark family imposes further constraints on the centered coordinates recovered by the inverse transform. Those constraints are not consequences of the marked Fourier image alone. D_r does not test them, and it does not discard phase in order to meet them.

## six-mark-membership

Labels, in order, are d2, d1, d, b, b1, b2. With the baseline origin omitted, the six-mark geometry (a, ε) has centered coordinates

z = a (−A, −B, −s, s, B, A),

where s = sin(ε/2), A = s + φ^2, B = s + 1, and φ = (1 + √5) / 2, so φ^2 = φ + 1. This release states the family for a > 0 and 0 < ε ≤ π, hence 0 < s ≤ 1. TGA 2.0's executable geometry map remains the published strict inequality 0 < ε < π. The endpoint ε = π belongs to this supplementary statement.

For a positive probability vector define the five consecutive log-ratio gaps

g_i = log(p_{i+1} / p_i), i = 1,…,5.

Necessity. If p = S_β(z) for a family vector z and β > 0, then g_i = β (z_{i+1} − z_i). The coordinate gaps are

z_1 − z_0 = a (φ^2 − 1) = a φ,

z_2 − z_1 = a,

z_3 − z_2 = 2 a s,

z_4 − z_3 = a,

z_5 − z_4 = a φ.

Hence g_2 = g_4 = β a > 0, g_1 = g_5 = φ g_2, and g_3 = 2 s g_2, so 0 < g_3 ≤ 2 g_2. The parameters are a = g_2 / β, s = g_3 / (2 g_2), and ε = 2 arcsin(s). Canonical-angle mode adds ε = π/648000, equivalently s = sin(π/1296000), equivalently

g_3 = 2 sin(π/1296000) g_2.

Sufficiency. Suppose p is a positive probability vector and the gaps satisfy those conditions for a fixed β > 0. Set a = g_2 / β > 0 and s = g_3 / (2 g_2) in (0, 1], and set ε = 2 arcsin(s) in (0, π]. The consecutive differences are then a (φ, 1, 2s, 1, φ). Two real vectors with the same consecutive differences differ by one additive constant. The zero-sum condition fixes that constant. The vector a (−A, −B, −s, s, B, A) is centered and has those differences, so it is the unique centered representative. Therefore the centered log-ratio coordinates of p are that geometric vector, and p represents the six-mark family. The five gap conditions reproduce the geometry. The zero-mean condition fixes the six coordinates.

Uniform probabilities p_i = 1/6 have every gap equal to zero, so g_2 = 0. They are valid positive probability data. They do not satisfy g_2 > 0, so they do not represent this positive-scale family.

## tolerance-policy

Binary64 evaluation of one vector reports numerical consistency, candidate parameters, residuals, and this policy. It does not issue an exact membership certificate. The exact statement is the schema in the previous section.

Let band(x) = 1e-9 + 1e-8 |x|. Gap equalities use the band at the larger of the two magnitudes. The scale g_2 counts as clearly positive only when g_2 > 1e-9. If g_2 ≤ 0, the vector is not in the positive-scale family. If 0 < g_2 ≤ 1e-9, the sign sits inside the tolerance of zero. That status is an uncertain boundary, not a forced positive scale.

The ratio s = g_3 / (2 g_2) is never clamped. Classify the measured value as follows.

If s is nonfinite, there is no membership result.

If s > 1 and s − band(s) > 1, the vector is not a member.

If 1 < s and s − 1 ≤ 1e-12, the excess is binary64 roundoff at the included endpoint ε = π. The measured s is reported unclamped. The candidate angle is π. This is still not an exact certificate, and s is not rewritten as 1.

If s > 1 by more than 1e-12 but s − band(s) ≤ 1, the boundary is uncertain. s is not replaced by 1, and arcsin is not applied to a clamped value.

If s ≤ 0 and s + band(s) ≤ 0, the vector is not a member.

If s ≤ 0 but s + band(s) > 0, the boundary is uncertain. s is not replaced by 0.

If 0 < s ≤ band(s), the open endpoint 0 is uncertain. s is not replaced by a positive token.

If band(s) < s ≤ 1, and the other gap equalities meet the band, the family is numerically consistent. Then ε = 2 arcsin(s) is a candidate parameter, including the allowed endpoint s = 1. This is still not an exact certificate.

Here band(s) = 1e-9 + 1e-8 max(1, |s|). Canonical-angle mode adds the comparison of g_3 with 2 sin(π/1296000) g_2 under the ordinary gap band. Failing that comparison does not decide the wider family.

## power-composition

The composition and inverse laws for P_r are proved under softmax-scale-power. They are checked when those operations run. They are not, by themselves, one of the two path-equality schemas admitted in this release.

## path-certificate

A path-equality certificate names the common source and target, both ordered paths, the versioned operation identifiers, the parameter values, and the retained context: β, coordinate units, and label order. It names the source-domain and intermediate-image requirements, the proof schema, and the derivation anchor in this file. Arithmetic mode is binary64 when a path is executed. The numerical execution record is a separate field from the mathematical justification.

Admission uses only the implemented schemas tga.2.1/proof/softmax-scale-power and tga.2.1/proof/fourier-mark-scale. The submitted paths must be exactly those schemas' paths. Parameters must lie in the declared domain. Every intermediate value must satisfy its contract. If a path is undefined, a contract fails, the schema is unsupported, or the written heading is missing, the result states that condition and does not contain a certificate. A small residual is not enough to admit an unknown equation. A large residual means this execution did not instantiate the schema, so no certificate is issued for that input.

## trust-boundary

This is not a general theorem prover. Inherited TGA 2.0 edges keep their own support labels. New maps and the two path identities are trusted analytic schemas with the derivations on this page. Numerical comparisons stay in their own record. Publication as a supplementary release is not mathematical status and is not an execution result.