Actual Finite Rectangle Transport

Abstract

Every finite rectangle menu on the positive five-mode fiber has an exact continuous transport realization.

Theorem 1.1 (Exact realization by finite continuous controls).

$$\begin{array}{c}\forall b:\mathrm{Base},\mathrm{ValidBase}\left(b\right)\Rightarrow \\ \forall k_0\in J\left(b\right),\forall A:\mathrm{List}\left({\mathbb{R}}^2\right),\\ (\forall e\in A,\mathrm{fst}\left(e\right)\in J\left(b\right))\Rightarrow \\ \exists q:\mathbb{R}\to \mathrm{State},\mathrm{Admissible}\left(b,\mathrm{Duration}\left(A\right),q\right)\wedge \\ q(0)=(k_0,0,0)\wedge \\ \mathrm{kappa}\left(q(\mathrm{Duration}\left(A\right))\right)=k_0\wedge \mathrm{chi}\left(q(\mathrm{Duration}\left(A\right))\right)=0\wedge \\ (\forall t\in [0,\mathrm{Duration}\left(A\right)],\exists p:\mathrm{InteriorProbability}\left(4\right),\mathrm{weight}\left(p\right)=\mathrm{probability}\left(b,\mathrm{kappa}\left(q(t)\right)\right))\wedge \\ (\forall t\in [0,\mathrm{Duration}\left(A\right)],\mathrm{Compatible}\left(q(t)\right))\wedge \\ \mathrm{phase}\left(q(\mathrm{Duration}\left(A\right))\right)=\mathrm{residual}\left(\mathrm{phaseWeight}\left(b\right),k_0,A\right)\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Fibers/FiniteRectangleTransport.finite_rectangles_realize (✓ std3). ∎

Source. Repository-derived.

Commentary.

The base b is the triple (X,Y,Z), with 0 < Z < 1 and 0 < X,Y < 1-Z. Its open fiber J(b) has endpoints max(0,X+Y-(1-Z)) and min(X,Y). The five probabilities, in the mode order (0,1,2,3,13), are (1-Z-X-Y+k,X-k,Z,Y-k,k). Their strict positivity and total one use the existing InteriorProbability carrier.

The direction is (1,-1,0,-1,1). The information coefficient is the sum of the four reciprocal bottom probabilities. The phase weight w is the direction divided coordinatewise by probability times information. Compatible(q(t)) asserts that the middle phase is zero and that the direction paired with the lifted phases equals the real relation phase. The state of a history q consists of the probability coordinate k, the real lifted relation phase c, and five real lifted phases v. They use the original negative phase convention psi(s)=sqrt(p(s))exp(-iv(s)). The instantaneous weighted phase velocity has zero probability mean, because the sum of p(s)*w(s) is zero. Duration(A) is four times the length of the finite menu A; its phase target is the sum of a times (w(k)-w(k0)) over the entries (k,a).

Admissible(b,N,q) requires continuity of the actual real-time function q, probability coordinates in J(b) on the closed interval from zero to N, finite variation of c, and an affine chart on each unit-time leg. On every open leg and for every mode, the probability derivative equals the direction times the derivative of k, and the derivative of v equals w(k) times the derivative of c. It also requires integrability of every actual transport component and equality of its integral with the corresponding terminal minus initial lifted phase. Thus the supplied object is a piecewise linear control with its transported state lift and exact integral residual.

The public probability_derivative contract is broader than its affine-leg use in this construction. For every b:Base, every real function k:Real->Real, every real slope v, every real time t, every hk:HasDerivAt k v t, and every i:Fin 5, it asserts HasDerivAt (fun s => probability b (k s) i) (direction iv) t. Each probability coordinate is affine in the scalar height k with linear coefficient direction i, so the ordinary chain rule sends the arbitrary height derivative v at the arbitrary time t to direction iv. This general theorem has no ValidBase, positivity, interval, admissible-chart, unit-leg, or transport hypothesis; those conditions belong only to the surrounding construction.

For each menu entry, the four successive vertices change k from k0 to k, change c from zero to a at k, return k to k0, and return c to zero at k0. The phase changes on the two phase legs are a times w(k) and minus a times w(k0). Concatenating these vertices gives the real-time interpolation; matching endpoints prove continuity, and affine charts give finite variation and the differential law.

All real coefficients, including negative and zero coefficients, repeated heights, either symmetry wall, and the empty menu are included. There is no uniform speed, energy or amplitude bound. This declaration realizes every supplied finite representation. The application below constructs representations on every pole stratum and then identifies the exact compact group.

Theorem 1.2 (Middle gauge and unit relation charge).

$$\forall b:\mathrm{Base},\mathrm{ValidBase}\left(b\right)\Rightarrow \forall k\in J\left(b\right),\mathrm{phaseWeight}\left(b,k\right)(2)=0\wedge \mathrm{phaseWeight}\left(b,k\right)(0)-\mathrm{phaseWeight}\left(b,k\right)(1)-\mathrm{phaseWeight}\left(b,k\right)(3)+\mathrm{phaseWeight}\left(b,k\right)(4)=1$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Fibers/FiniteRectangleTransport.weight_compatible (✓ std3). ∎

Source. Repository-derived.

Commentary.

At each interior height, the middle phase weight vanishes and the direction paired with the phase weight equals one. Strict positivity of the four bottom probabilities makes the information coefficient nonzero. These identities govern the transported gauge and relation phase on every finite rectangle and also apply pointwise to general histories.

Let T be finite, let k be continuous on the interval between zero and T with values in the same open fiber, and let alpha be interval integrable. Put H(i) equal to the integral of w(k(t))(i) times alpha(t), and put q equal to the integral of alpha. Each component of w composed with k is continuous: the positive affine probabilities and their positive reciprocal sum keep every denominator nonzero. Multiplication of an integrable function by a continuous function on a compact interval therefore proves that every component defining H is integrable.

Define V(b) by zero middle component, zero direction charge, equality of components 0 and 13 when X+Y=1-Z, and equality of components 1 and 3 when X=Y. Integrating the middle and charge identities gives H(2)=0 and H(0)-H(1)-H(3)+H(13)=q. On either wall the relevant affine probabilities and signs coincide, so the corresponding weights, and then their integrals, coincide. Subtracting q times w(k0), whose charge is one, shows that H-q*w(k0) belongs to V(b). This argument includes both walls simultaneously and does not require a finite affine chart decomposition.

For an absolutely continuous real phase lift chi, alpha is its derivative. The interval fundamental theorem of calculus identifies q with chi(T)-chi(0). Thus winding m gives H-2pim*w(k0) in V(b), and zero winding gives H in V(b). If the five state-phase coordinates are absolutely continuous and satisfy the transport derivative law almost everywhere, the same fundamental theorem identifies H with their terminal minus initial values. Finite variation alone cannot replace absolute continuity in this endpoint statement.

For a continuous phase that is C1 on finitely many consecutive subintervals, choose arbitrary nondecreasing partition times from zero to T. On each open subinterval its derivative agrees with a continuous rate on the closed subinterval. That rate is integrable; changing values at partition endpoints does not change the interval integral. The ordinary fundamental theorem on each subinterval and telescoping of the finite endpoint sum give q=chi(T)-chi(0). Hence the same upper inclusion applies to finite piecewise C1 controls as well, without imposing unit-time legs or affine motion.

When X=Y and X+Y=1-Z, the target equations give exactly h=(t,t,0,t,t), with t any real number. The weight is ((X-k)/(2X),-k/(2X),0,-k/(2X),(X-k)/(2X)). Fix k1=k0+(upper(b)-k0)/4 before selecting t. It is an interior height distinct from k0. The real coefficient a=-2Xt/(k1-k0) makes a*(w(k1)-w(k0)) equal h. Applying finite_rectangles_realize to the actual singleton menu [(k1,a)] supplies a continuous four-leg transport with strict support, the original gauge, zero real winding, and terminal phase h. Negative and zero targets are included. In particular the double wall has a real line of reachable residuals, including nonzero residuals.

At the double wall put r=1-Z. Direct substitution into the existing phaseWeight gives (1/2-k/r,-k/r,0,-k/r,1/2-k/r), throughout 0<k<r/2. For every real s and A with k+s also in this interval, the actual singleton menu [(k+s,A)] in finite_rectangles_realize gives a four-leg Admissible path starting at (k,0,0). Its terminal height is k, its real control phase is zero, and its five lifted increments are (-sA/r,-sA/r,0,-sA/r,-sA/r). Thus the original finite rectangle has exactly the simultaneous phase displacement computed from the affine weight, including either sign and zero A. For nonzero s, taking A=-r*t/s realizes every desired common increment t in this increment gauge. This is a finite original transport calculation, with no limiting bracket argument or additional control generator.

The same double-wall weight gives a local-coordinate calculation without a global angle choice. In real phase charts (k,u,v), put P=(1,0,0), Q=(0,1/2-k/r,-k/r), and C=(0,-1/r,-1/r). The pinned VectorField.lieBracket differentiates Q in direction P and subtracts the derivative of P in direction Q; it is exactly C. For r nonzero, aP+bQ+cC=0 forces a=b=c=0, so the third direction is independent everywhere. The one-form lambda(k)(w)=2kw(u)+(r-2k)*w(v) has kernel exactly span(P,Q). Explicitly, every kernel vector w equals w(k)P+2(w(u)-w(v))*Q, and the reverse inclusion follows by substitution. These formulas calculate the local plane field; a complete contact correspondence additionally requires the exterior derivative, wedge and standard-form pullback on the actual source manifold.

The two-amplitude coordinate map is zPlus=sqrt(2k/r)exp(-iu), zMinus=sqrt(1-2k/r)exp(-iv). For r>0 and 0<k<r/2, both components are nonzero and their squared complex norms sum to one. Thus the pair belongs to the unit sphere in EuclideanSpace over C with two coordinates. Conversely, every point of that sphere with both components nonzero has k=r*norm(zPlus)^2/2 strictly between zero and r/2. Choosing u=-arg(zPlus) and v=-arg(zMinus) recovers both components by norm times complex exponential of argument. This is an exact image characterization, with arguments serving only as existential circle representatives. It keeps the simultaneous phase of the pair. The fixed prepared orthonormal-vector decomposition into the five-mode state and the standard-contact-form pullback require their own correspondences; the sphere image alone proves neither.

For the construction on every stratum, put r=1-Z and A=X+Y-r. The bottom poles, in the source labels (0,1,3,13), are (A,X,Y,0). On the strict base A<X, A<Y, X>0 and Y>0. Thus the only collisions are A=0 and X=Y. Retain representatives 0 and 1, also 3 when X differs from Y, and also 13 when A differs from zero. In Fin 5 the last source label is index 4. The representative map sends 3 to 1 on X=Y and 13 to 0 on A=0, and fixes every other bottom mode. This restores both the pole and the target component in each omitted coordinate. There are g=4-deltaMinus-deltaPlus representatives, where the two indicators record the respective walls.

Fix the base and k0 before choosing the target. Enumerate the representatives by indices j from zero to g-1 and set k(j)=k0+(j/4)*(upper(b)-k0), with real division. Index zero gives k0. Since 2 <= g <= 4 and k0 is strictly below upper(b), these heights are distinct and lie strictly inside the original fiber. Every bottom probability is positive at each height, the information coefficient I is positive, and k(j) differs from every pole. Products of height differences, pole differences, and cross differences are therefore nonzero on every stratum. No genericity assumption removes either wall.

Here are explicit interpolation coefficients. For this fixed height menu define Q(t) as the product of t-k(l) over all g indices, and D(j) as the product of k(j)-k(l) over all l different from j. Let P(h) be the Lagrange polynomial of degree less than g with values h(s)*Q(lambda(s)) at the representative poles lambda(s). Equivalently P(h)(t) is the sum over representative s of h(s)*Q(lambda(s)) times the product, over representatives v different from s, of (t-lambda(v))/(lambda(s)-lambda(v)). Define a(j)=-I(k(j))*P(h)(k(j))/D(j). These are real signed coefficients determined by the target, with all heights already fixed.

The exact pinned Lagrange.interpolate, eval_interpolate_at_node, degree_interpolate_lt, eq_interpolate and interpolate_eq_sum identities give the construction without a determinant assumption. Reconstruct P(h) at the height nodes, evaluate at each representative pole, and divide by Q(lambda(s)). This yields h(s)=sum_j a(j)w(k(j))(s). The representative map extends the equality to all bottom modes; the middle equality uses h(2)=w(k(j))(2)=0. The minus sign in a(j) comes from replacing lambda(s)-k(j) by minus (k(j)-lambda(s)) after interpolation. The probability signs have already canceled in w(s)=1/(I(k-lambda(s))); adding another mode sign would give a different construction.

Apply weight_compatible to the reconstructed five-coordinate vector. It gives sum_j a(j)=h(0)-h(1)-h(3)+h(13). For h in V(b) this sum is zero. Consequently the reference coefficient is minus the sum of the other coefficients, and h is exactly the sum over 1 <= j < g of a(j)*(w(k(j))-w(k0)). The actual list [(k(1),a(1)),…,(k(g-1),a(g-1))] has length g-1 and all its heights are in the strict fiber. Applying finite_rectangles_realize directly to this list gives terminal phase h, zero real winding, the middle-fixed gauge and strict probabilities throughout the path. This includes the general stratum, each single wall separately, their intersection, and all signs or zeros of the coefficients.

