Six original frame words and selected-bank commit

Abstract

RarePriorLiteralController.LiveProducerRendering

The installed scanner cycles pay for resident-opcode copying before each native scan step. scan_exit combines the scanner refinement and PayloadGood invariant with the successful native result. result_exit and fields_exit then copy the successful payload and the original pre-state fields; prepare_event reaches the original event-row key.

Each row key is fieldsCodec times twenty-four plus the captured operation times six plus the slot. The address motor reads the installed frame bit at the current offset. row_emit and offset_emit advance through the entire frameWidth. finish_frame completes the current frame at phase eight while preserving its slot; render_remaining advances between slots, and render_all orders all six frame words. These are actual transition and trace equalities; the chronological slot and offset coordinates remain external proof parameters.

The result below requires rendering entry at phase five, slot and offset zero, the exact encoded old fields, matching row key, captured operation, installed program and the complete successful successor-result tape. It first emits the flattened six frame codes in increasing slot order and then performs quiet selected-bank writeback. The opposite bank, operation, role and outer installation context are retained.

preparing_quiet excludes output before rendering. For an execution that reaches phase eleven, retired_no_fault excludes phase twelve at every cut. render_commit preserves the outer installation context at its endpoint. Phase eleven is a retained-work endpoint; a canonical Ready reset, repeated full cycles, live fresh service, full-tail readout, COMPLETE membership and the full-class risk, radius and threshold claims are outside this result.

Theorem 1.1 (Exact six-frame stream followed by bank writeback).

$$\forall (s:\mathrm{LiveProducer}.\mathrm{CurrentBank}.\mathrm{State}),\forall (z:\mathrm{Runtime}),\forall (d:\mathrm{Runtime}),\forall (\mathrm{op}:\mathrm{Operation}),(s).\mathrm{phase}=5\to (s).\mathrm{operation}=\mathrm{operationCodec}(\mathrm{op})\to ((((s).\mathrm{addressed}).\mathrm{outer}).\mathrm{installation}).\mathrm{tape}=\mathrm{programTape}\to (s).\mathrm{row}=\mathrm{keyEntry}(\mathrm{word}(\mathrm{fieldsCodec}((z).\mathrm{fields})),⟨((s).\mathrm{operation}).\mathrm{val}\ast 6+((s).\mathrm{slot}).\mathrm{val}⟩)\to ((s).\mathrm{fields}).\mathrm{tape}=\mathrm{word}(\mathrm{fieldsCodec}((z).\mathrm{fields}))\to ((s).\mathrm{offset}).\mathrm{val}=0\to (s).\mathrm{slot}=0\to ((s).\mathrm{result}).\mathrm{tape}=\mathrm{word}(\mathrm{optionalRuntimeCodec}(\mathrm{some}(d)))\to \exists (t:\mathbb{N}),\exists (q:\mathrm{LiveProducer}.\mathrm{CurrentBank}.\mathrm{State}),((\mathrm{LiveProducer}.\mathrm{CurrentBank}.\mathrm{run}(s,t)=q)\wedge ((((q).\mathrm{phase}=11)\wedge ((((q).\mathrm{actual}=(\mathrm{if}(s).\mathrm{role}\mathrm{then}(s).\mathrm{actual}\mathrm{else}\mathrm{word}(\mathrm{runtimeCodec}(d))))\wedge ((((q).\mathrm{synthetic}=(\mathrm{if}(s).\mathrm{role}\mathrm{then}\mathrm{word}(\mathrm{runtimeCodec}(d))\mathrm{else}(s).\mathrm{synthetic}))\wedge ((((q).\mathrm{operation}=(s).\mathrm{operation})\wedge ((((q).\mathrm{role}=(s).\mathrm{role})\wedge (((((q).\mathrm{addressed}).\mathrm{outer}=((s).\mathrm{addressed}).\mathrm{outer})\wedge (\mathrm{LiveProducer}.\mathrm{CurrentBank}.\mathrm{trace}(s,t)=(\mathrm{List}.\mathrm{ofFn}((\mathrm{fun}\mathrm{slot}:\mathrm{Fin}(6)\mapsto \mathrm{bitCode}(\mathrm{frameCodec}(\mathrm{eventROM}((z).\mathrm{fields},\mathrm{op},\mathrm{slot})))))).\mathrm{flatten}))))))))))))))$$

Proof. Machine-checked in Lean as D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorLiteralController/LiveProducerRendering.render_commit (✓ std3). ∎

Source. Repository-derived.

Commentary.

The frame sequence is determined by the same original fields and operation as the row key. Its full bit trace survives concatenation with the quiet writeback trace, and both bank equations remain in the conclusion.

References

• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorLiteralController/LiveProducerRendering.render_commit
• Dependency: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorLiteralController/LiveProducerWork