Original vector recovery by a complete legal word

Abstract

InterleavedWordRecovery

Definition 1.1 (Complete promised source family).

Lean statement: D5/S3/Arith/FibonacciAtomic/Observer/OriginalVector/InterleavedWordRecovery.original

Formalization. D5/S3/Arith/FibonacciAtomic/Observer/OriginalVector/InterleavedWordRecovery.original (✓ std3).

Source. Repository-derived.

Commentary.

The cut is the entire level of addresses of length m = clog 2 h, including unselected leaves. At selected address q i numerical false is original zero, hence source alpha (true); numerical true is original one, hence source beta (false). Every unselected leaf is alpha. The ordered injective selection and complete skeleton are common promised input, rather than acquired shape evidence. Every full vector is allowed, including all-alpha sources outside the alpha orbit. At h = 1 the root is the selected leaf.

Definition 1.2 (Native Q, U and Z table).

Lean statement: D5/S3/Arith/FibonacciAtomic/Observer/OriginalVector/InterleavedWordRecovery.program

Formalization. D5/S3/Arith/FibonacciAtomic/Observer/OriginalVector/InterleavedWordRecovery.program (✓ std3).

Source. Repository-derived.

Commentary.

Q s reads q at index length s followed by length s divided by two right steps. At even epochs alpha and beta decode to zero and one; at odd epochs beta and branch decode to zero and one. The total four-valued response table holds Q s for unsupported replies, including absence. A supported Read appends one bit and enters U s or the final Z s. U s performs exactly one genuine substitution on the same source and enters Q s. Z s halts with its fixed full vector. The initial vertex is Q empty for every source.

Definition 1.3 (Alternating block level coordinates).

Lean statement: D5/S3/Arith/FibonacciAtomic/Observer/OriginalVector/InterleavedWordRecovery.encode

Formalization. D5/S3/Arith/FibonacciAtomic/Observer/OriginalVector/InterleavedWordRecovery.encode (✓ std3).

Source. Repository-derived.

Commentary.

For each zero-based Read index i, coordinates 5i and 5i+1 record zero and one. Coordinate 5i+3 records the following Update, when present. Coordinates of residues two and four remain zero. Earlier blocks stay activated and later blocks stay zero. The final Read block has no following separator or Update. The exact width is 5h-3. This is the source’s explicit level-coordinate construction, an application of the classical Havel–Moravek method, rather than an independent graph-theory result.

Definition 1.4 (Exact installed image).

Lean statement: D5/S3/Arith/FibonacciAtomic/Observer/OriginalVector/InterleavedWordRecovery.Installed

Formalization. D5/S3/Arith/FibonacciAtomic/Observer/OriginalVector/InterleavedWordRecovery.Installed (✓ std3).

Source. Repository-derived.

Commentary.

Installed h consists precisely of encode applied to all Q, U and Z vertices. No ambient word has an instruction row. The inverse is an immutable table lookup. It does not introduce a persistent decoded vertex.

Definition 1.5 (Word-only row selection).

Lean statement: D5/S3/Arith/FibonacciAtomic/Observer/OriginalVector/InterleavedWordRecovery.wordProgram

Formalization. D5/S3/Arith/FibonacciAtomic/Observer/OriginalVector/InterleavedWordRecovery.wordProgram (✓ std3).

Source. Repository-derived.

Commentary.

The only mutable controller argument is one Installed word. Its row chooses the instruction, materialized literal, immediate response word and fixed full output. Source, prefix support, epoch, rank and trace are proof coordinates and are unavailable to row selection. The proof uses NativeSerialMachine.Run and nativeStep for both representations, preserving the same physical source, chronological raw replies, source successors and first full Halt.

In the formula, m abbreviates clog 2 h; FullVectors h is the subtype of Boolean lists of length h; u x abbreviates original m q x; T x abbreviates chronology q 0 x; Q, U and Z omit proof-irrelevant bound fields. E is encode, I is install, J is inverse, and liftConfig changes only the vertex to its installed word. readCount is the length of answers; updateCount counts update events; Reached is nativeStep reachability from the common initial vertex, epoch zero, the original source and empty trace. ReachedVertices is the subtype of vertices for which some current register is actually reached from the fixed original u x. The displayed word reachability uses the corresponding installed initial word. These notations denote the actual definitions, not additional hypotheses or execution certificates.