The dimension and the rectangle count have matching quantifiers. Restriction to the representative coordinates is a linear equivalence from U(b), the space imposing the middle and wall equations, to the real functions on g representatives. Its inverse copies each representative value to its pole group and assigns zero to the middle mode. Hence U(b) has dimension g. The charge functional on U(b) is onto because w(k0) belongs to U(b) and has charge one. Rank-nullity gives dim V(b)=g-1: three off both walls, two on either single wall, and one on their intersection. On a fixed menu of n heights, the rectangle residual map is a linear map from real n-space to V(b). Surjectivity requires n >= dim V(b). The selected g-1 auxiliary heights attain this bound, and their residual differences form a basis; their coefficients are unique. This lower bound concerns a fixed target-independent menu. Individual targets can require fewer nonzero coefficients.

The finite chart description also identifies an original admissible control. On each closed unit leg, the constructed k and chi agree with affine functions whose derivatives are constant continuous rates; the transported phases obey the stated derivative law on the open leg. The complete path is continuous. The sum of its finitely many leg variations is finite, by the variation formula for adjacent intervals and the Lipschitz bound for each affine chart. It is therefore a finite piecewise C1 control with finite phase variation in the original loop class. Applying the finite piecewise fundamental theorem to every phase coordinate and using the transport derivative equality on each open leg identifies the original integral residual with the actual terminal phase. The original class also contains arbitrary absolutely continuous controls; the general-history upper inclusion above applies to those controls without a finite-chart hypothesis.

For any integer m and any target h with h-2pimw(k0) in V(b), first synthesize that remainder. Prepend the unit-time fixed-height phase leg k=k0, chi=2pimt, theta=2pimtw(k0). Follow it by the rectangle path with its relation phase translated by 2pim and its lifted phases translated by 2pimw(k0). The values match at the join, translations preserve the differential law, and weight_compatible preserves the gauge and exact real relation charge at every time. The final probability coordinate is k0, the relation phase is 2pi*m, and the final lifted phase is h. Every integer, including negative and zero winding, is included. The phase coordinate closes on its original circle; no state or ray return is asserted.

$\forall b:\mathrm{Base},\mathrm{ValidBase}\left(b\right)\Rightarrow \forall kzero\in J\left(b\right),\dim \left(V\left(b\right)\right)=d\left(b\right)\wedge \forall m\in \mathbb{Z},\forall h\in {\mathbb{R}}^5,\mathrm{Reachable}\left(b,kzero,m,h\right)\iff h-2\pi m\mathrm{phaseWeight}\left(b,kzero\right)\in V\left(b\right)$

Here Reachable uses the original absolutely continuous or finite piecewise C1 control class with finite phase variation and the integral of w(k)*chi’, and d(b)=3-deltaMinus-deltaPlus. The necessary inclusion and the explicit list construction prove both directions. The interpolation, dimension and integration tools are classical; their application gives no mathematical priority claim. The original source’s geometric-control and Cauchy-determinant references supply context, not additional hypotheses or a transport realization certificate. There is no imposed uniform speed, energy, coefficient or amplitude bound.

For the original open-prefix query, fix k0 and an arbitrary target v whose middle coordinate vanishes and whose increments satisfy each applicable wall equality. Set L=charge(v) and v0=v-Lw(k0). The unit-charge identity gives charge(v0)=0, and v0 has the same middle and wall constraints. The grouped interpolation menu above realizes v0 with exactly g-1 entries, all heights selected before v. Append the single fixed-height phase leg from control phase zero to L, adding Lw(k0), and one probability leg from k0 to any prescribed kstar in J(b), with phase fixed. The actual polygon has 4*(g-1)+2 unit-time legs and terminal state (kstar,L,v). Its finite affine charts, finite phase variation, full support and exact transport integrals are those of Admissible; its probability and control-phase coordinates satisfy OriginalControl through the finite piecewise C1 alternative. Conversely the integrated original law forces the middle and wall equations for every original control, including the absolutely continuous alternative. Thus the exact real prefix endpoints are J(b) times U(b), without a closing condition.

This realization permits all fixed preparation phases. Translate the control phase by any real c0 and add an arbitrary fixed five-vector thetaInitial to the transported state phases. Derivatives are unchanged. The integral of each original weight against the translated control-phase derivative remains v(i), giving terminal phase thetaInitial(i)+v(i). Choose c0=charge(thetaInitial) to keep the original real relation lift consistent. Wall equations concern the increments v, and impose no equality on preparation phases. All signed coefficients and zero coefficients are legal; the finite-path extension itself also permits an empty supplied menu. Convex probability legs remain in the strict interval, with compact positive range and no uniform speed or variation budget asserted.

For the exact compact holonomy of original Theorem 3.3, use the physical circle T=Real.Angle=R/(2piZ), with its quotient topology and additive group structure. A compact phase is a function from Fin 5 to T, with index 4 denoting the original mode 13. Write [h] for componentwise reduction of a real five-vector h. Define K(b) as the subgroup of these compact phases satisfying phi(2)=0, phi(0)-phi(1)-phi(3)+phi(13)=0 in T, phi(0)=phi(13) on Eminus, and phi(1)=phi(3) on Eplus. Give K(b) the subspace topology of T^5. The reachable set is precisely K(b): the quantifiers are over an integer winding and an actual original control, followed by its integral residual and reduction [h]. This equality involves no topological closure.

The original base b=(X,Y,Z), strict support interval J(b), negative state-phase convention and middle-fixed gauge are the same as in the real construction above. The control class is the original union of absolutely continuous k and chi, or continuous finite piecewise C1 k and chi, with finite phase variation. The upper inclusion holds for both alternatives. The sufficiency witnesses are actual continuous paths with finitely many affine charts, so belong to the second alternative without adding a regularity premise to the target. For either class, the real all-sector equivalence becomes Reachable(b,k0,m,h) if and only if h belongs to U(b) and its real charge h(0)-h(1)-h(3)+h(13) is 2pim. This follows by subtracting 2pim*w(k0), using w(k0) in U(b) with unit charge, and invoking the same real all-sector construction. It is not an assumption that a vector of this charge is already reachable.

For a candidate phi in K(b), choose one real representative of each grouped phase, copy it to every member of its group, and set the middle representative to zero. For example, choose phi(0).toReal and phi(1).toReal, use phi(1).toReal also at mode 3 on Eplus, and phi(0).toReal also at mode 13 on Eminus; use the independent representatives at the other modes off their walls. This gives v in U(b) with [v]=phi. The circle-kernel equation says [charge(v)]=0. The exact circle quotient criterion gives charge(v)=2pin for an integer n. Thus v-2pin*w(k0) is in V(b). Apply the original all-sector construction to this remainder and prepend its signed fixed-height winding leg. The final integral residual is v, with compact phase phi. No real reachability, desired kernel membership of a control output, or component classification is a premise of this sufficiency argument.

The grouped coordinates and coefficient rows retain their actual source order. Off both walls the groups are (0),(1),(3),(13), with row (1,-1,-1,1). On Eminus alone the groups are (0,13),(1),(3), with row (2,-1,-1). On Eplus alone the groups are (0),(1,3),(13), with row (1,-2,1). On the double wall the groups are (0,13),(1,3), with row (2,-2). These four rows suffice here; no generic Smith normal form or orbit-closure theorem is needed.

Here are explicit additive homeomorphisms, with all entries in T and the middle entry shown. Off both walls, send phi to (phi(0),phi(1),phi(3)); its inverse sends (a,b,c) to (a,b,0,c,b+c-a). On Eminus alone, send phi to (phi(0),phi(1)); its inverse sends (a,b) to (a,b,0,2a-b,a). On Eplus alone use the same selected coordinates, but the inverse is (a,b,0,b,2b-a). The charge equation and the respective wall equalities prove both inverse identities. Coordinate projection, addition and subtraction are continuous, so each map and inverse is continuous in the stated subgroup topology. Hence K(b) is topologically additively equivalent to T^3 off the walls and to T^2 on either single wall, in each orientation.

On the double wall put t=phi(1) and d=phi(0)-phi(1). Its charge equation is 2d=0. The pinned circle torsion criterion gives exactly d=0 or d=pi. Identify this two-point subgroup with ZMod 2 by the additive map rho([m])=[pim]. One construction first uses ZMod.toAddCircle into the unit-period circle, then the circle scaling equivalence from period one to period 2*pi. Its injectivity and the two-torsion criterion give a bijective additive map. Both finite two-point spaces have the discrete topology, so this map and its inverse are continuous. The double-wall equivalence is phi mapped to (t,rho inverse(d)), with inverse (t,e) mapped to (t+rho(e),t,0,t,t+rho(e)). This is a continuous additive equivalence K(b) with T times ZMod 2, rather than a set bijection or an additive equivalence without topology.

The real image is exact. Off both walls and on either single wall every point of K(b) has a zero-charge real lift: take real representatives of the selected torus coordinates and substitute them into the displayed inverse formulas. On the double wall a real zero-charge lift has equal positive and negative grouped components; its image therefore has d=0. Conversely every compact point with d=0 is the image of the real vector (t,t,0,t,t), using a real representative t of its common compact phase. Thus the image of V(b) is all of K(b) on the three connected strata and exactly the d=0 subspace on the double wall.

This subspace is the identity component inside K(b). The real additive circle is path connected, and finite products of it are connected. Transport of connected components through each additive homeomorphism gives the whole group in the first three strata. For the double-wall product, the product component theorem gives the circle component times the component of zero in ZMod 2. The latter is its singleton zero because the finite discrete group is totally disconnected. Pulling this product component back gives precisely d=0. Consequently range(h mapped to [h], h in V(b)) equals connectedComponent(0 in K(b)) as sets, with no closure of the real image substituted.

Each prescribed winding sector also has an explicit real lift. Write Q=2pim, and choose real representatives a,b,c of the selected compact coordinates. Off both walls use (a,b,0,c,b+c-a+Q). On Eminus alone use (a,b,0,2a-b-Q,a). On Eplus alone use (a,b,0,b,2b-a+Q). These vectors belong to U(b), have charge Q, and reduce to the desired compact phase because [Q]=0. Thus every integer winding realizes every compact class on either single wall and off both walls; there is no residual discrete component on a single wall.

On the double wall the prescribed-sector condition is d=rho([m])=[pim]. If it holds, choose a real representative t of phi(1) and use v=(t+pim,t,0,t,t+pim). It is in U(b), has charge 2pim, and reduces exactly to phi. Conversely any original control of winding m has a real residual in U(b) with this charge; the double-wall equalities force v(0)-v(1)=pim, so its compact component label is the residue of m in ZMod 2. Therefore the winding-m sector consists exactly of points whose second coordinate under the displayed double-wall equivalence is [m]. This statement quantifies over all integers, including negative winding and zero. A fixed-height circle has grouped difference pi and lands in the other component; its entire compact phase need not be an order-two element. Parity describes its component, not its order within the circle factor.

One can also keep an initially chosen grouped representative v with charge 2pin and correct it to any allowed winding m using integer representative shifts. Off Eminus add 2pi(m-n) only in mode 0; this covers the general stratum and the Eplus-only row (1,-2,1). On Eminus alone add 2pi(n-m) only in mode 1, the negative group of row (2,-1,-1). On the double wall, n and m have equal residues modulo two exactly when m-n=2l for an integer l; add 2pil to both modes 0 and 13. Each correction belongs to U(b), changes the charge to 2pim and has zero compact phase, so preserves [v]. There is no sign restriction on n, m or l. In every case the corrected vector minus 2pimw(k0) lies in the original V(b). Applying the actual all-sector lift gives a continuous finite-chart state path starting at (k0,0,0), ending at the same probability coordinate with real relation phase 2pim and the corrected lifted residual, maintaining Compatible at every time. Its phase transport integral equals that terminal residual in every mode. Thus integer representative sufficiency is connected to the original controls and the original w(k0), including the middle-fixed gauge.

The group assertion concerns actual outputs as well as coordinates. Every original loop output is in K(b), and every point of K(b) is an original loop output by the preceding construction. K(b) is an additive subgroup of T^5; its addition and negation are the ambient ones. The equality with this subgroup supplies exact actual-control realizations of the sum and negative of any reachable compact phases. The associated phase operators are diagonal, hence commute. The classification therefore applies to the exact reachable abelian subgroup.

For the endpoint-multiplicity formula, count vanishing original probabilities at the closed endpoints lower(b) and upper(b). The middle probability remains Z>0. At the lower endpoint, only mode 13 vanishes when X+Y<1-Z, only mode 0 when X+Y>1-Z, and both when X+Y=1-Z. At the upper endpoint only mode 1 vanishes when X<Y, only mode 3 when X>Y, and both when X=Y. The other bottom probabilities are strictly positive by the strict mean hypotheses. Consequently nuMinus=1+indicator(Eminus), nuPlus=1+indicator(Eplus), and dim V(b)=g-1=5-nuMinus-nuPlus. The gcd of these two actual endpoint counts is two precisely on the double wall and one otherwise. The four displayed continuous additive equivalences can therefore be written uniformly as K(b) equivalent to T^(5-nuMinus-nuPlus) times ZMod(gcd(nuMinus,nuPlus)), where ZMod 1 is the trivial topological additive group.

The completion cone angles 2pi/nuMinus and 2pi/nuPlus belong to the original endpoint geometry in Theorem 2.13; the compact-group calculation does not prove those metric statements. The correspondence between rank, component count and endpoint multiplicities uses this specific four-pole sign pattern and its two permitted same-sign collisions. It is not asserted for general symplectic reductions. The circle quotient, finite torsion and connected-component tools are classical, and their displayed application here claims no priority. The exact reachability construction, rather than the geometric-control terminology or determinant references in the original section 3.13, supplies the control bridge. No uniform cost, energy, speed, phase amplitude or adaptive-menu minimum is claimed.

