Mixed-cycle observation and recovery
Abstract
Mixed cycles determine an exact observable window and target-dependent recovery.
Let k and r be natural numbers with r <= k. Let V be a finite-dimensional real inner-product space with orthonormal basis b indexed by Fin(3) plus Fin(k). Write e_i = b(inl(i)) and f_j = b(inr(j)). Hidden indices in the formulas below start at zero: f_r is the first hidden axis outside the prefix of length r.
The visible subspace E is the span of the three e_i. The window W_r is the span of E and f_0 through f_(r-1). The set H consists of the block-diagonal isometries diag(A,Id_F), with A in the actual matrix special orthogonal group on Fin(3). Its definition specifies every basis image, rather than assuming a generic invariant-subspace action. The permutation C_r is the ordered cycle (e_0 f_0 … f_(r-1)), fixing every other basis vector; C_0 is identity.
Let G_r be the subgroup generated by H and C_r. It may be infinite. For g in G_r let y_g(x) = P_E(gx), and write M_r(x) for the entire G_r-indexed family of these vector readouts. The row space R_r is the supremum of g inverse applied to E. For a linear target T, Rec(T) means a linear map from the range of M_r to the target space whose composition with M_r is T. All reconstruction claims concern exactly the jointly attainable observations. Full(T) instead permits an arbitrary function on the entire readout space whose composition with M_r is T.
Theorem 1.1 (Exact row space, four target cases, and escape pairs).
Proof. Machine-checked in Lean as D5/S3/Observer/LinearMemory/MixedCycleRecovery.mixed_cycle_recovery (✓ std3). ∎
Source. Repository-derived.
Commentary.
All displayed conclusions hold together, for every basis and every r <= k, including k = r = 0 and r = 0 < k. Here rank(T) is the dimension of the range of the indicated linear map. It counts independent scalar target coordinates, not the number of vector-valued readouts.
Every generator fixes the hidden tail pointwise. Induction on the generated subgroup extends this fact to every group element and its inverse. Orthogonality then puts every pulled-back visible row in W_r. Conversely, the identity gives the three visible basis vectors, while C_r to the power j+1 sends e_0 to f_j for j < r. These powers give every prefix hidden direction as a pulled-back row. Thus R_r equals W_r.
The kernel of M_r is W_r orthogonal. The universal property of the linear quotient constructs reconstruction on the observation range for exactly those targets whose kernel contains this common kernel. It gives P_E and P_W_r. If r < k, the nonzero vector f_r lies in the common kernel, so x and x+a f_r have identical observations for every real a and distinct states whenever a is nonzero. If r = k, W_r is V and the common kernel vanishes, giving full reconstruction. The native target_recovery_criterion identifies arbitrary-function recovery of the identity target with injectivity, so the same equivalence holds without assuming a linear reconstruction function.
On source E with identity target, the identity group element already reads the entire source and the target rank is three. On source V with target P_E the target rank remains three. On source V with identity target full recovery holds exactly when r = k. On source V with target P_W_r, exact reconstruction and target rank 3+r hold for every r <= k.
This is the linear observation contract of sections 118.1 through 118.3 of AURIC_FIB_SECOND_ORDER_RELATION_COMPLETION_CONTINUATION. It does not supply implementation of C_r in native FIB operations. The number 3+r is an observable scalar rank, with no physical dimension, acquisition cost, seam compatibility or native reachability conclusion.