# Mathematical checks for T625

Policy evidence: `agents/runs/20261030T115517Z-build-skills/manifest.json`.
Both skill copies have SHA-256
`28ecbeeccb0c5e5d6eb541b5a5b0f88aec47b154374d909085116d34f5629199`.

## Metric and quotient

At Q = (I_k,0)^T a frame tangent is (A,B)^T, with A skew symmetric or skew
Hermitian. Its Frobenius squared norm is ||A||² + ||B||². The right O(k) or
U(k) fibre consists of the A directions; its metric is precisely the full-frame
Frobenius metric. Horizontal tangents have A=0. Differentiating P=QQ* gives
dP = [[0,B*],[B,0]], whose squared Frobenius norm is 2||B||². Thus the specified
half-projector metric equals the horizontal frame metric. Compact homogeneous
fibres have constant volume, so G_F(n,k)=V_F(n,k)/V_F(k,k).

For real frames EAS (2.39) gives ||A||²/2+||B||² in the canonical metric.
Each independent skew coordinate in A changes its squared norm from 1 to 2;
there are k(k-1)/2 such coordinates. The Gram determinant ratio is
2^[k(k-1)/2], so the volume factor is 2^[k(k-1)/4]. With the half-trace O(n)
volume from ZS (A26), this proves the real product-of-spheres frame formula.
The factor cancels between numerator and fibre. In a full group quotient,
horizontal matrices [[0,-B*],[B,0]] have Frobenius squared norm 2||B||².
Consequently its quotient metric is twice ours and its volume is
2^[beta*k*(n-k)/2] times ours, where beta=1,2. PWTH (92) confirms the complex
scale. The check constructs every real and imaginary horizontal coordinate
and its pairwise Gram entries for all retained shapes; it also checks every
real skew-coordinate determinant. Complementation preserves dP², so it is
an isometry. No oriented real cover is used.

## Exact reduction and numerical independence

The generator reduces
G_F(n,k) = pi^[beta*k*(n-k)/2] product_{i=1}^k
Gamma(beta*i/2)/Gamma(beta*(n-k+i)/2)
to c*pi^e with rational c and integer e. Every selected e is positive, so
there are no exact rational entries concealed as decimals.

The checker computes full group volumes from S_0=2, S_1=2*pi and
S_d = 2*pi*S_{d-2}/(d-1), then takes the group quotient with the scale factor
just derived. It shares no arithmetic helper with the generator. A second
600-bit computation uses unreduced Gamma functions. Both computations must
fit strictly inside the exact rational bounds represented by each 100-digit
serialized value. Finiteness, positivity and relative accuracy are tested
before any comparison. Known-answer controls and a deliberately shifted pi
value exercise the comparison routines before the full family.

For complex Grassmannians the Plücker map pulls back the Fubini–Study metric
to ours: at the reference plane the derivatives of the unit wedge in each
B coordinate are orthonormal. Unitary invariance extends this equality.
Writing D=k(n-k), the Kähler volume is pi^D deg(Gr)/D!, since the Kähler class
is pi times the hyperplane class (normalized by the projective line of area
pi). Buch, Notes on Grassmannians, Exercise 3.12, identifies this degree with
the number of standard tableaux of the k by (n-k) rectangle. The checker
counts them by removing a corner recursively, without a hook-length product
or Gamma factors. Controls give 2 for the 2 by 2 rectangle and 5 for 2 by 3.
All 64 complex coefficients are checked exactly and numerically this way.
This is a connection used to check the volume, not another quantity stored.

The projective slices independently compare all 30 entries with T572's Bures
pure-state volumes, T571's Hilbert–Schmidt pure-state volumes divided by
2^[beta*(n-1)/2], and T28's half-sphere or T27's even-dimensional ball volumes.
These equalities follow from the pure-state metrics; none is a copy of those
stored numbers. No repeats declaration is applied to these theorem-based
coincidences. T624's frame/fibre quotient is also checked on all 128 stored
entries, subject to both tables' finite, narrow serialized enclosures.

The ambient-dimension recurrence is checked wherever two retained rows can
be compared: G_F(n,k)/G_F(n-1,k) = pi^[beta*k/2]
Gamma(beta*(n-k)/2)/Gamma(beta*n/2). Exact complementary coefficients and
independent complementary quotient values are checked for every stored row.
All database checks operate on the text read back, not merely generated values.

## Sources actually read

* https://arxiv.org/html/1607.03132v4 : Section II-D; Theorem 1 (36);
  Appendix B-C (91)–(92).
* https://www.cis.upenn.edu/~cis5150/Stiefel-Grassmann-manifolds-Edelman.pdf :
  Sections 2.3.2 and 2.4.1, (2.28)–(2.31), (2.39).
* https://arxiv.org/pdf/quant-ph/0302197v3 : Appendix A, (A23)–(A28).
* https://sites.math.rutgers.edu/~asbuch/notes/grass.pdf : Exercise 3.12,
  pages 10–11, and Example 3.11's degree-two control.
* Live documents T9, T27, T28, T549, T550, T552, T571, T572 and T624.

The method does not claim to be an independent proof of every cited geometry
theorem. It supplies exact algebra, an independent complex geometric/combinatorial
check, external projective controls, metric-scale checks and certified numerics.