For the fixed-area application of original Theorem 3.5, retain an actual real control (k,chi) on a finite interval [0,T] at the same strict base b and with k(0)=k(T)=k0. Require the original alternative of absolutely continuous k and chi, or continuous finite piecewise C1 k and chi, and finite phase variation. Zero winding means the exact real equality chi(T)-chi(0)=0. Define A by the signed integral of k(t)*chi’(t), and h(i) by the integral of w(k(t))(i)*chi’(t). These definitions concern the actual history and its real lifts. The continuity of k and interval integrability of chi’ make the area integrand integrable, just as they do for the transport components.

Pair a real vector with the fixed initial law by L(h)=sum_i p(k0)(i)*h(i). Pointwise the original affine law gives p(k0)(i)=p(k)(i)-(k-k0)*d(i). The instantaneous mean-zero identity sum_i p(k)(i)*w(k)(i)=0 and weight_compatible, which gives sum_i d(i)w(k)(i)=1, therefore give L(w(k))=-(k-k0). Interval integral linearity for the five integrable components yields L(h)=-A+k0(chi(T)-chi(0)). The fundamental theorem for the absolutely continuous alternative, or the finite-piecewise fundamental theorem for the other alternative, supplies that endpoint difference. Every original zero-winding loop consequently obeys L(h)=-A, including controls with no finite affine-chart description.

Restrict L to the actual V(b) characterized above. The vector u=(1,1,0,1,1) belongs to V(b) on every stratum: its middle entry and direction charge are zero and it obeys both possible wall equalities. Its L value is r=1-Z>0. Thus for every real c, (c/r)*u is in V(b) and has L value c; the restriction is surjective. In particular hA=-(A/r)*u is a point of the level L=-A for every real signed area A, including zero and either sign.

Let K be the kernel of this restricted linear map. The level L=-A is exactly hA+K: subtracting hA turns its equation into L(h-hA)=0, and adding a kernel vector preserves it. This is a nonempty affine subspace of V(b), with direction K. Rank-nullity, using the one-dimensional range and the previously established dimensions of V(b), gives dim K=dim V(b)-1. The affine level therefore has dimension two off both walls, one on either single wall separately, and zero on their intersection. At double symmetry V(b) consists of multiples of u, so the unique real fixed-area residual is -(A/r)*u.

The area level is also exactly the original reachable residual set with prescribed area. Necessity uses the general-control inclusion in V(b) and the integral identity. For sufficiency take any h in V(b) with L(h)=-A. The finite selected-height construction supplies an actual admissible zero-winding state lift with integral residual h. Apply the same identity to that very history: its integral area is A. This proves prescribed-area realization for every vector in the affine level, rather than merely membership of a candidate vector or the existence of a separately chosen area witness.

Common initial phases can be retained throughout this construction. Given any fixed real thetaInitial with thetaInitial(2)=0, translate every constructed state (k,chi,theta) to (k,chi+d paired with thetaInitial,theta+thetaInitial). Translation preserves continuity and the finite affine charts. Its derivatives, strict probabilities, phase variation and signed area agree with the original increments. It starts at (k0,d paired with thetaInitial,thetaInitial), keeps the middle gauge and exact real relation phase, and ends with phases thetaInitial+h. The same translation applies to both comparison rectangles below. No initial bottom phase has been fixed specially to obtain their interference contrast.

Area is retained as a real signed history integral. It is not defined on arbitrary compact phase representatives. Changing a real lift h to h+2piz, for an integer five-vector z, changes the weighted expression by 2pisum_i p(k0)(i)z(i). Equality of compact phases alone consequently cannot define this real area pairing. The fixed-area dimension statements concern real affine levels, with exact real zero winding; reducing phases modulo 2pi is a subsequent operation.

For original Proposition 3.6 take exactly X=1/5, Y=2/5, Z=1/5, k0=1/20, k1=1/10 and k2=3/20. The strict fiber is (0,1/5); neither wall holds. In the source order (0,1,2,3,13), with mode 13 represented by Fin 5 index 4, the original law gives p(k0)=(5,3,4,7,1)/20. Divide each signed reciprocal d(i)/p(k)(i) by I(k), the sum of the four positive bottom reciprocals. This gives w(k0)=(21,-35,0,-15,105)/176, w(k1)=(22,-66,0,-22,66)/176 and w(k2)=(15,-105,0,-21,35)/176. These are the weights of this same probability source.

Use the actual singleton menus [(k1,2)] and [(k2,1)] in finite_rectangles_realize. Each is a four-unit-time rectangle: move from k0 to its selected height at fixed relation phase, raise the real relation phase by its selected phase height, return to k0 at fixed phase, and lower the phase to its initial value at k0. On the probability legs k is affine between positive interior heights; on the phase legs it is constant. The complete paths have strict positive support by the supplier, including all leg junctions. They are continuous with finite piecewise C1 controls and finite phase variation.

The residuals of these actual rectangles are hFirst=2*(w(k1)-w(k0)) and hSecond=w(k2)-w(k0). Their actual signed integrals are 2*(k1-k0)=1/10 and k2-k0=1/10. The two probability legs contribute zero area; the outbound and return phase legs contribute ak and -ak0. Equivalently applying the general integral identity to either supplied rectangle gives this same area from its residual. Both return to k0 with zero real winding and preserve the middle-fixed gauge. Their residual difference is exactly hFirst-hSecond=(1,1,0,-1,-1)/22. Its direction charge is zero, and its initial-probability pairing is zero: modes 0 and 1 together have mass 2/5, as do modes 3 and 13.

For any of the common initial phases, the two actual endpoint amplitudes are sqrt(p(k0)(i))exp(-i(thetaInitial(i)+hFirst(i))) and the same expression with hSecond. In the complex inner product their common initial phases cancel componentwise, leaving sum_i p(k0)(i)exp(i(hFirst(i)-hSecond(i))). The middle contribution is 1/5. The positive and negative difference pairs contribute (2/5)*exp(i/22) and (2/5)*exp(-i/22), so the overlap is the real number 1/5+(4/5)*cos(1/22). Its squared modulus is exactly [1/5+(4/5)*cos(1/22)] squared. Since 0<1/22<pi/2, its cosine is positive; strict decrease of cosine between zero and pi also makes it less than one. The bracket, and then its squared modulus, are strictly between zero and one.

These endpoints are different rays in the actual complex projective space. Their middle amplitude is the same nonzero number, because the initial phases agree and both middle increments vanish. A scalar identifying their rays would therefore equal one. Equality at mode 0 would then require exp(i/22)=1, contradicting cos(1/22)<1. The overlap inequality gives the same distinction between normalized endpoint states. Thus equal real signed area does not determine the endpoint ray at this original generic positive base. The pair is distinct from the uniform-probability rectangle example of section 2.6.

These consequences reuse the original probability, transport, real reachability and projective carriers together with classical interval integration, rank-nullity and complex exponential identities. They concern exact mathematical controls and ideal endpoint amplitudes. They impose no speed, energy, duration optimization, amplitude budget or finite-shot discrimination claim, and do not extend the positive-support gauge to a missing middle mode. The fixed-area assertion is confined to real zero winding; arbitrary-winding double-wall summaries, tensor spectra, support limits, conditioning, variation estimates and the coherence-history quotient require their respective further hypotheses and conclusions.

For the integral and compact parts of original Theorem 3.7, specialize the same law to X=Y=r/2, where r=1-Z>0. The modes remain (0,1,2,3,13), with Fin 5 index 4 denoting mode 13. Their probabilities are (k,r/2-k,Z,r/2-k,k), and the strict control interval is 0<k<r/2. Put b0=(1,1,0,1,1) and eplus=e0+e13=(1,0,0,0,1). Substitution in the original reciprocal information gives I(k)=r/[k*(r/2-k)]. Hence the original weight is w(k)=(1/2)*eplus-(k/r)*b0. This uses the original signed direction (1,-1,0,-1,1) and its original normalization, rather than a surrogate transport law.

Take any original admissible loop (k,chi) on [0,T], with k(0)=k(T)=k0, strict support at every time, finite phase variation, and the original alternative: k and chi are absolutely continuous, or they are continuous and C1 on a finite partition. Its winding is the exact real equation chi(T)-chi(0)=2pim for an arbitrary signed integer m. In either alternative chi’ is interval integrable and its integral is the endpoint difference. Continuity of k on the compact interval makes kchi’ integrable, so A=integral kchi’ is a finite real signed area. Componentwise integration of the displayed affine weight gives h=pimeplus-(A/r)b0. Thus h0=h13=pim-A/r, h1=h3=-A/r and h2=0 for every original history, including ones with no finite affine synthesis description. Finite affine controls supply realizations, not a necessary description of this entire control class.

Set the source circle coordinate t=phi0=pim-A/r modulo 2pi and e=m modulo 2. The compact residual is (t,t-pim,0,t-pim,t). The earlier doubleEquiv uses phi1 as its first coordinate, so its coordinates are (s,e) with s=phi1=-A/r modulo 2pi. The conversion is t=s+rho(e), where rho([m])=[pim]; conversely s=t-rho(e). These are different circle coordinates related by an additive homeomorphism of the circle times ZMod 2. In particular the source t is not the first coordinate of doubleEquiv.

This source circle/parity pair is unique on positive-support endpoint rays at a common base and common initial phases. Write the endpoint amplitude as sqrt(p_i(k0))exp(-i(thetaInitial_i+h_i)), with thetaInitial_2=0. If two such endpoints differ by a complex scalar, their equal nonzero middle amplitude forces the scalar to be one. Every other amplitude is nonzero as well, so componentwise equality is equivalent to equality of the residual phases modulo 2*pi. Mode 0 then determines t; the difference between modes 0 and 1 determines rho(e), whose injectivity determines e. Conversely equal t and e give equal compact residuals and therefore equal endpoint amplitudes. This argument allows arbitrary common initial bottom phases and uses the positive middle mass explicitly.

Every source circle/parity pair is actually reachable with those specified common initial phases. Choose any real representative t and any signed integer m with the requested parity, and put A=r*(pim-t). The vector (t,t-pim,0,t-pim,t) belongs to the original U(b) and has charge 2pim. Subtracting 2pimw(k0) puts it in V(b), so the actual all-sector synthesis supplies an admissible finite affine state lift at the same base. Translate that lift by thetaInitial, and its relation phase by the charge of thetaInitial, as in the common-initial-phase construction above. It begins at (k0,charge(thetaInitial),thetaInitial), ends at the same k0 with the displayed increment, and remains Compatible throughout. Applying the general integral identity to this very history gives its real area A. The arbitrary-history formula and this actual realization establish both directions of the circle/parity summary.

The compact pair does not specify a unique real area: real representatives and integer windings remain part of a history lift. Equality of compact phases does not license assigning a representative-independent real integral to the circle. Nor does a circle coordinate encode an arbitrary phase in finitely many bits. The summary describes exact mathematical endpoints, with no finite-shot discrimination or path-reconstruction assertion. The legal tensor-operator equality in Theorem 3.7 requires the declared embedding of section 3.8 and is a separate obligation from these integral, compact and ray statements.

The equal-real-area opposite-parity witness is an actual concatenation. Choose any distinct interior height ka, let alpha=-2pik0/(ka-k0), and use five unit-time legs starting from k0 and the current relation phase chiEnd. First keep k=k0 and increase chi by 2*pi. Next move k from k0 to ka at fixed chi. At ka increase chi by alpha, return k from ka to k0 at fixed chi, and finally change chi by -alpha at k0. The last four legs form the rectangle appended to the winding-one circle. Both heights lie in the strict interval, their affine connecting segments do too, and alpha is a finite real number because ka differs from k0. The construction has finite time and phase variation, including either sign of alpha.

More precisely, append these legs to any original loop on [0,T]. For 0<=u<=1 the five successive controls (k,chi), at times T+u, T+1+u, T+2+u, T+3+u and T+4+u, are respectively (k0,chiEnd+2piu), (k0+(ka-k0)u,chiEnd+2pi), (ka,chiEnd+2pi+alphau), (ka-(ka-k0)u,chiEnd+2pi+alpha), and (k0,chiEnd+2pi+alpha(1-u)). They agree at every junction and with the original endpoint. The original controls are left unchanged on [0,T]. Appending an affine leg to an absolutely continuous control preserves absolute continuity; for a finite-piecewise-C1 control append one chart to its finite partition. Continuity and bounded variation are preserved under this finite concatenation, and convexity of the strict interval preserves support on the probability legs. Thus the resulting history obeys the same original regularity alternative.

Area and transport are additive for this concatenation. On the original interval the controls and their derivatives almost everywhere agree with the original history. The finitely many junctions have zero measure. Interval-integral additivity then separates the five new legs: the three phase legs contribute 2pik0, alphaka and -alphak0 to area, while the two probability legs contribute zero. Their sum is 2pik0+alpha*(ka-k0)=0 exactly. The phase endpoint increases by 2pi, so winding m becomes m+1 for every integer m, including zero and negative integers. The residual increment is 2piw(k0)+alpha(w(ka)-w(k0)); at double symmetry the affine weight reduces this to pi*eplus. Consequently the prescribed real area A is preserved and the winding parity flips. This is postcomposition of each given actual history, rather than a separately realized endpoint with matching invariants.

