Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Own-path padded charge arrays

Abstract

Chronological own-path differences separate arbitrary INITIAL phase labels.

Definition 1.1 (Own successful differences).

Lean statement: D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/OwnPathCharges.ownCharge

Formalization. D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/OwnPathCharges.ownCharge (✓ std3).

Source. Repository-derived.

Commentary.

Starting from the current scalar, phase, tail, remembered free reading and actual archive, ownCharge follows the selector for a finite remaining budget. A successful issued word contributes its literal increment and recurses at the next scalar, phase, tail and completed archive. A stop, exhausted budget or rejection gives zero for all remaining coordinates. The rejection case retires a common-tail candidate archive; correctness will force every INITIAL label in that archive to agree.

Definition 1.2 (The full phase array).

Lean statement: D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/OwnPathCharges.phaseCharges

Formalization. D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/OwnPathCharges.phaseCharges (✓ std3).

Source. Repository-derived.

Commentary.

For k=2m-2, a constant phase table is retired at the root and has the zero array. Otherwise phaseCharges evaluates ownCharge at INITIAL scalar zero, phase minus j, tail zero, free reading some zero and empty archive. Each phase follows its own acquired path. These finite design coordinates are not extra observations available to a controller.

Theorem 1.3 (Support, cleared root and label separation).

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/OwnPathCharges.original_adaptive_charge_array (✓ std3). ∎

Source. Repository-derived.

Commentary.

Y is arbitrary, including higher universes. In the display k abbreviates 2m-2; flattenWords is the original history flatMap of each complete literal word. output, execute and OriginalRecord are the original scanner definitions, with their positive-k proof arguments omitted. nil is the empty acquired archive. Subtraction inside val is in ZMod(k+1), after casting t*m into that group. Natural subtraction in k remains truncated.

The controller is arbitrary. Its correctness premise covers every actual complete-block history with free reading zero, in either original alphabet, and the target premise retains both scalar values and every legal inherited tail. Coprimality and the joint-history realization supply every phase and tail in that premise. A nonconstant table forbids a leading-one root: tail k-1 would reject all phases into one absorbing native execution. Its first bit is therefore zero and clears every inherited tail. The root phase-zero increment is zero.

At a successful action, literal legality depends on the common tail and word, not on phase or scalar. The endpoint increment selects the next common-scalar, common-tail archive. Equal padded columns follow the same archive through the earlier stop. A common rejection gives the same absorbing continuation and hence a common label; replacing that continuation by zeros loses no label distinction. The support condition follows the actual chronological phase shift t*m, retaining waits and every issued word at its own index.

This theorem constructs the supported adaptive design array. Its rows need not have even full-window parity and need not be a common preset word. It establishes no donor correction, phase-separating fallback stream, preset decoder, finite price or four-block inequality.

Theorem 1.4 (Correct original histories give every actual native source).

Lean statement: D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/OwnPathCharges.native_fiber

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/OwnPathCharges.native_fiber (✓ std3). ∎

Source. Repository-derived.

Commentary.

For arbitrary k>=2, m>=1, either original alphabet, target f, saved value v, budget d and selector, suppose the selector returns the INITIAL target within d paid complete words on every original history whose free scalar is v. For every phase with gcd(m,k+1) dividing its representative and every inherited legal tail s<k, NativeExecute from (v,phase,s) returns f of that INITIAL record with some fee c<=d. Actual-history realization and scanner agreement transfer correctness without supplying the controller a history, phase, tail or clock.

Theorem 1.5 (Equal own arrays force equal labels).

Lean statement: D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/OwnPathCharges.charge_separates

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/OwnPathCharges.charge_separates (✓ std3). ∎

Source. Repository-derived.

Commentary.

For any label universe Y, k>=2, word length m, original selector pi and remaining budget b, take the same current scalar z, legal tail s<k, saved free output and own archive, and two phases p and q. If NativeExecute succeeds at these two records with labels x and y and possibly different paid counts, and their ownCharge arrays agree at every coordinate t<b, then x=y. Induction follows only their own executed actions. Equal successful increments produce equal acquired endpoints and tails; stops and simultaneous rejection have identical continuing archives. The statement permits arbitrary depth, stops and rejecting actions and imposes no schedule or phase-support assumption.

References