Original future profiles after actual motion
Abstract
A source-blind finite controller acquires the exact original future-profile cell from at most two genuine replies at one authentic moving cut.
Fix one positive rational original x and one source epoch. The finite chronological prefix u is the actual acknowledged L/R action sequence. Its natural matrix A has determinant one, diagonal entries at least one and nonnegative off-diagonal entries. Later letters multiply on the left, so the existing word-matrix convention is applied to the reverse of u. The actual current value is (ax+b)/(cx+d). No source inverse, reset, copy, saved original or unknown-source advice is an instruction.
The finite original interval I must already be earned by actual replies at authentic cuts, or by an earlier acquired archive on that same source. Its positive lower endpoint is included, zero is excluded, and its finite upper endpoint is excluded. The numerical premise is that x belongs to I. The controller receives only I, the known matrix and B; x occurs only in the semantic correctness assertion. Retained actual constraints must be intersected into this working interval before calling the controller. A hypothetical prediction contributes no acquired row.
Theorem 1.1 (The exact original cell and all future coordinates).
Proof. Machine-checked in Lean as D5/S3/Observer/RationalRouting/TwoReplyProfile.acquired_original_profile (✓ std3). ∎
Source. Repository-derived.
Commentary.
In the formula u is an arbitrary finite Boolean word, I a ProfileCell, B a natural and x a rational. The hypotheses are 1<=B, 0<=I.lower and I.Contains x. The typed local definitions bind the attained matrix A, current value z, source-blind program, output C, original upper bound U, raw-scale parameter Q, first interval J, current magnitude bound V and actual rows. The projections a(A), b(A), c(A) and d(A) denote the four natural matrix entries. Thus U=originalUpper(I)=ceil(I.upper), Q=B(cU+d), V=aU+b+1 and M=max(max(a,b),max(c,d)); size=Nat.size, iw=integerWidth and width=ProfileCell.width. For every B at least one, the first proposed scale is Q squared. The output equals the containing original cell, and membership in that cell is exactly equality of the complete common future profile. Its evaluator returns the original floor coordinate for every finite future word and every scale from 1 through B. There is no bound on the unknown original denominator, no bound on future word length, and no literal-history reconstruction.
First scan the original denominators in I. If the target is already constant, output its cell immediately. Before either possible read, compute the exact lower and upper bounds on that proposed current reply; equality derives the same integer and omits the read. The theorem proves both converses: an already constant target is detected, and every reply constant throughout the working interval is detected by the endpoint test. Otherwise request the complete integer reply at the actual current value. Derived values create no actual-read record, and no separate unit read is requested.
The first reply has scale Q squared. Inverting its half-open cell and intersecting with I gives J. The lower inverse endpoint is clipped at zero; when the upper raw endpoint reaches or exceeds the image asymptote, it imposes no new upper bound on I. This handles translations with c=0 and the zero original slice. The inverse threshold denominator is aD-cr; the forward transported denominator is cj+dm. These expressions have different roles.
Every original target cut j/m strictly inside J has m at most B and transported denominator cj+dm at most Q. Two distinct transported fractions with such denominators cannot share one raw cell at scale Q squared. The scan computes the least numerator above the lower endpoint at each original denominator. Repeated fractions identify the same cut. If none occurs, J already determines the full target. Otherwise the current reply at s=cj+dm decides the original side of j/m by comparison with p=aj+bm. This optional second scale is at most Q. Splitting at that cut leaves a single original full-profile class, including exact ownership of a cut equal to the actual source.
TwoReplyTrace lists the only possible genuine-read traces: no rows, the first row alone, the second row alone after a derived first reply, or both in chronological order. All rows concern the same actual current value. The read-only program type contains no action instruction. Every branch uses finite integer arithmetic, finite denominator scans and at most two supplied finite-completing services. B=1, repeated requested resolutions and noncoprime scales remain in the quantified range.
The arithmetic scans range over original denominators 1 through B, rather than over Q or an LCM. They use integer divisions and cross-products. The endpoint pass is tail recursive and retains only selected endpoint pairs and its current index. AcquisitionScans gives the exact recursive scan execution: at most 3B integer divisions and 4B integer cross-product comparisons across the initial target test, the post-reply cut test and the final endpoint scan. The first inverse interval and every operand in the two cut scans and final endpoint scan satisfy the displayed uniform W bound. The final reduced endpoint denominators are at most B and their numerator magnitudes are at most BU. The fixed amount of rational endpoint, clipping, derived-reply and representative arithmetic is outside these scan counters. Only the final two selected grid pairs are reduced by the endpoint scan. The theorem also bounds the sum of actual scale-name and reply binary widths, with one delimiter bit per integer, by 6 size(Q)+2 size(V)+4, where size is the natural binary bit length. This bound omits skipped rows and charges complete nonnegative replies. Within each quantified e, the native width formula uses W=acquisitionWidth(A,I,B,e)=16(e+(size(B)+1)+(size(U)+1)+(size(M)+1)+1). These integer sizes bound all listed scan operands. The source resource estimate uses its own conservative widths W=16(e+lambda(B)+lambda(U)+mu+1) and local work O(B W squared+W cubed), with only a constant number of selected-fraction reductions. Request bits, output bits, provenance, matrix replay and service-internal resources are separate charges. The reference in Theorem 39.7 to Proposition 39.10 is a source locator discrepancy: the finite-prefix resource vector is Proposition 39.12. The displayed theorem does not supply an execution-cost relation for every fixed rational operation, a total constant gcd-call bound, a uniform width bound for every intermediate of that full computation, or a schoolbook/Euclid primitive cost binding. The complete numerical bit-work estimate and the literal real-log payload bound with constant 12 remain open.