Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Exact resonant block responses

Abstract

Actual original-order Boolean words have exact controlled block-response signatures.

Fix any order k at least two and block width m at least one. Set T=k+1, g=gcd(m,T), and p=T/g, with g at least two. The actual weight at position n is c_n=dbonacci k (n+2) modulo two. A live record is (v,theta,s), where v lies in ZMod 2, theta lies in the ambient ZMod T, and s is the length of the trailing run of ones, below k. Complete block histories have theta in P, the image of multiplication by g on ZMod T. Rejection is an independent absorbing record and output.

The original scanner increments s on a one when s+1 is below k, rejects otherwise, and resets s to zero on a zero. Its acceptance agrees with runAdmissible with maximum fuel k-1 and current fuel k-1-s. Boolean lists and finite Boolean coordinate functions describe the same words. DBonacciAdmissible is exactly acceptance from zero. The source output of a legal word is the sum of its true-bit weights c_i, and an illegal word outputs rejection.

In the typed statement, natural subtraction is truncated and natural division is floor division. A value annotated by a ZMod type is the natural-number cast into that type; val is the canonical natural representative. Triples associate to the right. Finite-index brackets carry their displayed bound. All sets, images, products, and cardinalities are finite. FintypeDecidablePiFintype denotes the canonical finite function equality decision Fintype.decidablePiFintype. The Boolean parameter locally selects the full alphabet when false and the locally legal alphabet when true.

Theorem 1.1 (Signatures, joint reachability, and exact response classes).

Proof. Machine-checked in Lean as D5/S1/Words/AdmissibleWords/KBonacciResonantBlockResponses.kbonacci_resonant_block_responses (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every natural horizon H, put b=mH. W_j(theta) is the vector of actual weights c_(theta.val+i) for i in Fin j. At H=0 the signature is the current value, with a separate rejection symbol. At positive H, a nonterminal tail s<k-1 has signature (v,min(k-s,b+1),W_b(theta)). A terminal tail s=k-1 has the separate terminal tag and signature (v,terminal,W_(b-1)(theta+1)). The terminal tag is distinct from every numeric threshold.

For each input alphabet, two records have the same signature if and only if their output functions agree on every controlled suffix of at most H complete blocks. The full alphabet contains all m-bit words. The local alphabet contains precisely those m-bit words accepted from zero. Local legality is tested separately in each aligned block; it permits rejection when a run of k ones crosses a block boundary. Only outputs at complete block endpoints and the current endpoint are observed.

The actual weights have period k+1 modulo two. A one-bit transition adds c_theta to v on a surviving one, advances the ambient phase by one, and increments the tail. A zero advances the phase and clears the tail while keeping v. Concatenation composes these transitions exactly, so an m-bit block is m successive actual one-bit updates. No restriction to P is imposed at intermediate bit positions.

Every v, every phase in P, and every tail below k are jointly realized by one legal word of length divisible by m, in both input alphabets. Compatible congruences select a sufficiently large length N, divisible by m and congruent to theta modulo k+1. An optional initial pulse, zeros, and s final ones produce the requested value, phase, and tail together, because c_0=1. The record set is exactly the actual source image. From every record a finite suffix of locally legal blocks reaches rejection: zeros first clear the tail, k-1 ones end at a block boundary, and a one in the next block rejects.

Equal nonterminal signatures determine both the weighted increments and the initial-run rejection threshold for every suffix. After a first zero, the scanner has a common tail. For terminal records a first one rejects, whereas a first zero clears the tail and exposes exactly b-1 remaining weights from theta+1, including phase wrap. Conversely, the empty suffix distinguishes current values, padded initial runs distinguish unequal thresholds, and isolated pulses distinguish unequal window coordinates. A pulse in the first position separates the terminal and nonterminal tags. Terminal window pulses have an initial zero. Each distinguishing word belongs to both alphabets; an initial-run word may use the entire budget without a trailing zero.

For positive H, there are min(b,k-1) nonterminal thresholds, min(p,b/g+2) nonterminal windows, and min(p,b/g+1) terminal windows. Every combination with either current value is realized by the same-source construction. The disjoint terminal and nonterminal families, together with one rejection class, give the displayed exact counts. The conclusions include k=2, p=1, g=2, H=0, and arbitrarily long horizons.

Zero padding preserves the final output and absorbing rejection. Nonempty padding increases length, advances phase, and resets the live tail; empty padding leaves the record unchanged. Thus the equality relations on controlled response functions for at most H blocks and exactly H blocks coincide, for final outputs and for complete endpoint trajectories, including the current endpoint and H=0. The comparison quantifies over every allowed suffix. It does not assert that one final observed value recovers the earlier trajectory of an already executed input.

References