Exact native raw destinations

Abstract

Every inherited and allocated raw label follows the actual guarded native run.

Theorem 1.1 (All integer bindings of the same successful execution).

$$\forall t:\mathrm{Source}\left(\right),(\forall u:\mathrm{Source}\left(\right),(\forall labels:\mathrm{RawMap}\left(\right),(\forall result:\mathrm{RawMap}\left(\right),(\forall next:\mathbb{Z},(\forall after:\mathbb{Z},(\forall x:\mathrm{Value}\left(\right),(\forall y:\mathrm{Value}\left(\right),((\mathrm{nativeRun}\left(t,labels,next,x,\mathrm{calls}\left(t\right)\right)=\mathrm{some}\left(\mathrm{tuple}\left(u,result,after,y\right)\right))\Rightarrow ((after=(next)+(\mathrm{length}\left(\mathrm{fresh}\left(t\right)\right)))\wedge ((\forall i:\mathbb{Z},((\mathrm{lt}\left(i,next\right))\Rightarrow ((\mathrm{apply}\left(labels,i\right)\in \mathrm{terminals}\left(t\right))\Rightarrow (\mathrm{apply}\left(result,i\right)=\mathrm{inherited}\left(t,\mathrm{apply}\left(labels,i\right)\right)))))\wedge (\forall j:\mathbb{N},((\mathrm{lt}\left(j,\mathrm{length}\left(\mathrm{fresh}\left(t\right)\right)\right))\Rightarrow (\mathrm{apply}\left(result,(next)+(j)\right)=\mathrm{get}\left(\mathrm{fresh}\left(t\right),j\right))))))))))))))$$

Proof. Machine-checked in Lean as D5/S3/Arith/FibonacciAtomic/Geometry/NativeFreshSensorBindings.raw_bindings (✓ std3). ∎

Source. Repository-derived.

Commentary.

RawMap is the actual integer-to-terminal address table used by nativeRun. The integer next is the next fresh identifier, above every authentic original identifier. Inherited follows alpha to LL and beta to LLL, with original branch prefixes unchanged. Fresh lists alpha R and beta R then LR, in allocation order under the fixed left-to-right original-leaf traversal. The theorem proves every old binding below next and every newly allocated integer destination, and the final next integer. At beta, R and LR are distinct addresses and receive different successive integers. No numerical call or pre-growth Tick occurs. Authentic original completeness, genuine grants, framing and physical conformance remain installation premises.

References

• Truth anchor: D5/S3/Arith/FibonacciAtomic/Geometry/NativeFreshSensorBindings.raw_bindings
• Dependency: D5/S3/Arith/FibonacciAtomic/Geometry/NativeFreshSensorGrowth