Real Extension of Fibonacci Source Density Ratios

Abstract

Each real finite-product ratio increases strictly and crosses one at a unique bounded point.

F denotes the natural Fibonacci sequence with F(0)=0 and F(1)=1. Fix natural k>=1 and j. Put d=3k. Nonintegral t is an auxiliary real parameter of finite products; it does not represent a nonintegral number of tree leaves. E,A,D,L,a,b,n,H,q,c,g and lowerEnvelope are the real extension defined in SourceDensityMonotonicity.

Definition 1.1 (Composition count ratio).

Lean statement: D5/S3/Arith/FibonacciAtomic/SourceDensityCrossing.sourceDensity

Formalization. D5/S3/Arith/FibonacciAtomic/SourceDensityCrossing.sourceDensity (✓ std3).

Source. Repository-derived.

Commentary.

sourceDensity(k,t,i) is the ratio of fiberCount(t-i,i) to fiberCount(step iterated 3k times on (t-i,i)). The subtraction is natural subtraction. Its interpretation as a density on the t-leaf source grid requires t>=1 and i<=t. The definition still has values outside this domain, for example fiberCount(0,0)=1. The theorem uses only t>=j+1 with i=j or i=j+1.

In the displayed statement, logQ(k,j) denotes the function t maps to log(q(k,j,t)), and qOverT(k,j) denotes t maps to q(k,j,t)/t. R and N denote the real numbers and natural numbers.

Theorem 1.2 (Strict increase and unique crossing).

$$\forall k,j\in N,(1\le k)⟹(0<c\left(k\right))\wedge (\forall t\in R,(j+1\le t)⟹(0<q\left(k,j,t\right))\wedge (\mathrm{HasDerivAt}\left(\mathrm{logQ}\left(k,j\right),g\left(k,j,t\right),t\right))\wedge (\mathrm{lowerEnvelope}\left(k,j,t\right)\le g\left(k,j,t\right)))\wedge (\mathrm{StrictMonoOn}\left(q\left(k,j\right),\mathrm{Ici}\left(j+1\right)\right))\wedge (\mathrm{Tendsto}\left(\mathrm{qOverT}\left(k,j\right),\mathrm{atTop}\left(\right),\mathrm{nhds}\left(\frac{c\left(k\right)}{j+1}\right)\right))\wedge (\exists \tau \in R,((j+1\le \tau )\wedge (q\left(k,j,\tau \right)=1))\wedge (\forall z\in R,((j+1\le z)\wedge (q\left(k,j,z\right)=1))⟹z=\tau ))\wedge (\exists \tau \in R,((j+1\le \tau )\wedge (q\left(k,j,\tau \right)=1))\wedge (2j+1<\tau )\wedge (\tau <j+\frac{j+1}{c\left(k\right)})\wedge (\forall t\in N,(j+1\le t)⟹((q\left(k,j,t\right)<1)⟺(t<\tau ))\wedge ((q\left(k,j,t\right)=1)⟺(t=\tau ))\wedge ((1<q\left(k,j,t\right))⟺(\tau <t))\wedge ((\frac{\mathrm{sourceDensity}\left(k,t,j+1\right)}{\mathrm{sourceDensity}\left(k,t,j\right)}<1)⟺(t<\tau ))\wedge ((\frac{\mathrm{sourceDensity}\left(k,t,j+1\right)}{\mathrm{sourceDensity}\left(k,t,j\right)}=1)⟺(t=\tau ))\wedge ((1<\frac{\mathrm{sourceDensity}\left(k,t,j+1\right)}{\mathrm{sourceDensity}\left(k,t,j\right)})⟺(\tau <t))))\wedge (\forall t\in N,(j+1\le t)⟹q\left(k,j,t\right)=\frac{\mathrm{sourceDensity}\left(k,t,j+1\right)}{\mathrm{sourceDensity}\left(k,t,j\right)})$$

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

Source. Repository-derived.

Commentary.

The statement combines the analytic bounds, the integer bridge, and the actual density comparisons. The derivative is taken on the whole real line at each legal t, including the endpoint j+1. The reciprocal endpoint bounds follow from the logarithmic-mean kernel sandwich. Cassini’s squared determinant identity links the three affine coordinates, so their logarithmic errors are estimated together.

The finite-product factor H decreases strictly to c and lies strictly between c and one on the legal half-line. Hence q(2j+1)<1 and q(j+(j+1)/c)>1. Continuity gives the crossing between these two points. The decrease of H and its limit c give the strict lower bound H>c. Strict increase gives uniqueness and the three integer comparison equivalences for the real finite-product ratio and actual density ratio. For i=j or j+1 at a legal integer t, the iterated Fibonacci step has coordinates (At+Ei,Dt+Ai). The Catalan and binomial factorial identities give the adjacent fiber-count ratio. Pairing consecutive factors in rising(2n-1,2D)=4^D rising(n-1/2,D) rising(n,D) then gives the integer bridge.

References

• Truth anchor: D5/S3/Arith/FibonacciAtomic/SourceDensityCrossing.result
• Truth anchor: D5/S3/Arith/FibonacciAtomic/SourceDensityCrossing.sourceDensity
• Dependency: D5/S1/Scale/Fibonacci
• Dependency: D5/S3/Arith/FibonacciAtomic/GenealogicalFiberTransport
• Dependency: D5/S3/Arith/FibonacciAtomic/GlobalGcdSampling
• Dependency: D5/S3/Arith/FibonacciAtomic/SourceDensityMonotonicity
• Dependency: D5/S3/Divergence/MeanKernels/LogarithmicMeanSandwich