Theorem 1.6 (Full native recovery and exact word realization).

$$\forall h:Nat,((0<h)⟹(\forall q:\mathrm{Fin}\left(h\right)\to Address,((\mathrm{Injective}\left(q\right))⟹((\forall i:\mathrm{Fin}\left(h\right),(\mathrm{length}\left(q\left(i\right)\right)=\mathrm{clog}\left(2,h\right)))⟹((\mathrm{Injective}\left(\lambda x:\mathrm{FullVectors}\left(h\right),(\mathrm{original}\left(\mathrm{clog}\left(2,h\right),q,\mathrm{value}\left(x\right)\right))\right))\wedge (\forall x:\mathrm{List}\left(Bool\right),(\forall a:Address,(((\mathrm{length}\left(a\right)=\mathrm{clog}\left(2,h\right))\wedge (\forall i:\mathrm{Fin}\left(h\right),(q\left(i\right)\ne a)))⟹(\mathrm{subtree}\left(a,\mathrm{original}\left(\mathrm{clog}\left(2,h\right),q,x\right)\right)=\mathrm{some}\left(\mathrm{alpha}\left(\right)\right)))))\wedge (\forall x:\mathrm{List}\left(Bool\right),(\forall i:\mathrm{Fin}\left(h\right),(\mathrm{subtree}\left(q\left(i\right),\mathrm{original}\left(\mathrm{clog}\left(2,h\right),q,x\right)\right)=\mathrm{some}\left(\mathrm{of}\left(\mathrm{not}\left(\mathrm{getD}\left(x,\mathrm{value}\left(i\right),false\right)\right)\right)\right))))\wedge (\forall x:\mathrm{List}\left(Bool\right),((\mathrm{length}\left(x\right)=h)⟹((\mathrm{Run}\left(\mathrm{program}\left(q\right),\mathrm{initial}\left(h\right),0,\mathrm{original}\left(\mathrm{clog}\left(2,h\right),q,x\right),\mathrm{chronology}\left(q,0,x\right),x\right))\wedge (\mathrm{Run}\left(\mathrm{wordProgram}\left(q\right),\mathrm{install}\left(\mathrm{initial}\left(h\right)\right),0,\mathrm{original}\left(\mathrm{clog}\left(2,h\right),q,x\right),\mathrm{chronology}\left(q,0,x\right),x\right))\wedge (\forall t:Trace,(\forall z:\mathrm{List}\left(Bool\right),((\mathrm{Run}\left(\mathrm{wordProgram}\left(q\right),\mathrm{install}\left(\mathrm{initial}\left(h\right)\right),0,\mathrm{original}\left(\mathrm{clog}\left(2,h\right),q,x\right),t,z\right))⟹((t=\mathrm{chronology}\left(q,0,x\right))\wedge (z=x)))))\wedge (\mathrm{readCount}\left(\mathrm{chronology}\left(q,0,x\right)\right)=h)\wedge (\mathrm{length}\left(\mathrm{chronology}\left(q,0,x\right)\right)=2\cdot h-1)\wedge (\mathrm{updateCount}\left(\mathrm{chronology}\left(q,0,x\right)\right)=h-1)\wedge (\mathrm{localStep}\left(\right)\neg \in \mathrm{chronology}\left(q,0,x\right))\wedge (\mathrm{card}\left(\mathrm{ReachedVertices}\left(h,q,x\right)\right)=2\cdot h))))\wedge (\forall x:\mathrm{List}\left(Bool\right),((\mathrm{length}\left(x\right)=h)⟹(\forall v:\mathrm{Vertex}\left(h\right),(\forall r:Source,((\mathrm{Reached}\left(q,\mathrm{original}\left(\mathrm{clog}\left(2,h\right),q,x\right),v,r\right))⟺((\mathrm{Fits}\left(v,x\right))\wedge (r=\mathrm{iterate}\left(substitution,\mathrm{epochOf}\left(v\right),\mathrm{original}\left(\mathrm{clog}\left(2,h\right),q,x\right)\right))))))))\wedge (\mathrm{card}\left(\mathrm{Vertex}\left(h\right)\right)=3\cdot \mathrm{pow}\left(2,h\right)-3)\wedge (\mathrm{card}\left(\mathrm{Installed}\left(h\right)\right)=3\cdot \mathrm{pow}\left(2,h\right)-3)\wedge (\forall w:\mathrm{Installed}\left(h\right),(\mathrm{Adm}\left(5\cdot h-3,\mathrm{value}\left(w\right)\right)))\wedge (\mathrm{Injective}\left(\mathrm{encode}\left(h\right)\right))\wedge (\forall s:\mathrm{List}\left(Bool\right),((\mathrm{length}\left(s\right)<h)⟹(\forall b:Bool,(\mathrm{hammingDist}\left(\mathrm{encode}\left(Q\left(s\right)\right),\mathrm{encode}\left(\mathrm{child}\left(s,b\right)\right)\right)=1))))\wedge (\forall s:\mathrm{List}\left(Bool\right),(((0<\mathrm{length}\left(s\right))\wedge (\mathrm{length}\left(s\right)<h))⟹(\mathrm{hammingDist}\left(\mathrm{encode}\left(U\left(s\right)\right),\mathrm{encode}\left(Q\left(s\right)\right)\right)=1)))\wedge (\forall s:\mathrm{List}\left(Bool\right),((\mathrm{length}\left(s\right)<h)⟹(\forall r:Reply,((\mathrm{decode}\left(\mathrm{length}\left(s\right),r\right)=\mathrm{none}\left(\right))⟹((\mathrm{response}\left(s,r\right)=Q\left(s\right))\wedge (\mathrm{hammingDist}\left(\mathrm{encode}\left(Q\left(s\right)\right),\mathrm{encode}\left(\mathrm{response}\left(s,r\right)\right)\right)=0))))))\wedge (\forall w:\mathrm{Installed}\left(h\right),(\exists x:\mathrm{List}\left(Bool\right),((\mathrm{length}\left(x\right)=h)\wedge (\exists e:Nat,(\exists r:Source,(\exists t:Trace,(\mathrm{Reaches}\left(\mathrm{nativeStep}\left(\mathrm{wordProgram}\left(q\right)\right),\mathrm{tuple}\left(\mathrm{install}\left(\mathrm{initial}\left(h\right)\right),0,\mathrm{original}\left(\mathrm{clog}\left(2,h\right),q,x\right),\mathrm{emptyTrace}\left(\right)\right),\mathrm{tuple}\left(w,e,r,t\right)\right))))))))\wedge (\forall s:\mathrm{List}\left(Bool\right),((\mathrm{length}\left(s\right)<h)⟹(\mathrm{wordProgram}\left(q,\mathrm{install}\left(Q\left(s\right)\right)\right)=\mathrm{Read}\left(\mathrm{literal}\left(q,\mathrm{length}\left(s\right)\right),\lambda r:Reply,(\mathrm{install}\left(\mathrm{response}\left(s,r\right)\right))\right))))\wedge (\forall s:\mathrm{List}\left(Bool\right),(((0<\mathrm{length}\left(s\right))\wedge (\mathrm{length}\left(s\right)<h))⟹(\mathrm{wordProgram}\left(q,\mathrm{install}\left(U\left(s\right)\right)\right)=\mathrm{Update}\left(\mathrm{install}\left(Q\left(s\right)\right)\right))))\wedge (\forall s:\mathrm{List}\left(Bool\right),((\mathrm{length}\left(s\right)=h)⟹(\mathrm{wordProgram}\left(q,\mathrm{install}\left(Z\left(s\right)\right)\right)=\mathrm{Halt}\left(s\right))))\wedge (\forall w,c:\mathrm{Installed}\left(h\right),(\mathrm{wordProgram}\left(q,w\right)\ne \mathrm{localStep}\left(c\right)))\wedge (\mathrm{Injective}\left(\lambda x:\mathrm{List}\left(Bool\right),(\mathrm{answers}\left(\mathrm{chronology}\left(q,0,x\right)\right))\right))\wedge (\forall x:\mathrm{List}\left(Bool\right),((\mathrm{length}\left(x\right)=h)⟹(\forall w:\mathrm{Installed}\left(h\right),(\forall r:Source,((\exists e:Nat,(\exists t:Trace,(\mathrm{Reaches}\left(\mathrm{nativeStep}\left(\mathrm{wordProgram}\left(q\right)\right),\mathrm{tuple}\left(\mathrm{install}\left(\mathrm{initial}\left(h\right)\right),0,\mathrm{original}\left(\mathrm{clog}\left(2,h\right),q,x\right),\mathrm{emptyTrace}\left(\right)\right),\mathrm{tuple}\left(w,e,r,t\right)\right))))⟺((\mathrm{Fits}\left(\mathrm{inverse}\left(w\right),x\right))\wedge (r=\mathrm{iterate}\left(substitution,\mathrm{epochOf}\left(\mathrm{inverse}\left(w\right)\right),\mathrm{original}\left(\mathrm{clog}\left(2,h\right),q,x\right)\right))))))))\wedge (\forall v:\mathrm{Vertex}\left(h\right),(\forall e:Nat,(\forall r:Source,(\forall t:Trace,(\mathrm{nativeStep}\left(\mathrm{wordProgram}\left(q\right),\mathrm{tuple}\left(\mathrm{install}\left(v\right),e,r,t\right)\right)=\mathrm{map}\left(\mathrm{nativeStep}\left(\mathrm{program}\left(q\right),\mathrm{tuple}\left(v,e,r,t\right)\right),\mathrm{liftConfig}\left(h\right)\right))))))\wedge (\forall x:\mathrm{List}\left(Bool\right),(\forall a:Address,((\mathrm{length}\left(a\right)=\mathrm{clog}\left(2,h\right))⟹(\mathrm{subtree}\left(a,\mathrm{original}\left(\mathrm{clog}\left(2,h\right),q,x\right)\right)=\mathrm{some}\left(\mathrm{leafValue}\left(q,x,a\right)\right)))))\wedge (\forall u:Source,(\mathrm{substitution}\left(u\right)\ne u)))))))$$

