Native fresh sensor growth

Abstract

Fixed original-leaf growth is a successful guarded native execution with fresh-zero rational values.

Theorem 1.1 (Execution on every finite native source).

$$\forall t:\mathrm{Source}\left(\right),(\mathrm{run}\left(t,\mathrm{calls}\left(t\right)\right)=\mathrm{some}\left(\mathrm{grown}\left(t\right)\right))$$

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

Source. Repository-derived.

Commentary.

Source is the original Bool free magma, with true denoting alpha and false beta. The function grown replaces alpha by (beta,alpha) and beta by ((beta,alpha),alpha). The calls traverse the original leaves from left to right. At alpha they promote then split its owner; at beta they split its owner then its left child. Only guarded structural calls occur. Successful traces lift through the existing native runner in arbitrary output contexts.

Theorem 1.2 (Actual execution and fresh-zero inclusion).

$$\forall t:\mathrm{Source}\left(\right),((D\left(t\right))\Rightarrow (\forall l:\mathrm{RawMap}\left(\right),(\forall n:\mathbb{Z},(\forall x:\mathrm{Value}\left(\right),(\exists m:\mathrm{RawMap}\left(\right),(\exists j:\mathbb{Z},(\exists y:\mathrm{Value}\left(\right),((\mathrm{nativeRun}\left(t,l,n,x,\mathrm{calls}\left(t\right)\right)=\mathrm{some}\left(\mathrm{tuple}\left(\mathrm{grown}\left(t\right),m,j,y\right)\right))\wedge ((\forall p:\mathrm{Address}\left(\right),((p\in \mathrm{material}\left(t\right))\Rightarrow (y\left(p\right)=x\left(p\right))))\wedge (\forall p:\mathrm{Address}\left(\right),((p\in \mathrm{material}\left(\mathrm{grown}\left(t\right)\right))\Rightarrow ((\neg (p\in \mathrm{material}\left(t\right)))\Rightarrow (y\left(p\right)=0)))))))))))))$$

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

Source. Repository-derived.

Commentary.

The raw table and next integer are the actual nativeRun arguments and outputs. Every old material address keeps its original rational value and every new material address receives zero. This is the old-cell inclusion E on the same actual attained source. The installation still presumes authentic exhaustive raw bindings, current and fresh rights, complete exclusive framing, exact arithmetic, Hold and sufficient backing. Physical conformance and record isolation remain installation premises. The separate raw_bindings theorem characterizes every inherited and freshly allocated label on this same run; none of these claims acquires an installation premise.

Theorem 1.3 (Full material, terminal and designated counts).

$$\forall t:\mathrm{Source}\left(\right),(((\mathrm{length}\left(\mathrm{material}\left(\mathrm{grown}\left(t\right)\right)\right))+(1)=(5\cdot (\mathrm{fst}\left(\mathrm{composition}\left(t\right)\right)))+(7\cdot (\mathrm{snd}\left(\mathrm{composition}\left(t\right)\right))))\wedge ((\mathrm{length}\left(\mathrm{terminals}\left(\mathrm{grown}\left(t\right)\right)\right)=(2\cdot (\mathrm{fst}\left(\mathrm{composition}\left(t\right)\right)))+(3\cdot (\mathrm{snd}\left(\mathrm{composition}\left(t\right)\right))))\wedge ((\mathrm{length}\left(\mathrm{sensors}\left(t\right)\right)=\mathrm{length}\left(\mathrm{leaves}\left(t\right)\right))\wedge (\forall p:\mathrm{Address}\left(\right),((p\in \mathrm{sensors}\left(t\right))\Rightarrow (p\in \mathrm{terminals}\left(\mathrm{grown}\left(t\right)\right)))))))$$

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

Source. Repository-derived.

Commentary.

If a and c are the original composition counts, grown(t) has 5a+7c-1 actual material cells and 2a+3c current terminals. There is exactly one designated sensor per original logical leaf, and every such sensor is an actual current terminal. Counts include beta material markers and all nondesignated fresh terminals.

Theorem 1.4 (Ambient parent cancellation for a zero root).

$$\forall l:\mathrm{Source}\left(\right),(\forall r:\mathrm{Source}\left(\right),(\forall b:\mathrm{Bool}\left(\right),(\forall x:\mathrm{Value}\left(\right),((x\left(\mathrm{empty}\left(\right)\right)=0)\Rightarrow (\mathrm{update}\left(\mathrm{mul}\left(l,r\right),\mathrm{lift}\left(b,x\right)\right)=\mathrm{lift}\left(b,\mathrm{update}\left(\mathrm{if}\left(b,r,l\right),x\right)\right))))))$$

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

Source. Repository-derived.

Commentary.

The update sums the native neighbors at each material address and is zero outside material. Lift prefixes one edge and assigns zero at every exterior address. The attached root must have value zero; its contribution to the external parent then vanishes. The equation covers every address, including the exterior, and uses no assumed matrix actions.

References

• Truth anchor: D5/S3/Arith/FibonacciAtomic/Geometry/NativeFreshSensorGrowth.actual_values
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Geometry/NativeFreshSensorGrowth.executes
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Geometry/NativeFreshSensorGrowth.inventory
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Geometry/NativeFreshSensorGrowth.update_lift
• Dependency: D5/S3/Arith/FibonacciAtomic/Geometry/NativeGuardedLeafRepair