Scalar Stage Address Certificates

Abstract

One known Fibonacci scalar stage determines the exact price of certifying an actual ordered tree image.

Source is the existing nonempty finite ordered full binary tree algebra. The substitution rho sends alpha to beta and beta to pair(beta,alpha), and preserves ordered pairing. I(d) is the range of its d-fold iterate. A(V) and B(V) are the literal alpha and beta leaf-address sets of V; a(V) and b(V) are their cardinalities. D(V) is maximum leaf depth, with root depth zero. For natural L, f(L)=F(3L+3) and g(L)=F(3L+4), with F(0)=0 and F(1)=1. Write t(V,L)=max(0,b(V)+1-f(L)) and M(V,L)=min(b(V),a(V)+t(V,L)). S(f,g,d,V,h,Q) is QuantityAddressCertificate.ScalarSound: all queries in the finite set Q have depth at most h, and every complete U with fa(U)+gb(U)=fa(V)+gb(V) and matching raw replies on Q belongs to I(d). The scalar and replies refer to the same original tree. Competitor shape, composition, leaf count and height are unrestricted. Queries may include roots, branches or absent addresses and need not be closed under prefixes.

Theorem 1.1 (Exact minimum and every attaining set).

$$\forall k\in Nat,((1\le k)⟹(\forall L\in Nat,(\forall V\in Source,((V\in I\left(3\cdot k\right))⟹(\forall h\in Nat,((1\le a\left(V\right))\wedge (a\left(V\right)<b\left(V\right))\wedge ((h<D\left(V\right))⟹(\neg \exists Q\in \mathrm{Finset}\left(Address\right),(S\left(f\left(L\right),g\left(L\right),3\cdot k,V,h,Q\right))))\wedge ((D\left(V\right)\le h)⟹((\forall Q\in \mathrm{Finset}\left(Address\right),((S\left(f\left(L\right),g\left(L\right),3\cdot k,V,h,Q\right))⟹(M\left(V,L\right)\le \mathrm{card}\left(Q\right))))\wedge (\forall Q\in \mathrm{Finset}\left(Address\right),(((S\left(f\left(L\right),g\left(L\right),3\cdot k,V,h,Q\right))\wedge (\mathrm{card}\left(Q\right)=M\left(V,L\right)))\iff (((Q=B\left(V\right))\wedge (b\left(V\right)=M\left(V,L\right)))\vee (\exists C\in \mathrm{Finset}\left(Address\right),((C\subseteq B\left(V\right))\wedge (\mathrm{card}\left(C\right)=t\left(V,L\right))\wedge (Q=A\left(V\right)\cup C)\wedge (a\left(V\right)+t\left(V,L\right)=M\left(V,L\right)))))))\wedge (\exists Q\in \mathrm{Finset}\left(Address\right),((S\left(f\left(L\right),g\left(L\right),3\cdot k,V,h,Q\right))\wedge (\mathrm{card}\left(Q\right)=M\left(V,L\right))))))\wedge (((f\left(L\right)\le a\left(V\right))⟹(M\left(V,L\right)=b\left(V\right)))\wedge ((f\left(L\right)=a\left(V\right)+1)⟹(M\left(V,L\right)=b\left(V\right)))\wedge ((a\left(V\right)+1<f\left(L\right))⟹((f\left(L\right)\le b\left(V\right))⟹(M\left(V,L\right)=\mathrm{cut}\left(a\left(V\right)+b\left(V\right)+1,f\left(L\right)\right))))\wedge ((b\left(V\right)<f\left(L\right))⟹(M\left(V,L\right)=a\left(V\right))))\wedge (\forall Lprime\in Nat,((L\le Lprime)⟹(M\left(V,Lprime\right)\le M\left(V,L\right))))\wedge (\exists Lzero\in Nat,(\forall Lprime\in Nat,((Lzero\le Lprime)⟹(M\left(V,Lprime\right)=a\left(V\right)))))\wedge (\neg (\forall U\in Source,(\forall W\in Source,((n0\left(U\right)=n0\left(W\right))⟹(n1\left(U\right)=n1\left(W\right))))))\wedge (\neg (\forall U\in Source,(\forall W\in Source,((n1\left(U\right)=n1\left(W\right))⟹(n0\left(U\right)=n0\left(W\right))))))))))))$$

Proof. Machine-checked in Lean as D5/S3/Arith/FibonacciAtomic/StageScalarAddressCertificate.result (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every natural k at least one, every natural L, every V in I(3k) and every natural h, b(V)>a(V)>=1. Below D(V) there is no sound query set. At or above D(V), every sound set has at least M(V,L) queries, some sound set has exactly that many, and the displayed equivalence lists all such sets. They are B(V), when b(V)=M(V,L), and A(V) union C, where C is a subset of B(V) with cardinality t(V,L), when a(V)+t(V,L)=M(V,L). Thus a minimum set contains only original leaf addresses. The four price intervals are f<=a, f=a+1, a+1<f<=b and b<f, giving respectively b, b, a+b+1-f and a. For fixed V and h>=D(V), the price is nonincreasing in L and equals a at all sufficiently large stages. The two global scalar equivalence kernels at stages zero and one do not contain each other. Here n0(U)=2a(U)+3b(U) and n1(U)=8a(U)+13b(U); cut(x,y)=max(0,x-y).

Matching all beta endpoints fixes the branch skeleton. Positive weights 0<f<g make alpha the unique minimum-weight replacement of each remaining alpha slot, so the scalar equality reconstructs V. Matching all alpha endpoints and t beta endpoints recovers the exact composition: consecutive Fibonacci weights are coprime, and the remaining possible beta deficit is smaller than f, forcing that deficit to vanish. The existing composition certificate then gives actual image membership.

If both an alpha and a beta endpoint are omitted, the existing composition-preserving exchange produces an image-negative tree matching all queries. Hence soundness requires all alpha or all beta endpoints. Put p=F(3L+2), q=F(3L+1), so f=p+q and g=2p+q, with p,q positive. For any two disjoint sets X,Y of original beta leaves, simultaneous relabeling at X and expansion to pair(alpha,alpha) at Y produces a legal complete tree. Its composition changes by (card(X)+2*card(Y),-card(X)-card(Y)). Its exact reply-change support consists of X, Y and the two immediate children of each member of Y. A nonempty Y supplies a left alpha child, excluding the tree from the actual image.

If at least f beta endpoints are omitted and at least p of them have neither immediate child queried, choose p of those for Y and q other omitted endpoints for X. The batch preserves the scalar and every queried reply, contradicting soundness. Therefore fewer than p omitted slots are unblocked. Distinct blocked slots consume distinct queried child addresses outside the original leaves. This gives a strict excess over a(V)+t(V,L). When fewer than f beta endpoints are omitted, the elementary cardinality bound is a(V)+t(V,L), with equality precisely for the stated alpha-plus-beta subsets. Fibonacci monotonicity gives price monotonicity, and the unbounded Fibonacci lower bound eventually makes t zero. Actual trees of compositions (3,0) and (0,2) agree under n0 but disagree under n1. Actual trees of compositions (13,0) and (0,8) agree under n1 but disagree under n0.

References

• Truth anchor: D5/S3/Arith/FibonacciAtomic/StageScalarAddressCertificate.result
• Dependency: D5/S3/Arith/FibonacciAtomic/QuantityAddressCertificate