Proof. Machine-checked in Lean as D5/S3/Arith/FibonacciAtomic/Observer/OriginalVector/InterleavedWordRecovery.interleaved_word_recovery (✓ std3). ∎

Source. Repository-derived.

Commentary.

The complete family construction uses ActualCutPartitionRecovery.prefixTrie and its original prefixTrie_at theorem. NativeDepthPatterns.original_present_transport and the unrestricted append-readout component of ActualLeafHistoryRigidity.actual_address_geometry preserve navigation. DelayedOriginalReadout.right_clock_iterate and right_clock_readout supply the reply clocks and genuine-update witness. NativeSerialDepth.run_unique supplies labeled trace and output uniqueness. Pinned finite-cardinality and Hamming facts normalize the resulting exact counts; admissibility uses AdmissibleCount.Adm and AdmissibleCount.adm_iff_no_adjacent_true.

The new inference constructs the source-independent table and its actual native Run, proves both directions of actual Q/U/Z supports, and realizes exactly their installed legal image. Every allowed prefix has a promised completion, including every unary Update position and every fixed full-output halt. The installed union has 3 times 2 to h minus 3 states; one source visits exactly 2h states. Each supported primitive changes exactly one word bit, unsupported replies hold, and the first full Halt immediately follows the final primitive with no local step or intermediate output.

