Polynomial gain and unrestricted deterministic feedback
Abstract
Polynomial gain and unrestricted deterministic feedback
Fix natural numbers k and d, including zero. Parameters consist of three strictly positive real numbers p,q,r, a real vector gamma indexed by Fin k, and a real vector delta indexed by Fin(d+1). The source is the matrix [p,q;r,qr/p]. Its trace a is strictly positive. The gain has ordinary coefficient vector Fin.cons(1,gamma), and the drift has ordinary coefficient vector delta. Polynomial.ofFn makes both polynomials; hence the gain is 1 plus the sum of gamma(j) times t to the power j+1, while the drift is an arbitrary polynomial of degree at most d, including zero.
This is the full coefficient representation of the declared polynomial domain. Polynomial.ofFn_natDegree_lt bounds the actual degree, Polynomial.toFn_comp_ofFn_eq_id recovers every coefficient vector, and Polynomial.ofFn_comp_toFn_eq_id_of_natDegree_lt reconstructs every polynomial of the declared degree. Lower actual degrees are retained. Gain values at later samples may be positive, negative or zero, with arbitrary repeated roots. The initial gain is exactly one.
The full answer is the tuple consisting of the source divided by its trace, the polynomial a times the gain, and the drift polynomial. Equality is matrix equality and polynomial equality in all three components. This target is injective on the declared parameter domain: the constant coefficient of the second component gives a, its remaining coefficients give gamma, the first component then gives the source and its entries p,q,r, and the third component gives delta.
The chronological atoms and cumulative matrices are the original GainRay.action and GainRay.acquisition. Boolean false denotes M=[0,1;1,1], and true denotes J=[0,1;1,0]. The empty word gives the identity. GainRay.acquisition_append states that appending one atom multiplies the current cumulative matrix on the left by that atom. At original index i the scalar read is the gain evaluated at i times the trace of the cumulative prefix matrix times the source, plus the drift evaluated at i. A word of length s therefore has the complete scalar vector indexed by Fin(s+1), including the mandatory initial read.
A Protocol is an arbitrary total function of a chronological word and its complete scalar vector, returning either one next atom or a complete answer. Both inputs are available in full; there is no continuity, measurability, computability, finite-description, countability or linearity condition. The bounded evaluator run counts reads. With no remaining reads it returns none. With n+1 reads available it takes the current read and calls the decision function; an answer terminates with some answer, while a chosen atom continues at the appended word with n remaining reads. Every successful evaluation consequently follows one immutable world and one irreversible consecutive history. The evaluator permits no reset, copy, skipped read, idle operation, unread composite action, reindexing or extra observation.
UniformlyStops P m means that for every legal world, run P world m at the empty word returns some complete answer. The horizon is a total-read bound, not an expected bound. In particular, zero cannot be a uniform stopping bound because the initial read is compulsory. Early stopping is included. A continuation at the last permitted read fails this stopping condition.
Theorem 1.1 (Failure below the full parameter dimension).
Lean statement: D5/S3/Observer/Linear/PolynomialFeedbackDimension.unrestricted_polynomial_feedback_lower_bound
Proof. Machine-checked in Lean as D5/S3/Observer/Linear/PolynomialFeedbackDimension.unrestricted_polynomial_feedback_lower_bound (✓ std3). ∎
Source. Repository-derived.
Commentary.
For every natural k,d,m and every Protocol P, if m<k+d+4 and P stops on every legal world within m total reads, then there are a legal world x and an answer a such that its actual bounded execution returns a and a differs from the full target of x. The strict inequality is essential; this statement asserts no failure at equality.
The parameter domain is a nonempty open subset of a real vector space of dimension k+d+4. On a nonempty convex open chart, the next scalar read is continuously differentiable because p remains positive. If its differential vanishes throughout the chart, the mean value theorem makes it constant. Otherwise its nonzero scalar differential is onto. The implicit function theorem provides a locally injective continuously differentiable parametrization of a level set by the kernel of that differential. A sufficiently small open ball stays in the legal parent chart and has dimension exactly one less, by rank-nullity.
Induction on the remaining read bound preserves every earlier scalar and action in the same actual history. After the current read is made constant on a chart, the decision function is evaluated at one fixed complete history. A stopping answer is constant there, whereas the full target is injective and the chart still has positive dimension. A continuation fixes one atom and recurses on its immediate next read. This supplies the adaptive obstruction without imposing regularity on the protocol and without joining collisions from unrelated fixed words.
For a general positive-intercept gain with constant coefficient alpha>0, replacing the source R by S=alpha R and every higher gain coefficient beta(j) by gamma(j)=beta(j)/alpha preserves every actual scalar read and the full normalized target. This interpretation is restricted to positive alpha. The initial gain-one domain is a declared subdomain; it is not obtained by dividing at a zero initial gain.
The dimension bound specializes to d+5 when k=1 and d+4 when k=0. It supplies the dimension coordinate in comparisons with separate stronger bounds. Such comparisons require their own hypotheses and proofs. The result gives no matching upper bound, no randomized or expected-budget statement, and no assertion that this bound is strongest at every parameter pair. Noise, unknown clocks and additional observation channels are outside this contract.