Complete recovery on one literal trajectory
Abstract
Complete recovery on one literal trajectory
The carrier is the original GainRay.World(d): a strictly entrywise positive real 2 by 2 source of rank one and trace one, an arbitrary nonzero coefficient vector beta:Fin(d+1) to the reals, and arbitrary real drift. Its gain is the entire ordinary polynomial ofFn(d+1,beta). No individual coefficient, sampled value, sign, actual-degree or spectral eta assumption is added.
Put n=2(d+1). recoveryWord(d) is the chronological list of n individual M actions, one J action, then 2d+1 individual M actions. Its length is 4d+4. Native readings include clock zero and every action at its original clock, for exactly 4d+5 reads. All reads occur on the same world and trajectory. The construction uses a fixed word; it does not require root-dependent actions or return excursions.
The exact prefix matrix GainRayJets.exactBetaReadout returns beta from clocks 0 through n. Equal full histories therefore give equal entire gains. At clock zero trace normalization gives equal drifts. A nonzero degree-at-most-d polynomial has a nonzero value at a positive prefix clock: otherwise d+1 distinct zeros force its coefficients to vanish by GainRayHistory.evaluation_injective. GainRayWordGeometry.m_power_coordinates then gives equality of trace(M P).
In the final block, partition its 2d+2 consecutive clocks into d+1 adjacent pairs. If each pair contained a root, choosing one root from each pair would produce d+1 distinct roots and contradict the nonzero coefficient vector. Hence some pair has two nonzero values. Dividing the two equal read equations by these checked nonzero gains gives equal consecutive M-power traces against J M^n P. The recurrence M^2=M+I propagates this equality backwards to powers zero and one.
The four trace functionals against I,M,J,MJ separate every real 2 by 2 matrix. Apply them to M^n P and M^n Q: their first two traces agree from the pure-M prefix, and the last two from the final nonroot pair. Invertibility of the actual acquisition M^n gives P=Q. This identification step uses neither rank-one reconstruction as a premise nor an assumed inverse of the complete history map.
Theorem 1.1 (The original history determines the complete target).
Lean statement: D5/S3/Observer/Linear/GainRayCompleteRecovery.recovery_identifies
Proof. Machine-checked in Lean as D5/S3/Observer/Linear/GainRayCompleteRecovery.recovery_identifies (✓ std3). ∎
Source. Repository-derived.
Commentary.
For every natural d and every W,V:World d, equality of readings W recoveryWord(d) and readings V recoveryWord(d) implies W.source=V.source, W.coeff=V.coeff and W.drift=V.drift. The conclusion determines the original source and the entire coefficient vector, rather than only a gain ray.
recoveryMatrix(d) pads exactBetaReadout(d) with zero columns after clock n. recoveryReadout(d,w) is that matrix when w=recoveryWord(d), and zero otherwise. The native recoveryProtocol assigns the singleton containing recoveryReadout(d,w) to every word, so the palette is countable and independent of observed values. Before the fixed word length it executes the next single atom of recoveryWord; at and beyond that length it stops. The decisions are total on all histories.
recoveryAnswer(d,w,h) is a total function of the supplied word and history only. On a nonempty compatible-world fiber it chooses one compatible world and returns its source, entire gain and drift; on an empty fiber it returns zero. Classical choice is permitted by the unrestricted native function model. recovery_identifies proves that the chosen target is the actual target at the terminal word. This is an exact set-theoretic deterministic protocol; no computability, time complexity, numerical stability or finite-precision claim is made.
Theorem 1.2 (Complete target and exact beta at every actual terminal).
Lean statement: D5/S3/Observer/Linear/GainRayCompleteRecovery.complete_recovery
Proof. Machine-checked in Lean as D5/S3/Observer/Linear/GainRayCompleteRecovery.complete_recovery (✓ std3). ∎
Source. Repository-derived.
Commentary.
For every declared natural d with 1<=d, CompleteCorrect(recoveryProtocol(d),recoveryAnswer(d),4d+5) holds. In addition, for every original W:World d, word w, and matrix C in the protocol palette at w, if Terminates(recoveryProtocol(d),W,w,C), then w=recoveryWord(d), w.length+1=4d+5, C multiplied by readings W w equals W.coeff exactly, and recoveryAnswer(d,w,readings W w) equals (W.source,gain(d,W.coeff),W.drift). Thus the same actual terminal history supports full recovery and a fixed-matrix gain output with scale one.
Actual degree zero through d, zero individual coefficients, arbitrary signs and drift, sampled or repeated roots, and eta(P)=0 remain in scope. No source observation, world-dependent policy, reset, copied world, unread compound action, skipped read, extra sensor or changed clock is used. The bound supplies complete recovery, with no optimality assertion for unrestricted nonlinear protocols and no closure claim for other mixed-word bounds.