The phase lift can be kept on the same concatenated controls and initial gauge. Define theta_i(s)=thetaInitial_i+integral from 0 to s of w(k(x))_ichi’(x). Each component is absolutely continuous with finite variation and obeys the original transport derivative almost everywhere. Restricting the original controls to each prefix, the same fundamental theorem and weight_compatible give theta_2(s)=0 and charge(theta(s))=chi(s), provided chi(0)=charge(thetaInitial). Hence the lift is Compatible along the whole path. The unchanged prefix controls give unchanged prefix phase integrals. Its endpoint at double symmetry is thetaInitial+h+pieplus. Starting from the constant loop gives an actual odd-winding loop of exactly zero area at the same base and initial phases; the constant comparison has winding zero and area zero. Appending it to any prescribed-area loop retains that loop’s base and initial phases and flips parity without changing its real area.

For original Proposition 3.9 return to every valid base b, without imposing either wall. The vector b0 belongs to V(b): its middle entry is zero, its direction charge is 1-1-1+1=0, and it satisfies each possible same-sign wall equality. Thus tb0 belongs to V(b) for every real t. The actual zero-winding realization supplier, followed by the same initial-phase translation, produces a strict-support loop beginning at (k0,charge(thetaInitial),thetaInitial) and ending at (k0,charge(thetaInitial),thetaInitial+tb0). Its original transport integrals are exactly tb0. The same realized history has area -rt by the general pairing identity. Reachability here is actual synthesis for every valid base and parameter, rather than an assumed subgroup action.

At this positive base define the normalized bottom state B by B_i=0 for i=2 and B_i=sqrt(p_i(k0))exp(-ithetaInitial_i)/sqrt(r) otherwise. The original law sums the four bottom probabilities to r=1-Z>0; the complex exponentials have norm square one. Hence sum_i normSq(B_i)=1 and B is orthogonal to the unit vector in mode 2. With thetaInitial_2=0 the original state is psi=sqrt(r)B+sqrt(Z)e2. The reachable increment tb0, with the original negative phase convention, gives exactly psi_t=exp(-it)*sqrt(r)*B+sqrt(Z)*e2. Arbitrary common initial bottom phases are retained in B.

For the complex inner product use sum_i conjugate(psi_i)psi_t_i. The common initial phases cancel componentwise; the four bottom terms sum to rexp(-it), and the middle term is Z. Therefore normSq of the overlap is normSq(rexp(-it)+Z). Expanding its real and imaginary parts gives rr+ZZ+2rZcos(t). Substituting r+Z=1 and cos(t)=1-2sin(t/2)^2 gives exactly 1-4rZsin(t/2)^2. The sign inside the complex exponential is negative. This formula is a fixed-reference interference contrast for the actual reachable endpoints, not an assertion that Schmidt spectra detect this action.

At Z=0 use a separate boundary carrier: complex five-vectors v with v_2=0 and sum_i normSq(v_i)=1, allowing any bottom entries to vanish. An original nonnegative boundary probability law with total one and arbitrary phases gives such a vector by the same square-root amplitude formula; no strict-positive middle probability or positive-base gauge is required. On this carrier the b0 action is exp(-i*t)*v, a common scalar phase, since its four bottom entries are one. The boundary value r=1, Z=0 of the overlap formula is correspondingly one. The positive-support proof that a scalar must equal one has no application here: its nonzero middle amplitude is absent.

Parity can nevertheless survive on boundary support. Let D multiply modes 1 and 3 by -1 and modes 0,2,13 by +1. If v has a nonzero entry in {0,13} and a nonzero entry in {1,3}, then D*v cannot be a scalar multiple of v. Equality on the first nonzero entry would force that scalar to be +1; equality on the second would force -1. This condition does not demand that all four bottom amplitudes be nonzero. It shows why scalarity of the continuous b0 subgroup does not imply that all holonomy disappears when middle support vanishes. It is a support-level action statement; the positive-base reachability and unique-gauge proofs do not mechanically extend to a new boundary control problem.

The integral, compact, actual-concatenation and support applications above use the original five-mode probability and phase carriers, the actual synthesis construction, weight_compatible and classical interval-integral, absolute-continuity, circle and complex-exponential identities. They introduce no additional probability law, tensor embedding, cost calibration or literature-priority claim. The legal operator factorization and all fixed-position Schmidt spectra, the intermediate probability-leg counterexample, determinant conditioning, variation estimates and the coherence-history quotient retain their separate required statements and hypotheses. Completion of this integral/parity and bottom-versus-middle application does not settle those obligations or the full source.

For the operator and observation applications, keep the original five probabilities p(k)=(r-X-Y+k,X-k,Z,Y-k,k), r=1-Z, source order (0,1,2,3,13), and index 4 for mode 13. Every necessity statement ranges over the original controls on a finite interval [0,T]: continuous k and chi, k(t) in the strict open fiber at every time, finite variation of chi, and either absolute continuity of both controls or continuous finite piecewise C1 controls. Their actual residual is h_i=integral w_i(k(t))chi’(t). The previously derived integral inclusion and fundamental theorem give h_2=0 and h_0-h_1-h_3+h_13=2pi*m for each signed integer winding m. Finite affine synthesis supplies existence and never restricts this necessity class.

Allow any identical initial phase vector thetaInitial in the comparisons. If its middle entry is nonzero, subtract that entry from all five phases to use the original Compatible carrier, then restore it as one common phase. The direction charge is unchanged by this translation. The transported middle phase remains thetaInitial_2, while every residual has middle entry zero. Thus the middle-fixed residual gauge and the original negative convention psi_i=sqrt(p_i)exp(-i(thetaInitial_i+h_i)) coexist with arbitrary common initial phases. Positive support makes every amplitude, including the unchanged middle one, nonzero.

Use the declared embedding into the three binary position factors, in low, middle, high order: 0=000, 1=100, 2=010, 3=001, 13=101. The source occupation coordinates x,y,z mean low, high, middle; their position ordering is therefore x,z,y. On a binary position let N=diag(0,1). Its matrix exponential exp(-iaN) is diag(1,exp(-i*a)). Kronecker multiplication of the low, middle and high factors gives an operator on the eight-dimensional tensor space. Restriction to the five declared basis vectors gives the legal five-dimensional operator; all other three basis vectors have zero amplitude in an embedded legal state.

For an actual residual put a=h_1-h_0, b=h_3-h_0 and c=-h_0. The coefficient of exp(ic)[exp(-iaN_1) tensor exp(-icN_2) tensor exp(-ibN_3)] at the legal modes 0,1,2,3 is respectively exp(-ih_0), exp(-ih_1), 1 and exp(-ih_3). At mode 13 it is exp(-i*(h_1+h_3-h_0)). The actual charge identity gives h_13=h_1+h_3-h_0+2pim, so integer periodicity gives the same coefficient exp(-i*h_13). Off-diagonal entries vanish. This proves equality of the actual operators on the whole legal subspace for every signed winding, and therefore their actions agree on every legal complex vector, with arbitrary amplitudes and initial phases.

On the double wall use the actual integral result h=pim(e_0+e_13)-(A/r)b0, where b0=(1,1,0,1,1), A is the real signed integral and t=pim-A/r. The legal bottom projector b0hat=diag(1,1,0,1,1) has exponential exp(-itb0hat)=diag(exp(-it),exp(-it),1,exp(-it),exp(-it)). The position Pauli operators are Z_1=exp(-ipiN_1) and Z_3=exp(-ipiN_3), restricted to the legal space. They are unitary; Z_1*Z_3 is diag(1,-1,1,-1,1). Its integer power is defined in the unitary group, including negative m, and has coefficients (1,(-1)^m,1,(-1)^m,1). The position symbol Z_j is distinct from probability mass Z=p_2.

Multiplying these two actual matrices gives exp(-ih_i) at every legal mode. For modes 1 and 3, exp(-it)exp(-ipim)=exp(-i(t-pim)), because the two exponents differ by -2pim. For modes 0 and 13 the Pauli product is one, and the middle coefficient is one. Thus U_loop=exp(-itb0hat)(Z_1Z_3)^m on the declared legal subspace. The initial phases do not enter this operator identity. The area here is the real history integral; t modulo 2pi and m modulo two give the endpoint summary without defining a representative-independent compact area.

Fix any subset S of the three positions and its complement Sc. A bit assignment x corresponds bijectively to its restrictions u on S and v on Sc; the inverse joins those two assignments. This reindexing uses the declared tensor positions and includes every subset, both complementary choices and the empty and full subsets. For an embedded legal vector define the coefficient matrix M(u,v)=psi(join(u,v)). Its entries are exactly the amplitudes of the same tensor state in this partition, rather than a new tensor product. The side dimensions are 2 to the cardinality of S and 2 to the cardinality of Sc.

Let d=(a,c,b) in position order. The phase on a joined bit string separates as exp(-isum over S of d_ju_j) times exp(-isum over Sc of d_jv_j). Let L and R be the corresponding diagonal side matrices, absorbing the common scalar exp(ic) into L. Each diagonal entry has modulus one, so both matrices are unitary. Expanding the Kronecker action shows that the transformed coefficient matrix is LM*transpose(R): its (u,v) entry is sum over u’,v’ of L(u,u’)*M(u’,v’)*R(v,v’). The right action is transpose(R), as required by coefficient indexing. It is not inferred to be an adjoint from unitarity.

The retained-side reduced density matrix is Madjoint(M). Under the position action it becomes LM*transpose(R)*adjoint(transpose(R))adjoint(M)adjoint(L)=L(Madjoint(M))*adjoint(L), since the transpose of a unitary is unitary. This Gram matrix also equals partialTraceRight of the pure outer-product matrix after the subset/complement reindexing: the traced factor is the complement. This identifies the algebraic Gram matrix with the actual reduced density matrix for every declared partition. The companion naming partialTraceLeft would retain the other factor.

Pinned Matrix.charpoly_mul_comm and the unitary inverse identity give equality of the two reduced characteristic polynomials. Pinned Matrix.IsHermitian.eigenvalues_eq_eigenvalues_iff then gives equality of the complete finite eigenvalue lists, including repeated values and zeros. The sorted eigenvalues are nonnegative for these Gram matrices. The Schmidt coefficient list is their nonnegative square roots, retaining min(2^card(S),2^card(Sc)) entries in decreasing order, with zero coefficients kept. Equality of the full reduced eigenvalue lists implies equality of this list. This argument handles all fixed declared-position partitions and all legal vectors; it does not replace spectra by rank, determinant or a set that discards multiplicity. For actual loop endpoints the probability law is the same p(k0), so arbitrary identical initial phases are retained throughout the comparison.

Intermediate probability control has a different conclusion. At zero phases the coefficient matrix for middle versus the ordered outer pair (low,high) has rows (sqrt(p_0),sqrt(p_3),sqrt(p_1),sqrt(p_13)) and (sqrt(Z),0,0,0), with columns 00,01,10,11. Multiplication by its adjoint gives exactly the matrix with rows (r,sqrt(Zp_0)) and (sqrt(Zp_0),Z). The four bottom probabilities sum to r, and only the amplitudes at 000 and 010 share the outer pair 00. Its determinant is Z*(r-p_0), using p_0>=0 and Z>=0 to square the square-root product. This is derived from the actual five amplitudes and the same middle partition.

An exact strict-support witness fixes X=Y=2/5, Z=1/5 and r=4/5, with k moving from 1/20 to 1/10. The two original probability vectors are (1/20,7/20,1/5,7/20,1/20) and (1/10,3/10,1/5,3/10,1/10). Every entry is positive and each vector sums to one. The low and high means are both 2/5 and the middle mean is 1/5 at both points and throughout the affine fiber. On the unit-time leg k(s)=1/20+s/20, keep chi and all phases zero. Its controls are continuous affine, hence absolutely continuous and finite piecewise C1, with zero phase variation. All k(s) remain strictly between 0 and 2/5, and the original transport derivative is zero because chi’=0.

At the two ends of this probability leg the middle reduced determinants are 3/20 and 7/50, respectively, and both traces are one. Equality of the complete eigenvalue lists would force equality of their products, contradicting these exact determinants. The lists therefore differ; their nonnegative square-root Schmidt coefficients differ as well. This exhibits an admissible original probability leg whose intermediate middle spectrum changes. It can be the first leg of an original rectangle. The endpoint invariance statement compares the beginning and end of a loop at the same law, not the ends of this probability leg at different laws.

For the ideal coherence menu take the five oriented source edges 01,02,03,1-13,3-13, with 13 again index 4. Define matrix units E_ij=|i><j| and the actual Hermitian observables A_ij=E_ij+E_ji and B_ij=-iE_ij+iE_ji. Expanding sum over u,v of conjugate(psi_u)*O(u,v)psi_v gives expectations 2Re(conjugate(psi_i)psi_j) and 2Im(conjugate(psi_i)*psi_j). Thus equality of the two real expectations on one edge is equivalent to equality of the same complex edge product; the factor two is retained in both observables.

For an actual endpoint the edge product is sqrt(p_i)*sqrt(p_j)exp(i(thetaInitial_i+h_i-thetaInitial_j-h_j)). Its positive prefactor can be canceled because both endpoints have the same strict-support base. The common initial phases then cancel, and equality is precisely [h_i]-[h_j]=[g_i]-[g_j] in Real.Angle. Form the undirected graph from exactly the five declared edges. Modes 1,2,3 connect directly to 0; mode 13 connects by 0-1-13, also by 0-3-13. Its preconnectedness allows direct application of SparseCharacterSynchronization.edge_difference_kernel_eq_constants_iff with the additive circle group. The difference between the two compact phase functions is therefore constant. Its middle value is zero because the actual residuals both have zero middle entry, so the constant vanishes. Conversely identical compact residuals give identical edge products and all ten expectations. This proves both directions for any two actual histories with arbitrary identical initial phases.