This is conditional mathematical installation under Definition 1.3’s initialization, immutable lookup, literal delivery, native primitive execution, immediate response-write and fixed full-output services. It establishes neither their physical availability nor free setup. It asserts no optimal total cost or minimum width. The old and classical widths and U(h), arbitrary-competitor Read lower bound, Fibonacci and Theta(h) claims, literal/union/service bills and the whole parent theorem remain outside this result. The word execution clause is this explicit code instance; the generic obligations for arbitrary chosen codes in Verification 4.3 are not claimed.

References

• Truth anchor: D5/S3/Arith/FibonacciAtomic/Observer/OriginalVector/InterleavedWordRecovery.Installed
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Observer/OriginalVector/InterleavedWordRecovery.encode
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Observer/OriginalVector/InterleavedWordRecovery.interleaved_word_recovery
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Observer/OriginalVector/InterleavedWordRecovery.original
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Observer/OriginalVector/InterleavedWordRecovery.program
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Observer/OriginalVector/InterleavedWordRecovery.wordProgram
• Dependency: D5/S1/Words/AdmissibleWords/AdmissibleCount
• Dependency: D5/S3/Arith/FibonacciAtomic/Observer/DelayedOriginalReadout
• Dependency: D5/S3/Arith/FibonacciAtomic/Observer/NativeSerialDepth