back to table · edit · history · where entries came from · files · download
3706 bytes, as of the version from 2026-10-30 12:33 (current). Recorded here, not run.
# Metric and verification notes for T624
Write a tangent at Q=(I_k,0)^T as Delta=(A,B)^T. The real A is
skew-symmetric; the complex A is skew-Hermitian. The Frobenius squared norm
is tr(A* A)+tr(B* B). A real off-diagonal coordinate of A has norm squared 2;
each of the two real coordinates of a complex off-diagonal entry also has
norm squared 2. Complex imaginary diagonal coordinates and every coordinate
of B have norm squared 1. Thus the coordinate Gram determinant is
2^(beta*k*(k-1)/2), with beta=1 or 2. Its square root accounts for the
volume correction 2^(beta*k*(k-1)/4) relative to the conventional sphere
product. The checks construct all these sparse tangent vectors, compute their
pairwise inner products, and verify the determinants in every retained shape.
For real frames, EAS (2.22),(2.39) gives the canonical squared norm
(1/2)tr(A^T A)+tr(B^T B). ZS (A24),(A26) gives the half-trace orthogonal-group
volume as the product S_0...S_(n-1). Its quotient by O(n-k) therefore has
volume S_(n-k)...S_(n-1). The k*(k-1)/2 independent A coordinates double in
squared norm on passing to the Frobenius metric, giving the stated real
factor. This is a deduction from those two sources. It is not attributed as
a real formula stated by PWTH. For complex frames PWTH (35),(88)–(90)
provides the corresponding embedded volume directly.
An independent route uses Gaussian integration of X=QR with positive real
QR diagonal. Put a_i=beta*(n-i+1)-1 for i=1,...,k. Its triangular integral is
I_R = pi^(beta*k*(k-1)/4) * product_i Gamma((a_i+1)/2)/2.
In the coordinate frame measure, QR has Jacobian product_i r_ii^a_i;
conversion to Frobenius frame volume divides by
2^(beta*k*(k-1)/4). The full Gaussian integral is pi^(beta*n*k/2), hence
V = 2^(beta*k*(k-1)/4)*pi^(beta*n*k/2)/I_R.
The checker evaluates this formula with 600-bit gamma balls, without calling
the generator's sphere recurrence or exact-form reduction. It also evaluates
the complex factorial formula of PWTH (35) and the full-group formulas.
These checks share the geometric volume theorem; they are independent
arithmetic implementations, not independent proofs of that theorem.
External geometric controls are S^0 with volume 2, the circle S^1 with length
2*pi, both components of O(2) with total length 4*sqrt(2)*pi, O(3) with
volume 32*sqrt(2)*pi^2 (ZS A27), and U(2) with volume 8*pi^3 (PWTH 34).
All one-column cases are compared with the stored unit-sphere table T28.
The quotient by the right O(k) or U(k) action has fibre volume V(k,k) and
horizontal squared norm tr(B*B), or (1/2)Re tr(dP^2) for P=QQ*.
The check verifies the quotient's complementary-dimension symmetry on all
nontrivial shapes. Its one-column values agree with the pure-state Bures
volumes in T572 and, after the documented metric rescaling, T571.
No Grassmann volumes are stored as entries in T624.
Every generated transcendental expression is a positive rational multiple
of pi^m or sqrt(2)*pi^m with m>0, so none is rational. The unique rational
member is V_R(1,1)=2 and is returned exactly. Balls are finite and retain
more than 100 significant decimal digits. Checks compare exact rational
endpoints of the written intervals with both the generating and independent
balls, and reject deliberately shifted values and a missing metric factor.
Controls are checked before the full computations. All identities are repeated
on the values read from the private draft after filling it.
Sources and the selection policy are identified in argument-selection.md.
Numerical measurements, source hashes and the governing archived skill
manifest are retained with the run. The separate critique must perform its
own numerical and argument-selection review.