The compact group in this correspondence is the original K(b), imposing the middle, relation-charge and applicable same-sign wall equations on circle labels. The actual all-sector reachability result supplies every element of K(b); no reachability premise is added to the observation theorem. In particular off both walls it is three circles, on either single wall it is two circles, and on their intersection it is a circle times ZMod 2. The supplied offEquiv, minusEquiv, plusEquiv and doubleEquiv identify these groups. For any desired compact label choose its actual real residual and signed winding, synthesize its finite strict-support controls, translate by thetaInitial-thetaInitial_2, and restore the common middle phase. This realizes the label at the specified common base and phases while preserving finite time, variation and original transport.

At that same base the probabilities-only menu has the same value for every loop history, since normSq(psi_i)=p_i(k0). Every fixed declared-position Schmidt-only menu also has the same value for every pair of actual histories by the full spectrum equality above. The complete coherence menu identifies exactly equal compact residuals, and distinguishes different compact labels at the level of ideal expectations. It specifies no number of shots and no perfect finite-shot discrimination, nor does it assign a resource or energy calibration.

Path recovery fails for an explicit original control. At the strict witness base and k0=1/20, use four unit-time legs: move k to 1/10 at fixed chi, raise chi by one, return k to 1/20 at fixed chi, and lower chi by one. Follow those same legs in literal reverse order and direction. The eight probability slopes are (1/20,0,-1/20,0,0,1/20,0,-1/20), and the eight relation-phase slopes are (0,1,0,-1,1,0,-1,0). The second half satisfies k(t)=k(8-t) and chi(t)=chi(8-t) for 4<=t<=8. The control has finite time and finite phase variation, all heights and connecting segments retain strict support, and the two halves have opposite transport integrals. Its actual residual is zero, its lifted terminal phases equal the arbitrary common initial phases, and its endpoint law and compact label equal those of the constant loop. Nevertheless k(1)=1/10 differs from k(0)=1/20, so this history is nonconstant.

For four prescribed strictly ordered heights k0<k1<k2<k3 in J(b), define the real matrix C with rows (0,1,3) and columns w(kj)-w(k0), j=1,2,3. The bottom matrix W has four rows (0,1,3,13) and those four weight columns. Its entry is I(kj) inverse times (kj-lambda_i) inverse, with poles (X+Y-r,X,Y,0). The strict base makes the first pole less than X and Y, and X and Y positive. Thus all poles are distinct off exactly the two symmetry walls. Interior positivity makes every height-pole cross denominator nonzero. The signed charge of each weight is one; replacing the last row by the signed row sum, then subtracting column zero from the other columns, proves det(W)=-det(C). The absolute determinant equality has factor exactly one.

Apply the real specialization of the classical Cauchy double alternant to this matrix. The height product is the product of kj-ki for all six pairs i<j. The absolute pole product is XY(r-X)(r-Y)*absolute(X-Y)*absolute(X+Y-r). At each column, the product of the four absolute cross differences is exactly the product of the original four bottom probabilities; the two negative cross factors correspond to modes 1 and 3. Multiplying by I groups the four positive triple products into Qb(k)=XY(r-X-Y)+2XYk-rk squared. Therefore absolute(det(C)) is XY(r-X)(r-Y)*absolute(X-Y)*absolute(X+Y-r) times the six height differences, divided by the product of Qb at all four heights. No condition r-X-Y>0 is used. Neither symmetry and strict height order make this determinant nonzero.

For every h in the original V(b), solve the three selected rows with a=C inverse applied to (h0,h1,h3). Each column difference has zero middle component and zero relation charge. The target satisfies h2=0 and h13=h1+h3-h0, so the three-row solution recovers the whole five-component residual. These coefficients are unique at the supplied heights, which need not be the existential menu chosen by selected_coefficients_unique. Pass the actual menu [(k1,a1),(k2,a2),(k3,a3)] to finite_rectangles_realize. It gives twelve unit-time legs, returns to the prescribed base height k0 with zero winding, and has exactly residual h. Applying the original initial-phase translation gives the same construction from every compatible theta with theta2=0 and initial relation phase equal to its charge. The endpoint phases are theta+h; all intermediate states are compatible, all probabilities stay strictly positive, time and phase variation are finite, and the original derivative and integral laws hold. This is an actual finite control realization of the inverse coefficients.

For a family of such four-height matrices assume one fixed epsilon>0 bounds every bottom probability at each of the four sampled heights. The sampled denominator margin gives Qb>=4epsilon cubed and the four-column denominator product is at least (4epsilon cubed) to the fourth power. Each reciprocal term is at most I, so every absolute weight is at most one and every absolute matrix entry is at most two. The positive base factors X,Y,r-X,r-Y, both absolute symmetry gaps, and all six positive height differences are at most one. Thus absolute(det(C)) is bounded by any selected gap or height difference divided by that fixed denominator lower bound. If either gap tends to zero, or any height pair coalesces, squeezing proves determinant decay. These assumptions permit the base and all heights to vary together.

Use Matrix.toEuclideanLin on real Euclidean dimension three. The pinned norm determinant identity gives absolute(det(C))=sigma0sigma1sigma2. Its singular-value sequence is decreasing and nonnegative, hence sigma2 is the minimum among the three finite indices and sigma2 cubed is at most absolute(det(C)). Continuity of the nonnegative cube root therefore gives sigma2 tending to zero. The minimum here is index 2, without taking an infimum over the infinite sequence padded with zeros. Continuity of the determinant implies that every convergent matrix subsequence has determinant zero. This is a statement about conditioning of these exact synthesis coordinates. Without the uniform sampled margin no endpoint determinant-decay assertion follows. The variation bounds below require a margin at every point of the original control path; they do not follow from sampled margins alone.

The determinant application fixes the full original law and the ordered real height menu before the target is chosen. In the displayed formula HeightProduct means the product of kj-ki over all six pairs 0<=i<j<=3, and DenominatorProduct means Qb(k0)*Qb(k1)*Qb(k2)*Qb(k3). C has the source row order (0,1,3) and column order (k1-k0,k2-k0,k3-k0) in weight differences, with r=1-Z. All four heights are arbitrary strictly ordered points of J(b), and the base satisfies neither X=Y nor X+Y=r.

$\Vert \det \left(C\right)\Vert =\frac{XY(r-X)(r-Y)\Vert X-Y\Vert \Vert X+Y-r\Vert \mathrm{HeightProduct}\left(\right)}{\mathrm{DenominatorProduct}\left(\right)}$

The four-height determinant calculation depends on the external complex Cauchy identity RepresentationTheory.CauchyDeterminant.cauchy_det from mathlib-initiative/Etingof-RepresentationTheory-draft1, in clean-code/release/RepresentationTheory/CauchyDeterminant.lean at commit c6d86a8bd52065aafb8251fa1cdcd55b609743ef, licensed under Apache 2.0 with its LICENSE, NOTICE and README provenance. The real application embeds the original real poles and heights into that complex identity and returns the real determinant. The upstream Mathlib pin is 905b95818eb32af7874a58b427f50c1711a5e96c; the project Mathlib pin is db584cd6d46c92f209a44c0f1c829460d327499d. Pinned Matrix.nonsing_inv_mul supplies the inverse solve, while finite_rectangles_realize and the original compatible initial-phase translation supply the actual-control bridge.

The sampled Q floor follows directly from the original probabilities. With bottom indices (0,1,3,13), I=1/p0+1/p1+1/p3+1/p13 and Q=Ip0p1p3p13. Thus Q=p1p3p13+p0p3p13+p0p1p13+p0p1p3. Each term is positive on J(b); when all four masses are at least epsilon>0, each is at least epsilon cubed and Q>=4*epsilon cubed. This argument includes r-X-Y negative or zero, without requiring r-X-Y>0. The floor applies at each prescribed sampled height; it imposes no condition on a later path between samples.

For the phase-variation bounds retain the same strict base b=(X,Y,Z), r=1-Z>0, middle-fixed gauge, signed direction (1,-1,0,-1,1), and negative state-phase convention. For an interior k, subtraction of the actual signed reciprocal weights gives w1-w3=(X-Y)/(Ip1p3) and w0-w13=(X+Y-r)/(Ip0p13). These are signed real identities, including negative gaps and both exact walls. Apply pinned Finset.sq_sum_div_le_sum_sq_div to the four positive bottom masses with all numerators equal to one: their sum is r, so 16/r<=I, equivalently I*r>=16. No new coercivity assumption is introduced.

At any height where the four bottom masses are at least epsilon>0, the relevant two-mass product is at least epsilon squared. Positivity permits multiplication and division of I*r>=16, giving both pointwise estimates absolute(w1-w3)<=absolute(X-Y)r/(16epsilon squared) and absolute(w0-w13)<=absolute(X+Y-r)r/(16epsilon squared). All signs and both vanishing gaps are covered. These bounds are direct applications of the four-mass inequality and the reciprocal identities.

Let T>=0 be finite. The original OriginalControl requires continuous k and chi on [0,T], k(t) in J(b), finite variation of chi, and either both controls absolutely continuous or both controls continuous finite piecewise C1 with a finite nondecreasing partition and continuous derivative rates on each closed piece. Require k(0)=k(T)=k0 and chi(T)-chi(0)=2pim for any signed integer m. Take alpha=deriv chi and h_s=integral from zero to T of w_s(k(t))*alpha(t); put Vchi=integral from zero to T of absolute(alpha(t)). The absolutely continuous fundamental theorem, or the finite-piecewise fundamental theorem and endpoint telescoping, gives integrability of alpha and its integral equal to that exact real phase increment. Continuity of k and the nonzero positive denominators make w_s composed with k continuous; the original original_integrals application therefore gives integrability of every weighted component and of the area integrand. These are the actual original controls, without replacing their general regularity alternative by finite affine synthesis.

For this entire actual loop assume one epsilon>0 bounds p0,p1,p3,p13 at every time of the closed interval [0,T], including junctions and endpoints. Integral subtraction gives h1-h3=integral (w1-w3)*alpha and h0-h13=integral (w0-w13)*alpha. Apply pinned intervalIntegral.abs_integral_le_integral_abs and intervalIntegral.integral_mono_on to each integrable difference, then intervalIntegral.integral_const_mul. Integrating the pointwise estimates against absolute alpha proves both displayed whole-path inequalities. Every signed winding is retained; no zero-winding or surrogate-residual premise is added.

$\Vert h_1-h_3\Vert \le \frac{\Vert X-Y\Vert r}{16epsilo{n}^2}\mathrm{Vchi}\left(\right),\Vert h_0-h_{13}\Vert \le \frac{\Vert X+Y-r\Vert r}{16epsilo{n}^2}\mathrm{Vchi}\left(\right)$

For either coordinate pair write Delta=h1-h3 with gap=X-Y, or Delta=h0-h13 with gap=X+Y-r. If gap is nonzero, r and absolute(gap) are positive, and division of the corresponding inequality yields Vchi>=16epsilon squaredabsolute(Delta)/(r*absolute(gap)). This holds for all real Delta, in particular any nonzero real target. At an exact wall the upper bound is zero, so the corresponding real difference is exactly zero. The conclusion holds for the same actual residual and control that supplied Vchi.

For compact targets let phi_s be the period-2pi circle classes of the real residual h_s. The invariant distances are dMinus=norm(phi1-phi3) and dPlus=norm(phi0-phi13). Pinned QuotientAddGroup.norm_mk identifies norm([x]) with infDist(x,2piZ), where 2piZ is the additive subgroup of all integer multiples of 2pi. This distance is unchanged by choosing any other real lift, and because zero belongs to the subgroup it is at most absolute(x). Consequently every real lift x of either compact difference satisfies the corresponding compact lower bound Vchi>=16epsilon squarednorm([x])/(r*absolute(gap)) whenever it realizes the original loop difference; equivalently use dMinus or dPlus for the two target coordinates. For every actual real vector lift of the compact target, substitute h1-h3 or h0-h13, respectively, in the real bound. A chosen wrapped coordinate need not be the invariant distance and cannot provide a bound on every realization.

The sampled-margin conditioning statement and the whole-path-margin variation statement use distinct hypotheses. The first controls denominators and the least of the three finite singular values of the prescribed synthesis matrix; the second controls the total real relation-phase variation of each original admissible loop. Neither gives a calibrated energy, speed, elapsed-time or finite-shot discrimination bound. All quantitative consequences here use the transport and positivity results, the original integral-control identities and pinned analytic, matrix and quotient identities; the determinant calculation also uses the external Cauchy identity cited above.

Fix one original positive normalized probability p=probability(b,k0), the height k0 in J(b), and one initial phase vector theta with theta(2)=0. Index 4 denotes mode 13. The amplitude at residual h is sqrt(p(i))exp(-i(theta(i)+h(i))). Thus twice the real and imaginary parts of conjugate(psi(i))psi(j) are 2sqrt(p(i)p(j))(cos(delta(i,j)+h(i)-h(j)),sin(delta(i,j)+h(i)-h(j))), where delta(i,j)=theta(i)-theta(j). This positive phase difference follows from the original negative amplitude convention. Every edge magnitude is strictly positive, and the phase rotations and magnitudes depend only on the fixed preparation.

