Native ambient beta cherry sectors

Abstract

Six actual ambient pair actions imply the exact period and higher-power identities.

Theorem 1.1 (All six ambient actions).

$$\forall t:\mathrm{Source}\left(\right),(\forall p:\mathrm{Address}\left(\right),((\mathrm{subtree}\left(p,t\right)=\mathrm{some}\left(\mathrm{mul}\left(\mathrm{beta}\left(\right),\mathrm{beta}\left(\right)\right)\right))\Rightarrow ((\mathrm{adjacency}\left(\mathrm{grown}\left(t\right),\mathrm{vector}\left(p,\mathrm{empty}\left(\right)\right)\right)=(\mathrm{vector}\left(p,L\left(\right)\right))+(\mathrm{vector}\left(p,R\left(\right)\right)))\wedge ((\mathrm{adjacency}\left(\mathrm{grown}\left(t\right),\mathrm{vector}\left(p,L\left(\right)\right)\right)=((\mathrm{vector}\left(p,\mathrm{empty}\left(\right)\right))+(\mathrm{vector}\left(p,\mathrm{LL}\left(\right)\right)))+(\mathrm{vector}\left(p,\mathrm{LR}\left(\right)\right)))\wedge ((\mathrm{adjacency}\left(\mathrm{grown}\left(t\right),\mathrm{vector}\left(p,\mathrm{LL}\left(\right)\right)\right)=(\mathrm{vector}\left(p,L\left(\right)\right))+(\mathrm{vector}\left(p,\mathrm{LLL}\left(\right)\right)))\wedge ((\mathrm{adjacency}\left(\mathrm{grown}\left(t\right),\mathrm{vector}\left(p,\mathrm{LLL}\left(\right)\right)\right)=\mathrm{vector}\left(p,\mathrm{LL}\left(\right)\right))\wedge ((\mathrm{adjacency}\left(\mathrm{grown}\left(t\right),\mathrm{vector}\left(p,R\left(\right)\right)\right)=\mathrm{vector}\left(p,\mathrm{empty}\left(\right)\right))\wedge (\mathrm{adjacency}\left(\mathrm{grown}\left(t\right),\mathrm{vector}\left(p,\mathrm{LR}\left(\right)\right)\right)=\mathrm{vector}\left(p,L\left(\right)\right)))))))))$$

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

Source. Repository-derived.

Commentary.

For a literal original beta cherry at address p, vector(p,z) is the difference of coordinate vectors at pLz and pRz. The constants empty, L, R, LL, LR and LLL mean the corresponding lists of false and true. B is adjacency of grown(t), computed from its actual material and neighbor lists. Each equality is an equality of fields at every address. A complete local calculation includes the common parent, where the two owner contributions cancel. The zero-root transport theorem carries the calculation through an arbitrary native context, including every exterior coordinate.

Theorem 1.2 (Period two and exact higher powers).

$$\forall t:\mathrm{Source}\left(\right),(\forall p:\mathrm{Address}\left(\right),((\mathrm{subtree}\left(p,t\right)=\mathrm{some}\left(\mathrm{mul}\left(\mathrm{beta}\left(\right),\mathrm{beta}\left(\right)\right)\right))\Rightarrow ((\mathrm{adjacency}\left(\mathrm{grown}\left(t\right),\mathrm{half}\left(p\right)\right)=\frac{(\mathrm{vector}\left(p,R\left(\right)\right))-(\mathrm{vector}\left(p,\mathrm{LLL}\left(\right)\right))}{2})\wedge ((\mathrm{adjacency}\left(\mathrm{grown}\left(t\right),\mathrm{adjacency}\left(\mathrm{grown}\left(t\right),\mathrm{half}\left(p\right)\right)\right)=\mathrm{half}\left(p\right))\wedge ((\mathrm{iterate}\left(\mathrm{adjacency}\left(\mathrm{grown}\left(t\right)\right),2,\mathrm{vector}\left(p,\mathrm{empty}\left(\right)\right)\right)=((2\cdot (\mathrm{vector}\left(p,\mathrm{empty}\left(\right)\right)))+(\mathrm{vector}\left(p,\mathrm{LL}\left(\right)\right)))+(\mathrm{vector}\left(p,\mathrm{LR}\left(\right)\right)))\wedge ((\mathrm{iterate}\left(\mathrm{adjacency}\left(\mathrm{grown}\left(t\right)\right),2,\mathrm{vector}\left(p,\mathrm{LR}\left(\right)\right)\right)=((\mathrm{vector}\left(p,\mathrm{empty}\left(\right)\right))+(\mathrm{vector}\left(p,\mathrm{LL}\left(\right)\right)))+(\mathrm{vector}\left(p,\mathrm{LR}\left(\right)\right)))\wedge (\mathrm{iterate}\left(\mathrm{adjacency}\left(\mathrm{grown}\left(t\right)\right),4,\mathrm{vector}\left(p,\mathrm{empty}\left(\right)\right)\right)=((6\cdot (\mathrm{vector}\left(p,\mathrm{empty}\left(\right)\right)))+(5\cdot (\mathrm{vector}\left(p,\mathrm{LL}\left(\right)\right))))+(4\cdot (\mathrm{vector}\left(p,\mathrm{LR}\left(\right)\right))))))))))$$

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

Source. Repository-derived.

Commentary.

Write a=vector(p,empty), b=vector(p,L), c=vector(p,LL), d=vector(p,LLL), e=vector(p,R), f=vector(p,LR), and h=(a-c)/2. All scalars are rational. These identities use the six proved native actions and linearity of the actual neighbor sum. The iterate exponents are literal natural numbers; no finite-depth approximation is involved.

References

• Truth anchor: D5/S3/Arith/FibonacciAtomic/Geometry/NativeFreshSensorSector.attained_actions
• Truth anchor: D5/S3/Arith/FibonacciAtomic/Geometry/NativeFreshSensorSector.attained_powers
• Dependency: D5/S3/Arith/FibonacciAtomic/Geometry/NativeFreshSensorGrowth