Normalized coordinates of observable trajectories
Abstract
Normalized coordinates of observable trajectories
Theorem 1.1 (Trajectory-image coordinates and the integrated Gramian).
Proof. Machine-checked in Lean as D5/S3/Observer/Linear/ObservableTrajectoryCoordinates.observable_trajectory_coordinates (✓ std3). ∎
Source. Repository-derived.
Commentary.
Let d and p be any nonnegative integers, E and W the real Euclidean spaces of those dimensions, B:E→E and C:E→W continuous linear maps. Assume that C B^k x=0 for every k
There exists a bounded linear map F:E→H whose representatives equal C exp(t B)x almost everywhere for every x. It is injective and its range has dimension d. There exist an orthonormal basis b indexed by Fin d of that actual range, a bounded linear map U:H→E, and a real d by d matrix M. Write P for the actual orthogonal projection onto the range of F. U is the basis-coordinate isometry composed with the projection onto that range, and M represents U F in the standard Euclidean state coordinates.
For every L² class g and every i<d, the scalar function inner(b(i)(t),g(t)) is interval integrable on [0,T], and U(g)(i) equals its integral. Every representative is allowed; no continuity is imposed on g or the representatives of the basis. U contracts the norm and UU=P. Also (UF)(UF)=F*F. The display gives the representative and exact Gramian identities; the integral is the actual Bochner interval integral.
Here A and D denote the matrices of the given operators B and C, respectively, in the standard Euclidean bases. The matrix identity concerns the actual continuous exponential trajectory Gramian. Empty state or output index sets are permitted; in dimension zero the image basis and coordinate index set are empty.
Continuous trajectories belong to L² on the finite interval. If a trajectory is zero in L², continuity makes it zero on the interval. Analytic continuation and exponential-series coefficient uniqueness make every C B^k x zero, and finite observability makes x zero. An orthonormal basis of the image then provides the coordinate map. Orthogonal projection and the L² inner-product integral give its contraction and coefficient identities; preservation of trajectory inner products and exchange of a finite-dimensional continuous linear map with the integral give the exact Gramian.
The stronger observable_trajectory_coordinates_all_bases API quantifies over every orthonormal basis of the constructed trajectory image before producing U and M. It supplies all the displayed contraction, coefficient-integrability, projection and exact Gramian identities for that chosen basis. The original existential theorem selects one such basis from the image dimension and projects these facts. Any other bounded linear map with the same almost-everywhere exponential representatives equals this map in L2, so the all-bases assertion transports to its actual image as well. Neither the trajectory nor the chosen basis is replaced by a square root of a Gramian.
In the original derivative-layer noise experiment use the original state dimension d, the same positive time T, the actual trajectory F_T, and any chosen orthonormal image basis at each T. Set M_T to the standard-coordinate matrix of U_T F_T. Then M_T transpose M_T is precisely the integrated exponential Gramian G(T). There is no continuity or measurability requirement on the choice of basis as T varies. With beta>0 and variance v(T)>0, substitute M=M_T and tau=1/v(T) in GaussianObservationLaw. The all-measurable-estimator and noise-asymptotic conclusions for this same experiment are explained in SpectralNoiseAsymptotics; the present map-level theorem also retains empty state and output dimensions.
Same-delivery information-escape audits for the newly exposed API theorems remain unfinished; see https://github.com/the-omega-institute/trureturing/issues/20111. Existing audit sources are preserved. Neither compilation of candidate registrations nor this issue is declared_validated evidence.
For the finite observation experiment take d,p>=1. Any externally supplied bounded linear F with the displayed almost-everywhere trajectory representatives equals the F constructed above: equality of those representatives gives equality of their L2 classes for every state. Fix any orthonormal basis b of this same range. Its coordinate map is U=b.repr composed with orthogonal projection, and its matrix M represents UF. Since the projection is the identity on the trajectory range and b.repr is an isometry, (UF)UF=FF for this chosen basis as well. Thus M transpose M is the same integrated Gramian G(T), and each coordinate is the stated integral against that basis. The construction does not require replacing the supplied trajectory or its basis.
For finite polynomial moments, fix m>=0 and polynomials ell_0,…,ell_m orthonormal on [0,1], of degrees at most m. Index the q=(m+1)p scalar coordinates by pairs (k,r), and define row (k,r), column j of M to be T to the power -1/2 times the integral from 0 to T of ell_k(t/T) times the r coordinate of C exp(tB)e_j. These continuous integrands are integrable; moving evaluation through the finite-dimensional integral and expanding x in the standard basis gives (Mx)_(k,r)=T to the power -1/2 times the integral of ell_k(t/T)(C exp(tB)x)_r. Hence this is the actual normalized moment map, with Gramian G_mom=M transpose M. Use q independent standard Gaussian noise coordinates, independent of X, and data Y=MX+sigma xi. Applying gaussian_observation_law with this rectangular M gives posterior covariance (beta I+sigma to the power -2 times G_mom) inverse and mean sigma to the power -2 times that covariance times M transpose Y. Its information, all-measurable-estimator Bayes energy risk, centered free energy and known skew-flow future risk follow by the same joint-law and risk arguments in the Gaussian observation narrative. The moment formulas use G_mom; the trajectory-basis formulas use G(T). Neither matrix needs a rank hypothesis for the Gaussian calculation because beta>0 keeps the precision positive definite.
An already tapped nilpotent source gives a separate exact application of polynomial interpolation and integration. Fix d,p,nu>=1, real B and C of sizes d by d and p by d, B^nu=0, and T>0. Put E(t)=sum_(j<nu) t^j B^j/j!. The exponential-series identity NormedSpace.exp_eq_tsum, finite-support summation and pow_eq_zero_of_le identify E(t) with exp(t B). No minimal nilpotence index, observability, nonzero sensor or nonzero initial state is assumed. Fix the installed material and sensor charts and a source-independent schedule before quantifying over every real x0.
The input is a completed actual acquisition on one commissioned specimen: one initialization, one FlowStart, nu nondisturbing timed vector reads and one FlowStop. For nu>=2 the nodes satisfy 0=t_0<…<t_(nu-1)=T; for nu=1 the sole node is T. The actual trajectory is x(t)=E(t)x0 and the retained replies are y_i=Cx(t_i). A read at T precedes the stop, or uses the installed convention with the same endpoint. The completed record retains its chronological order, timestamps, start/stop phase and genuine source, port, version, chart, reference, owner and rights bindings. The stopped specimen is held at z=E(T)x0 while local computation takes place.
For output coordinate r form P_r(X)=sum_(j<nu) C_r(B^j x0) X^j/j!. Expanding matrix multiplication gives P_r(t)=(CE(t)x0)_r. Polynomial.degree_sum_fin_lt supplies its degree bound even when P_r is zero. For the distinct nodes, Lagrange.eq_interpolate gives P_r(t)=sum_i L_i(t)(y_i)r, where L_i(t)=product(j<nu,j!=i) (t-t_j)/(t_i-t_j). The literal product follows by evaluating Lagrange.basis and basisDivisor. Thus the interpolation applies to the actual replies with no inverse of C or of a state-observation map.
Define Memory_k independently as the vector interval integral from 0 to T of (t/T)^k Cx(t), for k<nu. Define W_ki independently as the scalar interval integral of (t/T)^k L_i(t). To construct a weight by finite arithmetic, multiply the displayed linear factors and write L_i(t)=sum_(r<nu) lambda_ir t^r. Polynomial.as_sum_range_C_mul_X_pow’ supplies this expansion. Interval-integral linearity and integral_pow then give W_ki=sum_(r<nu) lambda_ir T^(r+1)/(k+r+1). Node differences are nonzero and T>0; these are the only divisions required beyond the positive integer denominators. The receiver constructs the coefficients and weights from the supplied nodes and T, then computes mu_k=sum_i W_ki y_i after stop. Its computation requires no source integral operation and uses neither x0 nor a hidden trajectory as an operand.
Multiplying the interpolation identity by (t/T)^k and applying intervalIntegral.integral_finsetSum and integral_mul_const proves mu_k=Memory_k. All integrands are continuous on the finite interval. ContinuousLinearMap.intervalIntegral_comp_comm for each coordinate projection identifies the component calculation with the vector Bochner integral. This proves every k<nu; the same calculation in fact allows every natural weight exponent k. With rational nodes and rational positive T, Lagrange.basis over the rationals maps to the same real basis, so its coefficients and the displayed finite weight formula are rational. This rational-weight assertion does not require x0 to be rational and does not supply a serializer for an arbitrary real reply.
Preservation concerns the original installed run as well as the values. Let rho carry that native run, its actual chronological record, trajectory, stopped state and held processing phase, together with the original installed and performed-source relation. The finite receiver appends only the locally computed moment payload; its source projection is exactly rho. The nondisturbing comparison integrators have output Memory on that same rho. The equality above therefore identifies (rho,mu) with (rho,Memory), preserving the actual source relation, the entire trajectory on [0,T], the endpoint and the complete fixed framing. The run witness states this relation; it is not an operand that reveals hidden field coordinates to the receiver. This argument neither reconstructs provenance from an array nor checks or grants an absent source right. The chronological source trace remains the original initialization/start/taps/stop trace, with no second specimen, replay, future read or restoration operation. Mathematical evaluation at negative time installs no negative-duration source action.
For nu=1 the Lagrange product is empty, hence one, and the sole receiver output is mu_0=T y_0 with the actual tap at T. Zero B, zero C, zero x0 and all blind sectors remain in the same real domain. For the concrete source B=J_2, C=(1,0), T=1 and x0=(2,3), the actual taps at 0 and 1 are 2 and 5, the held endpoint is (5,3), and the weights are the rows (1/2,1/2) and (1/6,1/3). The receiver returns (7/2,2), the integrals of 2+3t and t(2+3t). If a duration-two action is actually called next, the same source advances from (5,3) to (11,3) and returns 11. This is an application of the identities, with the advanced current state retained.
This refinement assumes the paid known law, degree promise, charts, initialization, synchronized exact clock and origin, nondisturbing reads, start/stop and hold controls, serial exclusion, source backing and actual retained invocation rights. Weight construction, arithmetic, storage, parser and local elapsed time are receiver resources. The removed integrators are nondisturbing by their comparison contract. The exact real theorem supplies neither finite exact packets for arbitrary real data nor bit, runtime, energy or physical-realization bounds. A finite rational implementation additionally requires rational B,C,x0,T and nodes, an installed exact rational serializer and the corresponding paid arithmetic and backing. The interpolation creates no new information and makes no claim about independent noisy moment channels.
For the observable small-time moment experiment, retain the same B,C and assume d,p>=1 and C B^k x=0 for all k<d only when x=0. Put N_j=intersection of ker(C B^k) for k<j, E_j=N_j intersect N_(j+1) orthogonal complement, and d_j=dim E_j. Let m be the least j with N_(j+1)=0. Finite observability gives N_d=0, m
The time rescaling S_T:L2((0,T];R^p) to L2((0,1];R^p), represented by S_T g(s)=sqrt(T) g(Ts), is a linear isometry for every T>0. The moment coordinate map U on L2((0,1];R^p) has entries integral_0^1 ell_k(s)g_a(s) ds and contracts the norm by orthogonal projection. Thus U S_T acts on every native L2 class, and its entries are T^(-1/2) integral_0^T ell_k(t/T)g_a(t) dt. Cauchy-Schwarz gives the required integrability for arbitrary representatives; continuous trajectories are only one class of inputs. Applying this same map to C exp(tB)x gives M_T x.
Write D_T=diag(T^(w_i+1/2)) and P(s)=sum_j s^j C B^j projection_(E_j)/j!. The derivative-layer normalized observation theorem gives convergence of the rescaled, layer-normalized trajectory to P with operator error O(T). Every coordinate of P is a polynomial of degree at most m, so U preserves its inner products exactly for every allowed ell. Consequently H_T=D_T^(-1) M_T transpose M_T D_T^(-1) tends to H_0=integral_0^1 P(s)*P(s) ds with error O(T). DerivativeLayerNativeGramian and DerivativeLayerGramianPositivity give positivity of this actual H_0. GradedCongruenceSpectrum then gives positive constants c,K and simultaneous bounds c T^(2w_i+1)<=lambda_i(T)<=K T^(2w_i+1) for all i and sufficiently small T>0, where lambda_i are the canonical decreasing eigenvalues of G_mom(T)=M_T transpose M_T. Also det G_mom(T)=T^(sum_i(2w_i+1)) det H_T and det H_T=det H_0+O(T). These assertions concern the moment Gramian itself.
On any probability space take measurable independent X and xi with laws N(0,beta^(-1)I_d) and the standard Gaussian in R^((m+1)p), where beta>0. For every real sigma with sigma squared positive, Y_T=M_T X+sigma xi has the GaussianObservationLaw joint law with precision tau=1/(sigma squared). The actual Radon-Nikodym relative entropy I_T is finite and equals one half log det(I+G_mom(T)/(beta sigma squared)). Define R_T as the infimum of expected half squared error over all measurable estimators of X from Y_T, and Q_T as the infimum of expected squared error over that same class. Infinite-risk competitors remain in both infima. The Gaussian posterior attains the infimum, R_T is one half trace(beta I+G_mom(T)/(sigma squared)) inverse, and Q_T=2 R_T, both as extended nonnegative values and after conversion to real values.
Diagonalize this same G_mom(T) and apply SpectralNoiseAsymptotics with exponents 2w_i+1. If sigma(T) squared=T^alpha for every T>0, then for every real alpha, I_T=(1/2) sum_j d_j max(alpha-(2j+1),0) log(1/T)+O(1). This information assertion includes equality at every layer threshold. If alpha differs from 2j+1 whenever d_j>0, then R_T tends to (1/(2 beta)) sum_(j:alpha<2j+1) d_j; no exclusion is imposed by an empty layer. For every variance schedule v(T)>0 and every real amplitude schedule with sigma(T) squared=v(T), R_T tends to zero if and only if v(T)=o(T^(2m+1)); the same equivalence holds for Q_T. Necessity uses the occupied last layer, and sufficiency uses the simultaneous spectral upper bounds for risk. No continuity, monotonicity or measurability in T is imposed on these schedules, and their signs may vary.
For fixed signed nonzero sigma, the first-order information coefficient also uses this moment experiment. Its rescaled trajectory is sqrt(T) C exp(TsB). The polynomial space contains the constant functions, so U preserves the initial term sqrt(T) C exactly; the exponential remainder and contraction give G_mom(T)=T CC+O(T squared) in operator norm. The logarithmic determinant estimate in PhysicalFixedNoiseInformation bounds the difference between log det(I+sG) and s trace(G) by (d/2)s squared times the squared operator norm of G for positive G and s>=0, and its trace estimate bounds absolute trace error by d times operator norm error. Apply these estimates with G=G_mom(T) and s=1/(beta sigma squared). Together with the actual Gaussian relative-entropy formula they give I_T=T trace(CC)/(2 beta sigma squared)+O(T squared). In particular there are K>=0 and delta>0 such that the absolute error is at most K T squared for every 0<T<=delta. The constants may depend on the fixed model, basis, beta and sigma. The finite-time moment Gramian is not identified with the integrated exponential-trajectory Gramian; its own estimate supplies the coefficient.