Use the oriented edge order (0,1),(0,2),(0,3),(1,13),(3,13). Put alpha=h(0)-h(1), beta=h(0), gamma=h(0)-h(3) as real lifts before reducing to the period-2pi circle. The exact real charge gives h(1)-h(13)=gamma-2pim and h(3)-h(13)=alpha-2pi*m. Their circle characters therefore agree with gamma and alpha, respectively. The character assignment in this edge order is (alpha,beta,gamma,gamma,alpha). Repeated edges have fixed, possibly different, initial-phase rotations and positive magnitudes; their readouts are the corresponding fixed linear transforms of the same character pair.

For q(t)=sqrt(2)*(cos(t),sin(t)), each generic decoder row is (a(e)/sqrt(2))R(delta(e)) acting on the assigned pair, and is zero on the other pairs. The complete generic coordinate is (q(alpha),q(beta),q(gamma)). On X+Y=1-Z, the real wall equation h(0)=h(13) gives gamma=-alpha modulo 2pi. On X=Y, h(1)=h(3) gives gamma=alpha even as a real lift. A single-wall coordinate is (q(alpha),q(beta)); on the first wall put J=diag(1,-1) before the initial-phase rotation on edges (0,3) and (1,13). On the second wall these two blocks use the identity. These are fixed linear decoders with zero affine offset.

At both walls the real equation is alpha=pim, so all four bottom-edge pairs equal their fixed initial vectors a(e)(cos(delta(e)),sin(delta(e))) multiplied by epsilon=(-1)^m. The middle pair is (a(0,2)/sqrt(2))*R(delta(0,2))*q(beta). Hence the all-winding coordinate is (q(beta),epsilon), with a fixed linear decoder and zero offset. Under the history restriction m=0, absorb the four fixed bottom pairs into one fixed offset and retain only the middle pair as the varying decoder block.

These are the actual reachable character domains. For any signed winding m, generic real targets alpha,beta,gamma are attained by h=(beta,beta-alpha,0,beta-gamma,beta-alpha-gamma+2pim). On the first single wall arbitrary alpha,beta are attained by h=(beta,beta-alpha,0,beta+alpha-2pim,beta); on the second they are attained by h=(beta,beta-alpha,0,beta-alpha,beta-2alpha+2pim). Each vector belongs to its original U(b) and has charge 2pim, so the all-sector realization supplies an original finite control with the fixed initial phases. Reduction gives the complete three-circle and two-circle domains. At both walls, h=(beta,beta-pim,0,beta-pi*m,beta) attains arbitrary beta in each sector. Its compact domain is a circle times parity, and m=0 attains the whole circle with parity one. The wall equations give the matching necessary restrictions.

For arbitrary original histories and arbitrary compatible prescribed later original loops, use OriginalControlComposition.concatenate_original. The second probability control is the same path shifted in time; its real phase control is translated by the terminal first phase minus its own initial phase. The theorem includes arbitrary finite durations, zero durations, both regularity alternatives and finite variation. Its scalar integral identity applied to every original weight component proves that the actual residuals add exactly and that the real windings add. Applying the transported phase lift to the joined control preserves compatibility at all times and agrees with the original first lift on its full prefix. The preparation and probability base are fixed throughout this operation contract.

The coordinate action is consequently R(uAlpha) directsum R(uBeta) directsum R(uGamma) in the generic case, R(uAlpha) directsum R(uBeta) on either single wall, and R(uBeta) directsum [(-1)^mU] at both walls. The cosine and sine addition identities give q(h+u)=T(u)q(h). Rotation addition and multiplication of signed integer parities give T(v+u)=T(v)T(u). Updating a fixed decoder means D[u]=DT(u), so D[u][v]=DT(u)T(v)=DT(u+v). The fixed offset is unchanged. On the chosen zero-winding double-wall histories and prescribed zero-winding loops, the update is just the middle rotation and Dzero[u]=Dzero*R(uBeta). A nonzero even winding is excluded from this chosen history class even though its endpoint parity is one.

For the positive family p=(a,b,8b,b,a), where a,b>0 and 2a+10b=1, the original base is (a+b,a+b,8b), J(b)=(0,a+b), and k0=a. Both a and k1=a/2 are strictly interior, and k1-k0=-a/2 is nonzero. For any signed integer m and real desired angle t, prepend the fixed-height signed circle with phase increment 2pim to the four-leg rectangle at heights a and a/2. Its relative phase height is A=(2*(a+b)(pim-t)-2pima)/(a/2-a). The rectangle residual is A(w(a/2)-w(a)); adding the circle residual 2pimw(a) gives exactly (t,t-pim,0,t-pim,t). Thus beta=t and the winding is m. The loop returns to the original probability base and carries the fixed compatible initial phase vector theta to theta+(t,t-pim,0,t-pi*m,t).

This representative has five unit-time affine legs, finite real phase variation and strict probabilities along every leg. The two heights lie in a compact positive subinterval, all coefficients are finite, and the probability returns to a. Its parameters depend only on the source, the desired angle and the signed winding. It is a prescribed loop independent of the input history. Every circle angle can use a real representative, so no closure or limiting-control argument is needed. The same explicit representatives supply every sector and angle in the paired comparison below.

The least affine decoding dimension is computed on the complete actual reachable domain, with the preparation fixed. For every natural k, let an encoder be any function from actual original histories, or from their reachable compact labels, into R^k. No measurability, continuity or linearity is required of this encoder. A competing decoder has one fixed offset c and one fixed linear map L, so y=c+L*encode. The direction of the affine span of its image is contained in the range of L and consequently has dimension at most k. This is exactly AffineMap.map_vectorSpan together with Submodule.finrank_map_le and Submodule.finrank_le. It applies even when different histories with the same endpoint receive different encodings.

The actual character representatives above give the full products of radius-sqrt(2) Euclidean circles in generic and single-wall position, the product of one such circle with {-1,1} at both walls, and one circle for actual zero-winding histories. Here Euclidean radius means the explicit identity q(t,0)^2+q(t,1)^2=2, not the default norm on a function type. Opposite circle points have differences spanning each coordinate axis: use angles 0 and pi for the first axis and pi/2 and -pi/2 for the second. Fixing all other factors gives every product coordinate direction. The parity difference 1-(-1)=2 supplies its independent direction. Hence the latent affine-span dimensions are 6,4,3 and 2, respectively.

Every actual decoder is injective on these latent spaces. In the generic case the three positive source edge blocks 01,02,03 separately recover the three pairs after undoing their fixed rotations and positive magnitudes. On either single wall the positive blocks 01,02 recover both pairs, including the reflection case. At both walls the positive middle block recovers the circle pair, and any positive bottom block recovers the parity scalar. Under zero winding only the middle block varies. The image affine-span dimensions are therefore exactly 6,4,3 and 2. The source factorizations attain these dimensions with one fixed affine decoder, so these are the least dimensions against all the competing encoders just quantified. The number of circle factors in the compact group, the affine decoding dimension, and a matrix kernel dimension are different quantities.

The Haar law uses response characters rather than the raw coordinates of the compact-group equivalences. Off the walls, change raw coordinates (a0,a1,a3) to (a0-a1,a0,a0-a3); its inverse is (beta,beta-alpha,beta-gamma). On either single wall change (a0,a1) to (a0-a1,a0), with inverse (beta,beta-alpha). At both walls the supplied raw circle coordinate is h1. Change (h1,e) to (h1+pie,e), where pie is the period-2*pi two-torsion homomorphism; the first coordinate is exactly beta=h0, and the inverse subtracts that two-torsion value. Each change is an explicit continuous additive equivalence of its actual compact group.

Normalized Haar uniqueness, applied through AddMonoidHom.measurePreserving to each of these continuous surjective homomorphisms, transports normalized Haar on K(b) to the corresponding product of normalized circle measures. At both walls it transports to normalized circle measure times half counting measure on ZMod 2. Thus the actual beta and parity labels are independent, and each parity component has mass one half. Each wall uses its own actual group equivalence; the three-circle formula is not continued across a wall. The endpoint law is an ideal averaging convention and specifies no law for sampling laboratory controls.

For a period-2pi circle write r=Re(fourier 1) and s=Im(fourier 1). The original FourierModeDetermination period-2pi Haar integral suppliers give integral r=integral s=0, integral rr=integral ss=1/2, and integral r*s=0. Their real-lift values are cos(t) and sin(t). Multiplication by sqrt(2) gives zero-mean quadratures with second-moment matrix I2. Distinct product coordinates have zero cross moments. For parity epsilon=1 on label zero and -1 on label one, half counting measure gives mean zero and second moment one; its cross moments with both circle coordinates vanish by product integration. The preceding actual group maps transport these exact integrals to K(b).

Flatten the five oriented real-imaginary pairs in the fixed edge order into ten real coordinates, without changing their Euclidean geometry. Matrix entries are the actual fixed decoder applied to standard coordinate vectors. If q has the just-derived zero means and identity second moments, expanding each coordinate y_i=c_i+sum_j D_ijq_j and integrating the finite sums gives mean(y_i)=c_i and C_out(i,l)=sum_j D_ijD_lj. Thus the actual centered ten-output covariance is DD transpose, whereas the latent pullback Gram is D transposeD. Repeated-edge cross blocks in the former are retained. All bilinear and squared-length expressions here are explicit finite sums of coordinate products.

For generic position the pullback Gram is diag(lambdaAlpha I2,lambdaBeta I2,lambdaGamma I2), where lambdaAlpha=2*(p0p1+p3p13), lambdaBeta=2p0p2 and lambdaGamma=2*(p0p3+p1p13). On either single wall it is diag(lambdaBottom I2,lambdaBeta I2), where lambdaBottom=2*(p0+p13)(p1+p3). The sign reflection has square one and preserves the explicit pair inner product, so both single walls have this same coefficient formula. At both walls the pullback Gram is diag(lambdaBeta,lambdaBeta,lambdaParity), where lambdaParity=4(p0p1+p0p3+p1p13+p3p13). The parity coordinate is a scalar of square one; it is not another normalized circle pair.

These formulas follow by summing the actual edge contributions a(e)^2/2=2p_ip_j on circle blocks and a(e)^2=4p_ip_j on the scalar parity block. Every displayed coefficient is strictly positive for every original positive source. The full characteristic-root multisets of the actual covariance are four zeros plus two copies of each generic coefficient, six zeros plus two copies of each single-wall coefficient, and seven zeros plus two copies of lambdaBeta and one copy of lambdaParity at both walls. Equal coefficient values retain and add all their copies. Matrix.charpoly_mul_comm_of_le and the diagonal characteristic polynomial give these algebraic multiplicities; the existing GramNonzeroSpectrumMultiplicity result supplies the general nonzero-spectrum correspondence. No simplicity or absence-of-collision hypothesis is used.

The ten-output covariance ranks are consequently 6,4 and 3. More directly, the positive diagonal pullback Grams and Matrix.rank_self_mul_transpose give these ranks, and rank-nullity gives output nullities 4,6 and 7. Matrix.ker_mulVecLin_transpose_mul_self identifies the kernel of D*D transpose with the kernel of D transpose. These are exactly the linear relations among output coordinates. They are distinct from the latent decoder kernel, which is zero by injectivity.

For the actual m=0 double-wall task, take uniform beta on the circle and the endpoint label obtained by the inverse actual double-wall equivalence at (beta,0). The exact sector realization supplies an original zero-winding history for every one of these labels. The source bottom parity is deterministically one, so its four bottom pairs form the fixed offset c=D(0,1). The mean is exactly c. Centering leaves only the original middle decoder Dzero, with pullback Gram lambdaBeta I2 and actual covariance Dzero*Dzero transpose. Its rank is 2, nullity is 8, and root multiset is eight zeros plus two copies of lambdaBeta. This chosen history domain still requires winding exactly zero; a nonzero even-winding history is not admitted by its endpoint parity.

For the explicit anisotropic source of Corollary 5.2 take p=(1,2,3,4,5)/15 in the original order (0,1,2,3,13), b=(X,Y,Z)=(7/15,9/15,3/15), and kappa=5/15. The actual probability decoder gives probability(b,kappa)=p. Its strict source conditions are 0<Z<1, 0<X,Y<1-Z, and lower(b)=4/15<kappa=5/15<7/15=upper(b). The two wall tests are p0=p13 iff X+Y=1-Z and p1=p3 iff X=Y; here neither equality holds. This is the original positive fiber source and its actual decoder, with the fixed preparation, negative phase convention, and all admissible controls retained.

Substitution in the actual generic Gram coefficients gives lambdaAlpha=2((1/15)(2/15)+(4/15)(5/15))=44/225, lambdaBeta=2(1/15)(3/15)=6/225, and lambdaGamma=2((1/15)(4/15)+(2/15)(5/15))=28/225. They are pairwise distinct and positive. The existing actual generic output matrix has characteristic-root multiset four zeros together with two copies of each of these three coefficients for every fixed allowed initial phase. The frozen nonzero-spectrum bridge transfers the same positive roots and algebraic multiplicities between the actual ten-output covariance and its pullback Gram.

