RarePriorLiteralController.CurrentAcquisition
The current physical bank determines the native query and successful payload. The same captured operation controls old-field copying, six-frame rendering and successor-bank writeback; role selection preserves the opposite bank.
Theorem 1.1 (Physical bank to resident opcode prefix).
∀ ( saved : LiveProducer . State ) , ∀ ( image : TransferSnapshot ) , ∀ ( a : Fin ( runtimeSize ) → Bool ) , ∀ ( c : Fin ( runtimeSize ) → Bool ) , ∀ ( role : Bool ) , ∀ ( z : Runtime ) , ∀ ( op : Operation ) , (( Function . Injective ( LiveProducer . Current . code )) ∧ ((( ∀ ( q : LiveProducer . Current . State ) , ( programImage ) . length + ( LiveProducer . Current . staticImage ) . length + ( LiveProducer . Current . code ( q )) . length < LiveProducer . Current . bound ) ∧ ((((( image ) . installation ) . tape = programTape → ( if role then c else a ) = LiveProducer . word ( runtimeCodec ( z )) → ∃ ( t : N ) , ∃ ( q : LiveProducer . Current . State ) , (( LiveProducer . Current . run ( LiveProducer . Current . entry ( saved , image , a , c , role , operationCodec ( op )) , 0 , 0 , t ) = q ) ∧ (((( q ) . acquiring = false ) ∧ ((((( q ) . current ) . phase = 2 ) ∧ ((((( q ) . current ) . query = LiveProducer . word ( nativeKeyCodec (( z , op )))) ∧ ((((( q ) . current ) . native = scannerEntry ( nativeKeyCodec (( z , op )))) ∧ (((((( q ) . current ) . opcodes ) . tape = LiveProducer . CurrentBank . opcodeTape ( 0 )) ∧ ((((( q ) . current ) . actual = a ) ∧ ((((( q ) . current ) . synthetic = c ) ∧ ((((( q ) . current ) . operation = operationCodec ( op )) ∧ ((((( q ) . current ) . role = role ) ∧ ((((( q ) . current ) . addressed ) . outer ) . installation . tape = programTape ))))))))))))))))))))) ∧ ((( ∀ ( q : LiveProducer . CurrentBank . State ) , ((( q ) . addressed ) . outer ) . installation . tape = programTape → ( q ) . query = LiveProducer . word ((( q ) . native ) . query ) → (( q ) . opcodes ) . tape = LiveProducer . CurrentBank . opcodeTape ((( q ) . native ) . pc ) → ( LiveProducer . CurrentBank . scanStep ( q )) . native = installedGraphStep ( nativeTable , ( q ) . native )) ∧ ((( ∀ ( q : LiveProducer . CurrentBank . State ) , ∀ ( n : N ) , ( q ) . role = true → ( LiveProducer . CurrentBank . run ( q , n )) . actual = ( q ) . actual ) ∧ ((( ∀ ( q : LiveProducer . CurrentBank . State ) , ∀ ( d : Runtime ) , ( q ) . phase = 9 → ( q ) . bankProbe = 0 → (( q ) . result ) . tape = LiveProducer . word ( optionalRuntimeCodec ( some ( d ))) → ∃ ( t : N ) , ∃ ( r : LiveProducer . CurrentBank . State ) , (( LiveProducer . CurrentBank . run ( q , t ) = r ) ∧ (((( r ) . phase = 11 ) ∧ ((( LiveProducer . CurrentBank . bank ( r ) = LiveProducer . word ( runtimeCodec ( d ))) ∧ (((( r ) . operation = ( q ) . operation ) ∧ (( q ) . role = true → ( r ) . actual = ( q ) . actual ))))))))) ∧ ((( ∀ ( q : LiveProducer . CurrentBank . State ) , (( q ) . pre ) . tape = LiveProducer . word ( runtimeCodec ( z )) → LiveProducer . CurrentBank . fieldROM ( q ) = LiveProducer . word ( fieldsCodec (( z ) . fields ))) ∧ ((( ∀ ( x : Letter ) , ∀ ( y : Letter ) , LiveProducer . Current . step ( LiveProducer . Current . sourceEntry ( saved , image , a , c ) , x , y ) = LiveProducer . Current . entry ( saved , image , a , c , false , operationCodec ( Operation . read ( x )))) ∧ ( ∀ ( q : LiveProducer . Current . State ) , ∀ ( alpha : Letter ) , ∀ ( beta : Letter ) , ∀ ( chi : Letter ) , ∀ ( eta : Letter ) , LiveProducer . Current . actualRequest ( q ) = false → LiveProducer . Current . step ( q , alpha , beta ) = LiveProducer . Current . step ( q , chi , eta )))))))))))))))))
Proof. Machine-checked in Lean as D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorLiteralController/CurrentAcquisition.current_bank_paid_fetch✓ std3). ∎
Source. Repository-derived.
Commentary.
An unprepared current-bank entry reaches the live query and paid resident opcode cut. Installed key/payload accesses refine the native scanner under exact physical relations. A role-selected bitwise writeback preserves the other actual bank during synthetic work. This is a prefix and conditional-suffix result; the full native retirement and canonical-ready cycle remain required.
Theorem 1.2 (Physical bank through installed payload and field copy).
∀ ( saved : LiveProducer . State ) , ∀ ( image : TransferSnapshot ) , ∀ ( a : Fin ( runtimeSize ) → Bool ) , ∀ ( c : Fin ( runtimeSize ) → Bool ) , ∀ ( role : Bool ) , ∀ ( z : Runtime ) , ∀ ( d : Runtime ) , ∀ ( op : Operation ) , (( image ) . installation ) . tape = programTape → ( if role then c else a ) = LiveProducer . word ( runtimeCodec ( z )) → runtimeStep ( z , op ) = some ( d ) → ∃ ( t : N ) , ∃ ( q : LiveProducer . Current . State ) , (( LiveProducer . Current . run ( LiveProducer . Current . entry ( saved , image , a , c , role , operationCodec ( op )) , 0 , 0 , t ) = q ) ∧ (((( q ) . acquiring = false ) ∧ ((((( q ) . current ) . phase = 5 ) ∧ ((((( q ) . current ) . payload = LiveProducer . word ( optionalRuntimeCodec ( some ( d )))) ∧ (((((( q ) . current ) . native ) . pc = 2 ) ∧ ((((( q ) . current ) . actual = a ) ∧ ((((( q ) . current ) . synthetic = c ) ∧ ((((( q ) . current ) . operation = operationCodec ( op )) ∧ ((((( q ) . current ) . role = role ) ∧ ((((((( q ) . current ) . addressed ) . outer ) . installation . tape = programTape ) ∧ (((((( q ) . current ) . result ) . tape = LiveProducer . word ( optionalRuntimeCodec ( some ( d )))) ∧ (((((( q ) . current ) . pre ) . tape = LiveProducer . word ( runtimeCodec ( z ))) ∧ (((((( q ) . current ) . fields ) . tape = LiveProducer . word ( fieldsCodec (( z ) . fields ))) ∧ ((((( q ) . current ) . slot = 0 ) ∧ (((((( q ) . current ) . offset ) . val = 0 ) ∧ ((((( q ) . current ) . row = LiveProducer . keyEntry ( LiveProducer . word ( fieldsCodec (( z ) . fields )) , ⟨( operationCodec ( op )) . val ∗ 6 ⟩)) ∧ ((( ∀ ( x : Letter ) , ∀ ( y : Letter ) , role = false → op = Operation . read ( x ) → LiveProducer . Current . run ( LiveProducer . Current . step ( LiveProducer . Current . sourceEntry ( saved , image , a , c ) , x , y ) , 0 , 0 , t ) = q ) ∧ ( ∃ ( n : N ) , ∃ ( r : LiveProducer . Current . State ) , (( LiveProducer . Current . run ( q , 0 , 0 , n ) = r ) ∧ ((((( r ) . current ) . phase = 7 ) ∧ ((( LiveProducer . Current . output ( r ) = some ( frameTape ( eventROM (( z ) . fields , op , 0 ) , 0 ))) ∧ ((((( r ) . current ) . actual = a ) ∧ ((( r ) . current ) . synthetic = c ))))))))))))))))))))))))))))))))))))))))))
Proof. Machine-checked in Lean as D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorLiteralController/CurrentAcquisition.current_bank_native_payload✓ std3). ∎
Source. Repository-derived.
Commentary.
A current physical bank and raw captured Operation, with all work tapes initially unprepared, reach the original successful Runtime payload, its copied result tape and the original old-field tape. The first event-row key uses this same Operation, and its actual carry and installed address execution expose the original first frame bit. No full retirement, canonical-ready cycle or COMPLETE/U conclusion is asserted.
Theorem 1.3 (Six original frame words and full bank writeback).
∀ ( saved : LiveProducer . State ) , ∀ ( image : TransferSnapshot ) , ∀ ( a : Fin ( runtimeSize ) → Bool ) , ∀ ( c : Fin ( runtimeSize ) → Bool ) , ∀ ( role : Bool ) , ∀ ( z : Runtime ) , ∀ ( d : Runtime ) , ∀ ( op : Operation ) , (( image ) . installation ) . tape = programTape → ( if role then c else a ) = LiveProducer . word ( runtimeCodec ( z )) → runtimeStep ( z , op ) = some ( d ) → ∃ ( tp : N ) , ∃ ( p : LiveProducer . Current . State ) , ∃ ( tr : N ) , ∃ ( q : LiveProducer . Current . State ) , (( LiveProducer . Current . run ( LiveProducer . Current . entry ( saved , image , a , c , role , operationCodec ( op )) , 0 , 0 , tp ) = p ) ∧ (((( p ) . acquiring = false ) ∧ ((((( p ) . current ) . phase = 5 ) ∧ ((( LiveProducer . Current . run ( p , 0 , 0 , tr ) = q ) ∧ ((((( q ) . current ) . phase = 11 ) ∧ ((((( q ) . current ) . actual = ( if role then a else LiveProducer . word ( runtimeCodec ( d )))) ∧ ((((( q ) . current ) . synthetic = ( if role then LiveProducer . word ( runtimeCodec ( d )) else c )) ∧ ((((( q ) . current ) . operation = operationCodec ( op )) ∧ ((((( q ) . current ) . role = role ) ∧ ((((((( q ) . current ) . addressed ) . outer ) . installation . tape = programTape ) ∧ ((( LiveProducer . CurrentBank . trace (( p ) . current , tr ) = ( List . ofFn (( fun slot : Fin ( 6 ) ↦ bitCode ( frameCodec ( eventROM (( z ) . fields , op , slot )))))) . flatten ) ∧ ((( LiveProducer . CurrentBank . trace ( LiveProducer . CurrentBank . entry ( image , a , c , role , operationCodec ( op )) , tp + tr ) = ( List . ofFn (( fun slot : Fin ( 6 ) ↦ bitCode ( frameCodec ( eventROM (( z ) . fields , op , slot )))))) . flatten ) ∧ ((( ∀ ( k : N ) , k ≤ tp + tr → ∃ ( suffix : List ( Bool )) , ( List . ofFn (( fun slot : Fin ( 6 ) ↦ bitCode ( frameCodec ( eventROM (( z ) . fields , op , slot )))))) . flatten = LiveProducer . CurrentBank . trace ( LiveProducer . CurrentBank . entry ( image , a , c , role , operationCodec ( op )) , k ) + + suffix ) ∧ ((( ∀ ( n : N ) , ((( LiveProducer . CurrentBank . run ( LiveProducer . CurrentBank . entry ( image , a , c , role , operationCodec ( op )) , n )) . phase = 12 ) ∧ ( role = true → ( LiveProducer . CurrentBank . run ( LiveProducer . CurrentBank . entry ( image , a , c , role , operationCodec ( op )) , n )) . actual = a ))) ∧ ((( List . map ( original , List . filterMap ( id , List . ofFn (( fun slot : Fin ( 6 ) ↦ decodeFrame ( bitCode ( frameCodec ( eventROM (( z ) . fields , op , slot )))))))) = eventBlock (( z ) . fields , op )) ∧ ( ∀ ( x : Letter ) , ∀ ( y : Letter ) , role = false → op = Operation . read ( x ) → LiveProducer . Current . run ( LiveProducer . Current . step ( LiveProducer . Current . sourceEntry ( saved , image , a , c ) , x , y ) , 0 , 0 , tp + tr ) = q ))))))))))))))))))))))))))))))
Proof. Machine-checked in Lean as D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorLiteralController/CurrentAcquisition.current_bank_original_frames✓ std3). ∎
Source. Repository-derived.
Commentary.
The same unprepared physical-bank producer reaches its old-field row, streams all six original frame codes in exact slot/offset order, and then writes the entire successor Runtime to its selected physical bank while preserving the opposite bank. Every paused output is a prefix of this exact stream, its decoded frame list is the original eventBlock, and all cuts exclude fault and preserve the actual bank in the synthetic role. Actual Read zero and one retain their own acquired Operation. Phase eleven retains work and is not canonical Ready; the exact output claim covers the unprepared physical-bank entry through rendering and writeback.