The obstruction uses the stated comparator class itself. For every real positive-semidefinite 2-by-2 matrix A and every real 6-by-6 orthogonal Q, the reindexed matrix Q*(A tensor I3)*Q transpose has characteristic polynomial whose every root multiplicity is divisible by three; this follows from the pinned Kronecker characteristic-polynomial identity and invariance under the orthogonal conjugation. The actual diagonal Gram with entries (44/225,44/225,6/225,6/225,28/225,28/225) has multiplicity two at 44/225, so it cannot be orthogonally equivalent to any such comparator. This argument uses the actual source coefficients and positive multiplicities, rather than a dimension count. If arbitrary finite zero blocks are appended, the pinned zero-padding identity preserves every nonzero root multiplicity, including all collisions; the four actual output null directions therefore cannot repair this obstruction. No physical spatial metric or native SO(3) action is inferred.

The complete positive-spectrum classification now applies to every original positive normalized five-mode source. The actual wall equations are p0=p13 iff X+Y=1-Z and p1=p3 iff X=Y, so they identify the source regimes before the appropriate actual matrix is selected. Off both walls the active Gram is diag(lambdaAlpha I2,lambdaBeta I2,lambdaGamma I2). Its positive multiplicity patterns are (2,2,2), (4,2), or, if all three coefficients coincide, (6). The exact identity lambdaAlpha-lambdaGamma=2*(p0-p13)*(p1-p3) rules out the all-equal case in the generic regime. Thus every generic collision pattern still contains a positive multiplicity 2 or 4 and fails divisibility by three.

On exactly one wall the actual wall matrix has two positive 2-by-2 blocks, with coefficients lambdaBottom and lambdaMiddle=2p0p2. Collisions can only change the positive pattern from (2,2) to (4), and neither pattern is divisible by three. The reflected wall uses the same Gram formula because its actual reflection preserves the edge inner products; the generic three-block formula is not continued through the wall.

At both walls the actual active Gram is three-dimensional, with the circle coefficient 2p0p2 occurring twice and the parity coefficient 4*(p0p1+p0p3+p1p13+p3p13) occurring once. Put p0=p13=a and p1=p3=b. Positivity gives a,b>0. The positive multiplicities are divisible by three exactly when the two coefficients are equal, and the equality is exactly 2ap2=16ab, hence p2=8b. Normalization then gives 2a+10b=1. Conversely, every a,b>0 satisfying this normalization produces the original source p=(a,b,8b,b,a), base (a+b,a+b,8b), strict fiber height a, both wall equalities, and both coefficients 16a*b. These statements include both directions and all positivity and normalization obligations.

The same positive-multiplicity equivalence holds for the actual ten-output covariance by the D transpose D versus D D transpose algebraic spectrum theorem; only the zero multiplicity changes by the actual output nullities four, six, or seven. On the locus the active Gram is exactly 16ab I3, hence [16ab] tensor I3 after the canonical product-index reindexing. For the padded six-coordinate display, use the concrete isometric embedding E(v)=(v,0) with E(i)=Fin.castAdd 3 i on the first block: E transpose E=I3 and E*(16ab I3)E transpose=diag(16ab I3,0)=diag(16a*b,0) tensor I3. This is a three-dimensional source support with a zero-padded representation, never a six-dimensional source. Arbitrary finite zero padding preserves every nonzero multiplicity, including collisions.

For Proposition 6.2 retain an actual positive normalized source p=probability(b,k0), with the original base, strict height and fixed allowed preparation. Require both non-wall conditions X+Y differs from 1-Z and X differs from Y. Its actual active six-dimensional Gram is the generic decoder transpose times that decoder. Flatten Fin 3 times Fin 2 to Fin 6 by finProdFinEquiv; the actual Gram is diag(lambdaAlpha,lambdaAlpha,lambdaBeta,lambdaBeta,lambdaGamma,lambdaGamma). The U2 decoder calculation holds for every fixed initial phase vector, so this Gram and the distance below are independent of the fixed allowed preparation. Conversely, every positive five-vector of total one reconstructs the original source with base (p1+p13,p3+p13,p2) and height p13 strictly between the original endpoints. The two source non-wall tests are exactly p0 differs from p13 and p1 differs from p3.

Use the single Frobenius geometry throughout: Fsq(M)=sum_i sum_j M(i,j)^2 and F(M)=sqrt(Fsq(M)). For every real matrix this squared sum equals RHLinalg.frobSq(M)=trace(M transposeM), and F(M)^2=Fsq(M). These explicit sums do not use Matrix’s default norm. Define the comparison set to contain every Q(A tensor I3)Q transpose, where A is an arbitrary real symmetric positive-semidefinite 2-by-2 matrix and Q is any real 6-by-6 matrix satisfying Q transposeQ=Q*Q transpose=I. Here flatten Fin 2 times Fin 3 to Fin 6 by finProdFinEquiv before the conjugation; this indexing differs from the source’s pair indexing.

Every matrix in this complete comparison set is real Hermitian: the Kronecker entries inherit the symmetry of A, and orthogonal conjugation preserves it. The pinned Kronecker determinant identity gives its characteristic polynomial as charpoly(A)^3. The real Hermitian spectral theorem and positive-semidefinite eigenvalue theorem give two nonnegative real values; put them in order a<=b. The full comparator characteristic polynomial is (X-a)^3*(X-b)^3. Apply Matrix.IsHermitian.sort_roots_charpoly_eq_eigenvalues₀ to its entire root multiset, and use the antitone list (b,b,b,a,a,a), to obtain equality with the actual ordered Hermitian eigenvalue function. Thus the increasing order is (a,a,a,b,b,b). This step includes a=0, a=b and a=b=0: repeated or zero roots keep every copy, and no simple-spectrum hypothesis is imposed. Characteristic multiplicities alone are not being used as ordered eigenvalue equality.

Let sigma be any permutation of the three actual block labels that puts their values in order x<=y<=z; Tuple.sort supplies one for every source, including every collision. Extend sigma to pairs by (j,c) mapped to (sigma(j),c), and flatten it to a permutation of Fin 6. Let P be its real permutation matrix, whose rows select the original coordinates in this sorted order. The exact alignment is PGP transpose=diag(x,x,y,y,z,z), with P transposeP=PP transpose=I. Applying the same Hermitian root-sorting identity gives the actual decreasing eigenvalue list (z,z,y,y,x,x). The public real RCLike-generic RHLinalg.vonNeumann_trace_ineq, together with the two squared spectral trace identities, gives sum_i (lambda_i(G)-lambda_i(M))^2<=Fsq(G-M) for every comparator M. No private complex overlap proof or complex-to-real spectrum identification is required.

For that comparator’s ordered values a<=b the spectral lower bound is 2*(x-a)^2+(y-a)^2+(y-b)^2+2*(z-b)^2. Put mu=(2x+y)/3 and nu=(y+2z)/3. Completing squares makes this exactly (2/3)((y-x)^2+(z-y)^2)+3(a-mu)^2+3*(b-nu)^2. Positivity of the actual block values and x<=y<=z give 0<=mu<=nu. The concrete real matrix A=diag(mu,nu) is positive semidefinite, and its reindexed A tensor I3 is diag(mu,mu,mu,nu,nu,nu). Take the actual orthogonal matrix Q=P transpose. Its conjugate belongs to the full comparison class, and the Frobenius residual is precisely 2*(x-mu)^2+(y-mu)^2+(y-nu)^2+2*(z-nu)^2=(2/3)*((y-x)^2+(z-y)^2). Thus the optimal groups are [x,x,y] and [y,z,z], with the two copies of y split between them. This constructs an attaining matrix in the original coordinates, as well as its spectral values.

The set of distances F(G-M) over all actual comparators is nonempty because the displayed A and Q belong to it. It is bounded below by zero because F is a nonnegative square root. The pointwise spectral lower bound and the displayed attaining comparator prove that sqrt((2/3)((y-x)^2+(z-y)^2)) is its least element. Hence its real infimum distF is attained and distF^2=(2/3)((y-x)^2+(z-y)^2). No compactness of the unbounded comparator class, unattained limiting argument or substitution of a spectral surrogate for the matrix class is needed.

For the same actual source, lambdaAlpha-lambdaGamma=2*(p0-p13)(p1-p3) by expansion of its source coefficients. Every sorting permutation puts both lambdaAlpha and lambdaGamma in [x,z], including all coincidences; consequently their squared difference is at most (z-x)^2. The adjacent-gap identity gives (y-x)^2+(z-y)^2>=(z-x)^2/2. Combining these two inequalities with the attained distance formula yields distF^2>=(4/3)((p0-p13)*(p1-p3))^2. The nonnegative distance, absolute source product, positive sqrt(3) and sqrt(3)^2=3 then give the unsquared bound distF>=2/sqrt(3)abs((p0-p13)(p1-p3)). The source conditions and every fixed preparation remain in scope; no wall formula is inferred from this generic six-dimensional comparison.

Sharpness uses the actual source p*=(2,3,3,1,1)/10, in the original order (0,1,2,3,13). Its base is (2/5,1/5,3/10), r=7/10 and height kappa=1/10. The actual probability formula reconstructs p*, all five weights are strictly positive and their sum is one; the original fiber endpoints are lower=0 and upper=1/5. Both non-wall conditions hold. Its actual coefficients are (lambdaAlpha,lambdaBeta,lambdaGamma)=(7/50,3/25,1/10). Swapping the alpha and gamma block labels gives (x,y,z)=(1/10,3/25,7/50), with both adjacent gaps 1/50. The source product (p0-p13)(p1-p3)=1/50. For every fixed allowed preparation the attained squared distance is 1/1875, and both sides of the unsquared source bound equal 1/(25sqrt(3)). This is an original positive generic source witness with its actual fiber, rather than a freely specified spectral triple.

This application establishes Proposition 6.2 on the actual generic latent support. It uses the public real trace suppliers, pinned Hermitian spectral sorting, finite permutations, Kronecker identities and scalar least squares; it claims no new spectral approximation theorem or mathematical priority. The comparison does not assert that an optimizing comparator is another realizable source, extend the distance formula to padded walls, or assign a physical laboratory error. The static representation and support/law analysis below use a different comparison; common-history cross moments and every actual native-loop optimizer remain separate obligations.

For Section 6.3 use the actual source pIso=(1,1,8,1,1)/12, base (1/6,1/6,2/3), r=1/3 and kappa=1/12. Its strict fiber is (0,1/6), and both wall equations hold. The source is the locus point a=b=1/12. Substituting in the original three-column decoder, with every fixed allowed initial phase retained, gives D transposeD=I3/9. The four bottom pairs still multiply the signed winding parity, while the middle pair carries sqrt(2)(cos(beta),sin(beta)); the all-winding affine offset is zero. The zero-winding task with a constant bottom offset is a different restriction.

The static construction works for every positive locus source p=(a,b,8b,b,a), a,b>0, 2a+10b=1, with lambda=16ab. For its original ten-by-three decoder define W(Q)=I10+lambda^(-1)D(Q-I3)D transpose. Multiplying the Gram identity by lambda^(-1) gives the left inverse lambda^(-1)D transpose, hence D is injective. For every output v put u=lambda^(-1)D transposev and z=v-Du. Then D transposez=0. The finite dot-product identity says this kernel is exactly the Euclidean orthogonal complement of range(D). Thus every output decomposes as Du+z in the original ten real coordinates.

The same single formula gives W(Q)(Du)=D*(Qu) and W(Q)z=z whenever D transposez=0. Injectivity gives uniqueness of u on range(D), so the prescribed image action is well-defined; matrix multiplication proves its linearity on the whole output space. Expanding with D transposeD=lambdaI3 gives W(I3)=I10 and W(QR)=W(Q)W(R) for every Q,R. Transposition gives W(Q) transpose=W(Q transpose). Therefore Q transposeQ=I3 implies W(Q) transpose*W(Q)=I10, and the exact intertwining is W(Q)D=DQ. In particular this is one full orthogonal representation of SO(3), acting as identity on the orthogonal complement. The equality of Euclidean squared lengths is the explicit sum over all ten squared output coordinates.

Give the actual compact endpoint group its normalized Haar law as above. Its actual double-wall coordinate homeomorphism sends this law to uniform angle times the balanced counting measure on ZMod(2); the parity is independent of the angle. In these coordinates define q(beta,e)=(sqrt(2)*cos(beta),sqrt(2)sin(beta),epsilon(e)), with epsilon(0)=1 and epsilon(1)=-1. This is exactly the original circle/parity coordinate, not a new surrogate distribution. Its range is S={v:v0^2+v1^2=2, v2^2=1}. For the reverse inclusion, the unit complex number (v0+iv1)/sqrt(2) has an argument beta with the required cosine and sine, and v2^2=1 supplies one of the two actual parities.

The map q is continuous on the compact angle-times-parity group. Haar measure is positive on every nonempty open set, and each parity has positive mass. Consequently the support of q-pushforward Haar is exactly range(q)=S: the compact range is closed and conull, and the preimage of every open neighborhood of an image point is nonempty open and has positive measure. This argument proves the full support on every positive locus source. For any latent linear Q, the same pushforward argument gives support(Q-pushforward nu)=Q*S. For orthogonal Q, its transpose is the continuous inverse, so this is also the usual support transport by the actual homeomorphism. Equality of the complete measures therefore implies equality of their supports.

The support stabilizer is derived without presupposing a block form. Write the third row of a proper orthogonal Q as (x,y,z). Support preservation says that the third coordinate squared is one on every actual endpoint. Apply it to (sqrt(2),0,1),(-sqrt(2),0,1),(0,sqrt(2),1),(0,-sqrt(2),1),(1,1,1), which all belong to S. Together with x^2+y^2+z^2=1 these equations give xz=yz=x*y=0 and x^2=y^2, hence x=y=0 and z=+1 or -1. Orthogonality then makes the first two entries in the third column zero. The upper two-by-two block A is orthogonal, and det(Q)=1 forces z=det(A). This proves the necessary form A directsum det(A) from the support itself.

Conversely every A in O(2) is a planar rotation or a planar rotation followed by diag(1,-1). The pinned two-dimensional special-orthogonal classification and the argument of its unit first column give an angle theta; the determinant is respectively +1 or -1. Its action on the actual source parameters is (beta,e) mapped to (theta+beta,e) in the first case and (theta-beta,e+1) in the second. Haar translation and inversion on the circle, and translation of balanced parity, preserve the whole product measure. Mapping this exact measure identity through q proves full endpoint-law invariance and preserves independence, with no inference from moments. Thus, inside latent SO(3), the proper law stabilizer, proper support stabilizer and {A directsum det(A):A in O(2)} are exactly equal. Every displayed block is itself a proper orthogonal matrix.

All these law and support conclusions transfer through the same original affine decoder v mapped to c+Dv. Its continuous affine left inverse is y mapped to lambda^(-1)D transpose(y-c). Therefore equality of decoded pushforward laws is equivalent to equality of the latent laws. The decoded support is exactly c+DS, and the comparison target support is c+D*(QS). Injectivity likewise makes equality of these supports equivalent to QS=S. For the original all-winding ten-output menu take its existing c=0. The actual compact endpoint readout equals D*q under its original coordinate homeomorphism; exact reachability identifies this endpoint range with outputs of the original finite lawful histories. These statements apply to every positive locus source and every fixed allowed preparation.

For the mixing counterexample take Qx(pi/2)=[[1,0,0],[0,0,-1],[0,1,0]], whose transpose product is I3 and determinant is one. The actual q0=(0,sqrt(2),1) is q(pi/2,0). The original finite circle-and-rectangle construction with winding zero, height a/2 and target angle pi/2 realizes it from every fixed allowed initial phase. At the isotropic source this keeps the original base and kappa. The image is (0,-1,sqrt(2)), outside S since its third coordinate squared is two. By injectivity c+DQxq0 lies outside c+D*S.

The mixing law comparison uses a measurable event with positive mass. The closed set S has nu(S complement)=0. The preimage of S complement under Qx composed with q is open and contains (pi/2,0), so its actual product-Haar measure is strictly positive. Hence (Qx-pushforward nu)(S complement)>0 and the complete endpoint laws differ. On the output space use the complement of the compact decoded support c+D*S: its original probability is zero, whereas its Qx target probability is strictly positive by the same open-preimage argument and decoded injectivity. The conclusion does not rely on the probability of one exceptional point.

Every native loop, with its one residual increment u fixed independently of the input history and its actual integer winding m, acts by R(uBeta) directsum [(-1)^m]. The existing original-control endpoint theorem and concatenation law give precisely this matrix for both allowed regularity classes and every integer winding. Its parameter action is angle translation and parity translation, so it preserves the same full endpoint law and support; the original affine decoder preserves the resulting equality of complete ten-output laws. Qx has a nonzero mixing entry in row three, column two, whereas every such native matrix has zero there. It therefore cannot be the original native loop operation. Static equivariance, scalar Gram isotropy, support/law invariance and native controllability are distinct statements.

The explicit proper target QStar=diag(1,-1,-1) acts by (beta,epsilon) mapped to (-beta,-epsilon), or (beta,e) mapped to (-beta,e+1). This preserves the entire product-Haar law, S and their original decoded laws and supports. Its planar determinant is -1, while every native planar rotation has determinant +1, so it differs from every lawful loop action. More generally A directsum det(A) in the proper support stabilizer is native exactly when det(A)=1. To see the same-history distinction directly, equality with a fixed native action on all q(beta,e) at beta=0 and beta=pi/2 would force both cos(theta)=1 and cos(theta)=-1. Thus some actual common-history endpoint gives different latent and, by decoder injectivity, different ten-output paired responses, even though the single-endpoint laws agree. The set of common endpoints with different decoded responses is open. Its preimage under q contains such a witness and has strictly positive product-Haar measure. The actual compact-group Haar bridge gives the same positive-measure distinction for the original endpoint history, with the one native loop fixed for every input.

These are applications of the existing original-control, decoder and Haar bridges and pinned matrix algebra. The support calculation uses Measure.support_subset_of_isClosed, Measure.support_eq_forall_isOpen, Measure.map_apply and positive measure of nonempty open sets. The angle construction uses Complex.norm_mul_cos_arg and Complex.norm_mul_sin_arg; the planar classification uses Matrix.mem_specialOrthogonalGroup_fin_two_iff. Full law preservation uses measurePreserving_add_left, Measure.measurePreserving_neg, MeasurePreserving.prod and Measure.map_map. They establish the complete conditional static representation and the support/law structure in Section 6.3 and Corollary 7.4 on the positive locus, without a new probability preparation or a physical interpretation. The symmetry classification concerns latent SO(3) and its induced decoder-image action; it does not classify all ambient O(10) symmetries. The paired comparison below uses this same law and the actual native loop image. The conditional mathematical model is evaluated under its stated assumptions; no premise-free physical derivation is imposed.

For the paired comparison keep every positive source p=(a,b,8b,b,a), a,b>0 and 2a+10b=1, its original base X=Y=a+b, Z=8b, r=2*(a+b), kappa0=a, fixed preparation and fixed initial phases. Put lambda=16ab>0 and retain the original ten-output decoder y(h)=c+Dq(h), D transposeD=lambdaI3. The residual endpoint h has the same normalized Haar law already derived: uniform circle angle and independent balanced parity, with mean(q)=0 and E[qq transpose]=I3. This specifies no uniform law on integer winding numbers or loop paths. The loop u is prescribed once, independently of h, and its original residual increment acts on that same h by q(h+u)=T(u)*q(h). The actual operation is T(u)=R(theta) directsum [(-1)^m] for its signed integer winding m. Odd windings are included even though their three-dimensional native matrix has determinant -1; the comparison target Q belongs to SO(3).

Use centered responses Yu(h)=y(h+u)-c and Y(h)=y(h)-c. Expanding the original coordinate sums and integrating their mixed second moments gives the ordered matrix Cu=E[Yu(h)Y(h) transpose]=DT(u)D transpose. The order fixes T rather than its transpose. Multiplying by D transpose on the left and D on the right gives D transposeCuD=lambda^2T(u), hence T(u)=lambda^(-2)D transposeCu*D. The same formula for CQ gives Cu=CQ if and only if T(u)=Q. The recovered object is the action. Angles differing by a full period and windings differing by two can have the same action; neither the entire path nor the integer winding is recovered.

The error is the expectation of the explicit sum over all ten original coordinates of (y(h+u)_i-yQ(h)_i)^2, with yQ(h)=c+DQq(h). Finite-sum integration and the actual second moment give E(u,Q)=trace(D*(T-Q)(T-Q) transposeD transpose)=lambdasum_ij(T_ij-Q_ij)^2. Orthogonality of T and Q, including native determinant -1, gives E(u,Q)=lambda(6-2trace(T transposeQ)). The offset cancels. These are Euclidean output and Frobenius matrix sums, not the default function-space supremum norm, and no whitening changes the source metric.

For genuinely independent h and hPrime use the product of the same two endpoint Haar measures, with u still fixed. Product integration factors each cross term into two zero means, so E[Yu(hPrime)Y(h) transpose]=0. The squared-error cross term vanishes, while each of the two original output second moments contributes 3lambda; the error against any Q in SO(3) is 6*lambda. Equal endpoint marginal laws alone do not imply this product-law conclusion. The common-history and independent-preparation comparisons use different specified joint laws, with no replacement coupling, adaptive feedback or physical sampling assertion.

For Q in SO(3) set z=Q33, x=Q11+Q22 and v=Q21-Q12. Orthogonality gives -1<=z<=1. The determinant-one cofactor identity Q11Q22-Q12Q21=z, together with the row and column unit-square identities, gives x^2+v^2=(1+z)^2. For sigma=(-1)^m the trace is xcos(theta)+vsin(theta)+sigmaz. The planar term is at most 1+z. If z>-1, equality holds exactly when cos(theta)=x/(1+z) and sin(theta)=v/(1+z); their squares sum to one, so such an angle exists and is unique modulo 2pi. If z=-1 then x=v=0 and every angle attains the planar maximum. These are both necessary and sufficient equality conditions.

It follows that every prescribed signed integer sector m has attained minimum 4lambda(1-z) when m is even and 4lambda when m is odd, always averaging over the same balanced input parity. Over all actual loops the attained infimum is 4lambda*(1-max(z,0)). A loop minimizes globally exactly when its angle satisfies the preceding equality condition and its winding is even for z>0, odd for z<0, or of either parity for z=0. At z=-1 the even and odd sector minima are 8lambda and 4lambda and every angle is sector-minimizing. At z=0 both sector minima are 4lambda with the unique angle just described. At z=1 the sector minima are zero and 4lambda. Zero best error holds exactly for Q=R(theta) directsum [1], the proper native targets.

Attainment uses the original finite controls, with no density argument. Given any signed integer m and any real angle representative theta, take a constant-height winding-m circle at kappa=a on the first unit interval, followed by the original four-leg relative zero-winding rectangle at the terminal phase lift. The rectangle has fixed interior height kappa1=a/2 and signed phase height alpha=(r*(pim-theta)-2pima)/(a/2-a). Its denominator is -a/2, hence nonzero. Its vertices in height and relative control phase are (a,0), (a/2,0), (a/2,alpha), (a,alpha), (a,0). This is the actual polygon used by the finite-rectangle construction, rather than an arbitrary existential endpoint representative.

The circle has signed area 2pima. The rectangle has signed area alpha(a/2-a), so the concatenated area is exactly r*(pim-theta). The original transport identity then gives endpoint beta=theta and total winding m. On each horizontal or vertical affine leg the height lies in the closed interval [a/2,a]; the circle stays at a and phase translation in concatenation leaves this height unchanged. Since a,b>0, the whole interval lies strictly inside the original fiber (0,a+b). Thus the same constructed path has full support throughout, not merely some path with the same endpoint. The five finite affine legs have finite real phase variation and satisfy the original continuous finite-piecewise-C1 alternative; the comparison class continues to include its full AC alternative as well. The probability returns to a, the lifted control phase changes by exactly 2pim, and the original phase lift is compatible at every time and ends at the initial phase plus the stated residual. Only probability/base and control phase modulo 2pi are required to close; the state need not return to its initial phase.

All construction parameters depend only on the source, m, theta and fixed preparation, never the incoming h. The existing original-control concatenation theorem adds the same residual to each actual incoming history, while the actual compact-group readout identifies it with D*q(h+u). Choosing every angle allowed by the equality conditions above therefore realizes every sector-minimizing native action in every prescribed signed sector, and every global minimizing action when its parity is selected. This proves an actual least element of each original loop-error set and of their union, not just a matrix extremum or an unattained infimum.

Apply the exact proper support and full-law stabilizer {A directsum det(A):A in O(2)} already obtained from the same endpoint law. Its det(A)=1 elements are proper native actions with attained zero error. Its det(A)=-1 elements have Q33=-1 and attained best error 4lambda. In particular QStar=diag(1,-1,-1) preserves the complete single-endpoint law shared by every lawful loop, yet Cu differs from CQStar for every loop: equality would recover the impossible native action QStar. Its least paired error is the strictly positive 4lambda. This concerns latent SO(3) and the induced original decoder-image action, without classifying all ambient O(10) symmetries.

At the actual isotropic source a=b=1/12, lambda=1/9 and the original metric gives the attained best error (4/9)*(1-max(Q33,0)), QStar error 4/9 and genuinely independent-preparation error 2/3. The same finite circle-and-rectangle witnesses attain all stated minima, including all boundary targets and every signed sector. The derivation reuses the original reachability, transport, concatenation, decoder and Haar results, finite integration identities, matrix adjugate/cofactor identities, and the circle cosine-sine parameterization. It is a conditional mathematical result under the declared source, operation and joint-law hypotheses; it makes no claim that metric isotropy, static equivariance or endpoint-law symmetry supplies an additional native control operation.

The affine-span, Haar transport, finite-moment, decoder-matrix and rank calculations above are applications of the original source reachability and operation results, the period-2*pi Fourier integrals, and pinned affine, Haar, integration and matrix identities. They retain the original positive normalized source, fixed height and preparation, negative amplitude phase convention, five oriented readouts and all signed winding sectors. These conclusions establish the response capacity, Theorem 5.1 averaging calculation, Corollary 5.2 anisotropic obstruction, Theorem 6.1 positive-spectrum locus, and Proposition 6.2 attained matrix distance and sharp source lower bound. The static support/law analysis in this exposition preserves these same source and control contracts. The paired comparison retains the same original source, law and operation contracts.

These operator, tensor-spectrum and observation conclusions are applications of the original transport and synthesis results, the connected-graph kernel theorem, and the pinned matrix exponential, Kronecker, unitary, characteristic-polynomial and Hermitian-spectrum identities. The finite source correspondence and witness arithmetic introduce no alternative probability law or assumed history class. The quantitative applications above retain their respective sampled and whole-path hypotheses and use the external Cauchy identity for the four-height determinant.

References

• Truth anchor: D5/S3/Quantum/Fibers/FiniteRectangleTransport.finite_rectangles_realize
• Truth anchor: D5/S3/Quantum/Fibers/FiniteRectangleTransport.weight_compatible
• Dependency: D5/S3/Quantum/Fibers/InteriorProbabilityPhaseFiber