Effective common-direction digit scheduling

Abstract

A uniform digit controller combines prime-power tests into common-direction positive experiments and retains their complete scalar replies.

Fix a public natural modulus H>=1 and an arbitrary natural pair v=(a,b), including zero. The original chronological calls are R(a,b)=(b,a+b) and G(a,b)=(a+1,b); true means R in TerminalGcdAcquisitionCost.runWord. Write q(a,b)=2a+3b, K=PositiveProbeCompiler.direction(H), Gamma=PositiveProbeCompiler.graftBound(H), and B=costBound(H), the maximum of factorization(H,p)*(p-1) over the finite set primeFactors(H), with empty maximum zero. An experiment word precedes a separately paid current gcd read. The reply is the whole natural number gcd(q(current),H).

In the formulas N denotes the naturals and A(H)=ZMod(H); for positive H this is the residue ring modulo H, while A(0) is the integers. cast(H,n) is the canonical natural-number cast into A(H). PrimeIndex(H) is the subtype of natural primes in primeFactors(H); factorization(H,p) is the exponent of its underlying natural prime. Joint(H) is the function type PrimeIndex(H)->Axis. The definitions below are total for all natural parameters, without a validity condition on local records. All natural subtractions, including p-1 and the rank, truncate at zero; subtraction in a typed A(H) expression is ring subtraction. ite(P,x,y) means x if P holds and y otherwise. let binds its typed local name in the following expression; a typed mapsto expression denotes a function, and constant(X,x) is the function on X taking the value x at every argument. fst and snd are product projections. Triples associate to the right, except that an Axis triple denotes its three-field record constructor; braces in the Axis display list the typed fields of that record type. List(X) is the type of finite ordered lists of X; nil is the empty list, cons prepends, append concatenates left before right, map(f,l) applies f in list order, length counts entries, and count(w,b) counts occurrences of Boolean b in w.

Definition 1.1 (A finite digit record).

$$\mathrm{Axis}=\{\mathrm{level}:\mathbb{N},\mathrm{residue}:\mathbb{N},\mathrm{trial}:\mathbb{N}\}$$

Formalization. D5/S3/Arith/FibonacciAtomic/SourceCoordinates/CommonDirectionScheduler.Axis (✓ std3).

Source. Repository-derived.

Commentary.

For a prime power p^e, a record (s,r,d) consists of a completed digit level, its prefix residue, and the trial digit. Initially it is (0,0,0). The field functions level, residue and trial project these three natural fields; initialAxis=(0,0,0), and center(p,a)=residue(a)+p^level(a)trial(a). The proof invariant for the unknown scalar n is s<=e, r=n mod p^s, 0<=d<p-1, and d<=floor(n/p^s) mod p. The natural rank is (e-s)(p-1)-d.

Definition 1.2 (Advance from the full reply).

$$\forall p:\mathbb{N},(\forall e:\mathbb{N},(\forall a:\mathrm{Axis},(\forall g:\mathbb{N},(\mathrm{advance}\left(p,e,a,g\right)=\mathrm{ite}\left(e\le \mathrm{level}\left(a\right),a,\mathrm{ite}\left((p{)}^{(\mathrm{level}\left(a\right)+1)}\mid g,((\mathrm{level}\left(a\right)+1),(\mathrm{residue}\left(a\right)+((p{)}^{\mathrm{level}\left(a\right)}\cdot \mathrm{trial}\left(a\right))),0),\mathrm{ite}\left((\mathrm{trial}\left(a\right)+1)<(p-1),(\mathrm{level}\left(a\right),\mathrm{residue}\left(a\right),(\mathrm{trial}\left(a\right)+1)),((\mathrm{level}\left(a\right)+1),(\mathrm{residue}\left(a\right)+((p{)}^{\mathrm{level}\left(a\right)}\cdot (p-1))),0)\right)\right)\right)))))$$

Formalization. D5/S3/Arith/FibonacciAtomic/SourceCoordinates/CommonDirectionScheduler.advance (✓ std3).

Source. Repository-derived.

Commentary.

Completed records stay fixed. Otherwise divisibility of the complete reply g by p^(s+1) accepts the center as the next prefix and resets the trial to zero. A failed test increments d when another tested digit remains. After all p-1 failures the last digit p-1 is inferred, the prefix is extended, and the trial resets. Each active update strictly decreases the rank; accepting a low trial can decrease it by more than one. No valuation or Boolean answer replaces g.

Definition 1.3 (One computable CRT shift).

$$\forall H:\mathbb{N},(\forall a:\mathrm{Joint}\left(H\right),((\forall c:\mathbb{N},(\mathrm{Compatible}\left(H,a,c\right)⟺(\forall p:\mathrm{PrimeIndex}\left(H\right),((p{)}^{\mathrm{factorization}\left(H,p\right)}\mid (\mathrm{ite}\left(\mathrm{factorization}\left(H,p\right)\le \mathrm{level}\left(a\left(p\right)\right),\mathrm{residue}\left(a\left(p\right)\right),(\mathrm{residue}\left(a\left(p\right)\right)+((p{)}^{\mathrm{level}\left(a\left(p\right)\right)}\cdot \mathrm{trial}\left(a\left(p\right)\right)))\right)+c))))\wedge \mathrm{shift}\left(H,a\right)=\mathrm{getD}\left(\mathrm{find}\left(\mathrm{range}\left(H\right),((c:\mathbb{N})\mapsto \mathrm{decide}\left(\mathrm{Compatible}\left(H,a,c\right)\right))\right),0\right))))$$

Formalization. D5/S3/Arith/FibonacciAtomic/SourceCoordinates/CommonDirectionScheduler.shift (✓ std3).

Source. Repository-derived.

Commentary.

For each unfinished axis request the negative of its trial center modulo p^e; for a finished axis request the negative of its recovered residue. Compatible(H,a,c) means that desired(p,a)+c is divisible by p^e at every prime divisor. The algorithm searches 0,…,H-1 for the first compatible shift. The existing ZMod CRT equivalence proves that this bounded search succeeds when H>0. The equivalence is used only in the correctness proof; the computation is the finite search. In the formula range(H) is the ascending list 0,…,H-1, decide turns a decidable proposition into its Boolean truth value, find(l,f) returns the first element of l satisfying f as an option, and getD(o,z) returns that element or the default z if the option is empty. This specifies shift even at H=0. No polynomial local-work bound is attached to it.

Definition 1.4 (Chronological full-reply execution).

$$\forall H:\mathbb{N},((\forall a:\mathrm{Joint}\left(H\right),(\forall g:\mathbb{N},(\mathrm{advanceAll}\left(H,a,g\right)=((p:\mathrm{PrimeIndex}\left(H\right))\mapsto \mathrm{advance}\left(p,\mathrm{factorization}\left(H,p\right),a\left(p\right),g\right))))\wedge \forall answer:\mathbb{N}\to \mathbb{N},((\forall a:\mathrm{Joint}\left(H\right),(\mathrm{rounds}\left(H,answer,0,a\right)=(a,\mathrm{nil}))\wedge \forall j:\mathbb{N},(\forall a:\mathrm{Joint}\left(H\right),(\mathrm{rounds}\left(H,answer,(j+1),a\right)=\mathrm{let}c:\mathbb{N}:=\mathrm{shift}\left(H,a\right)\mathrm{in}(\mathrm{let}g:\mathbb{N}:=\mathrm{answer}\left(c\right)\mathrm{in}(\mathrm{let}t:\mathrm{Joint}\left(H\right)\times \mathrm{List}\left(\mathbb{N}\times \mathbb{N}\right):=\mathrm{rounds}\left(H,answer,j,\mathrm{advanceAll}\left(H,a,g\right)\right)\mathrm{in}((\mathrm{fst}\left(t\right),\mathrm{cons}\left((c,g),\mathrm{snd}\left(t\right)\right)))))))))))$$

Formalization. D5/S3/Arith/FibonacciAtomic/SourceCoordinates/CommonDirectionScheduler.rounds (✓ std3).

Source. Repository-derived.

Commentary.

A round computes c from the current finite table, receives g from the reply interface, advances every axis from that same g, and records (c,g) before the recursively generated suffix. After B rounds every prime-power residue is complete. Completed axes remain valid during padding rounds. Negating a final compatible shift in ZMod H reconstructs n modulo H. Thus all axes finish with B paid scalar replies, rather than a sum of their budgets. advanceAll(H,a,g) updates each prime record with the same full reply: at p it is advance(p,factorization(H,p),a(p),g).

Definition 1.5 (The two public directions).

$$\forall H:\mathbb{N},((\forall f:\mathbb{N}\to \mathbb{N},(\mathrm{stage}\left(H,f\right)=\mathrm{ite}\left(H=1,(\mathrm{cast}\left(H,0\right),\mathrm{nil}),\mathrm{let}u:\mathrm{Joint}\left(H\right)\times \mathrm{List}\left(\mathbb{N}\times \mathbb{N}\right):=\mathrm{rounds}\left(H,f,\mathrm{costBound}\left(H\right),\mathrm{constant}\left(\mathrm{PrimeIndex}\left(H\right),\mathrm{initialAxis}\right)\right)\mathrm{in}((-\mathrm{cast}\left(H,\mathrm{shift}\left(H,\mathrm{fst}\left(u\right)\right)\right),\mathrm{snd}\left(u\right)))\right))\wedge \forall answer:\mathbb{N}\to (\mathbb{N}\to \mathbb{N}),(\mathrm{schedule}\left(H,answer\right)=\mathrm{let}s:A\left(H\right)\times \mathrm{List}\left(\mathbb{N}\times \mathbb{N}\right):=\mathrm{stage}\left(H,\mathrm{answer}\left(\mathrm{direction}\left(H\right)\right)\right)\mathrm{in}(\mathrm{let}t:A\left(H\right)\times \mathrm{List}\left(\mathbb{N}\times \mathbb{N}\right):=\mathrm{stage}\left(H,\mathrm{answer}\left((\mathrm{direction}\left(H\right)+1)\right)\right)\mathrm{in}(((\mathrm{fst}\left(s\right),\mathrm{fst}\left(t\right)),\mathrm{append}\left(\mathrm{map}\left(((x:\mathbb{N}\times \mathbb{N})\mapsto (\mathrm{direction}\left(H\right),x)),\mathrm{snd}\left(s\right)\right),\mathrm{map}\left(((x:\mathbb{N}\times \mathbb{N})\mapsto ((\mathrm{direction}\left(H\right)+1),x)),\mathrm{snd}\left(t\right)\right)\right)))))))$$

Formalization. D5/S3/Arith/FibonacciAtomic/SourceCoordinates/CommonDirectionScheduler.schedule (✓ std3).

Source. Repository-derived.

Commentary.

The same local digit policy runs first at direction K and then at direction K+1. The output contains both recovered scalars and the chronological concatenation of triples (k,c,g). For H=1 both stages return zero with an empty tape. The controller takes only H and incoming replies; it never takes a hidden source coordinate. compiledReply(H,v,k,c) is the mathematical interpreter obtained by executing the actual compiler word at v and reading its gcd. Explicitly, terminalGcd(H,w,v)=gcd(q(runWord(w,v)),H), compiledReply(H,v,k,c)=terminalGcd(H,compile(H,k,c),v), and recover(H,a)=-cast(H,shift(H,a)). The displayed stage equation uses this last definition directly. compile is the PositiveProbeCompiler positive Boolean-word compiler; direction is its least k>=1 with fib(k+4)>=H, where fib(0)=0 and fib(1)=1, and graftBound(H)=1+floor((direction(H)+2)/2). runWord executes its list chronologically with true=R and false=G. The interpreter is not a local primitive supplied to the controller.

Definition 1.6 (An explicit earned entry residue).

$$\forall H:\mathbb{N},(\forall y:A\left(H\right)\times A\left(H\right),(\mathrm{decode}\left(H,y\right)=\mathrm{apply}\left(\mathrm{inverse}\left((\mathrm{residueReplace}\left(H\right){)}^{\mathrm{direction}\left(H\right)}\right),(((5\cdot \mathrm{fst}\left(y\right))-(3\cdot \mathrm{snd}\left(y\right))),((-3\cdot \mathrm{fst}\left(y\right))+(2\cdot \mathrm{snd}\left(y\right))))\right)))$$

Formalization. D5/S3/Arith/FibonacciAtomic/SourceCoordinates/CommonDirectionScheduler.decode (✓ std3).

Source. Repository-derived.

Commentary.

The two consecutive quantity rows have matrix [[2,3],[3,5]]. Apply its integer inverse [[5,-3],[-3,2]] in ZMod H, then apply the inverse of the public residue replacement permutation to the K-th power. The resulting pair is the entry residue. This is a computation on the two earned scalars, not a hidden label. Here residueReplace(H) is the permutation of A(H) x A(H) sending (x,z) to (z,x+z), with inverse (x,z) |-> (z-x,x). Its power is composition iterated direction(H) times, and inverse denotes the inverse permutation; apply evaluates it. All coefficients in decode are cast into A(H).

Theorem 1.7 (All natural sources and the complete reply tape).

$$\forall H:\mathbb{N},((1\le H)⟹(\forall v:\mathbb{N}\times \mathbb{N},(\mathrm{let}T:(A\left(H\right)\times A\left(H\right))\times \mathrm{List}\left(\mathbb{N}\times (\mathbb{N}\times \mathbb{N})\right):=\mathrm{schedule}\left(H,\mathrm{compiledReply}\left(H,v\right)\right)\mathrm{in}((\mathrm{decode}\left(H,\mathrm{fst}\left(T\right)\right)=\mathrm{residueSource}\left(H,v\right)\wedge \mathrm{fst}\left(T\right)=(\mathrm{cast}\left(H,q\left(\mathrm{iterateR}\left(\mathrm{direction}\left(H\right),v\right)\right)\right),\mathrm{cast}\left(H,q\left(\mathrm{iterateR}\left((\mathrm{direction}\left(H\right)+1),v\right)\right)\right))\wedge \mathrm{length}\left(\mathrm{snd}\left(T\right)\right)=\mathrm{ite}\left(H=1,0,(2\cdot \mathrm{costBound}\left(H\right))\right)\wedge \forall t:\mathbb{N}\times (\mathbb{N}\times \mathbb{N}),((t\in \mathrm{snd}\left(T\right))⟹(((\mathrm{fst}\left(t\right)=\mathrm{direction}\left(H\right)\vee \mathrm{fst}\left(t\right)=(\mathrm{direction}\left(H\right)+1))\wedge \mathrm{fst}\left(\mathrm{snd}\left(t\right)\right)<H\wedge \mathrm{count}\left(\mathrm{compile}\left(H,\mathrm{fst}\left(t\right),\mathrm{fst}\left(\mathrm{snd}\left(t\right)\right)\right),\mathrm{true}\right)=\mathrm{fst}\left(t\right)\wedge \mathrm{count}\left(\mathrm{compile}\left(H,\mathrm{fst}\left(t\right),\mathrm{fst}\left(\mathrm{snd}\left(t\right)\right)\right),\mathrm{false}\right)\le \mathrm{graftBound}\left(H\right)\wedge \mathrm{snd}\left(\mathrm{snd}\left(t\right)\right)=\gcd \left((q\left(\mathrm{iterateR}\left(\mathrm{fst}\left(t\right),v\right)\right)+\mathrm{fst}\left(\mathrm{snd}\left(t\right)\right)),H\right)\wedge \mathrm{snd}\left(\mathrm{snd}\left(t\right)\right)=\mathrm{terminalGcd}\left(H,\mathrm{compile}\left(H,\mathrm{fst}\left(t\right),\mathrm{fst}\left(\mathrm{snd}\left(t\right)\right)\right),v\right)\wedge \forall current:\mathbb{N}\times \mathbb{N},((\mathrm{residueSource}\left(H,current\right)=\mathrm{residueSource}\left(H,v\right))⟹((\mathrm{residueSource}\left(H,current\right)=\mathrm{residueSource}\left(H,v\right)\wedge \mathrm{terminalGcd}\left(H,\mathrm{compile}\left(H,\mathrm{fst}\left(t\right),\mathrm{fst}\left(\mathrm{snd}\left(t\right)\right)\right),current\right)=\mathrm{terminalGcd}\left(H,\mathrm{compile}\left(H,\mathrm{fst}\left(t\right),\mathrm{fst}\left(\mathrm{snd}\left(t\right)\right)\right),v\right))))))))))))$$

Proof. Machine-checked in Lean as D5/S3/Arith/FibonacciAtomic/SourceCoordinates/CommonDirectionScheduler.effective_scheduler (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every H>=1 and every actual natural pair v, the decoded output is residueSource(H,v). The two scalar outputs are q(R^K(v)) and q(R^(K+1)(v)) in ZMod H. The tape has zero entries when H=1 and exactly 2B otherwise. Every triple has k in {K,K+1}, c<H, exactly k actual R calls and at most Gamma actual G calls in its compiler word, and its retained g equals both the original complete terminal gcd and gcd(q(R^k(v))+c,H). In the formula iterateR(k,v) denotes k iterations of the original R on v, and residueSource(H,v) is its coordinatewise natural cast into A(H) x A(H). The innermost conjunction expands ClosingCut(H,k,c,v,current) into its residue equality and its equality of complete terminal compiler replies.

Digit correctness uses Nat.mod_pow_succ to split a prefix and its next digit. Since p^(s+1) divides H, its divisibility in gcd(n+c,H) is equivalent to the next prefix matching the center. The rank decreases on every unfinished axis; its initial value is e*(p-1)<=B. A finite induction therefore completes all axes at once. CRT injectivity reconstructs the scalar. The concrete PositiveProbeCompiler.effective_short_compiler supplies the actual word, its two action counts, and the exact full terminal reply identity for every natural source. Finally the inverse scalar rows and the residue replacement permutation recover the entry pair.

The reply-interface interpretation requires an actual cut of the same retained handle before each experiment. At that cut the current residue must equal the entry residue. Execute compile(H,k,c) in its listed chronological order, consume each fixed acknowledgement, perform one paid full current gcd read, close by positive original actions back to the required residue, and commit the local table before the next callable cut. ClosingCut states the residue and complete-reply equalities required at an experiment cut. Constructing those positive closing words, their least period, and their actual concatenated action tape is a separate obligation; the present two-stage tape is a tape of requested experiments and replies.

Same-run counting must relate each requested triple to exactly one actual read and include every closing action. In the original notation its target equalities are Q=T0+T1, NR=L_H*(KT0+(K+1)T1), and NG=Hsum(g_j), followed by the stated bounds Q<=2B, NR<=L_H(2K+1)B and NG<=2HGamma*B. These equalities, the integer affine endpoint and every-prefix growth bounds do not follow merely from compiler-word counts. An installed continuation must additionally preserve the immutable earned entry and a separately synchronized current residue after each action, acknowledgement and local commit. No such closing or synchronized continuation is asserted here.

Definition 1.8 (Finite binary local control).

$$\forall H:\mathbb{N},(\forall answer:\mathrm{Binary}\to \mathrm{Binary},((\forall b:\mathrm{BinaryJoint}\left(H\right),(\mathrm{binaryRounds}\left(H,answer,0,b\right)=(b,\mathrm{nil}))\wedge \forall j:\mathbb{N},(\forall b:\mathrm{BinaryJoint}\left(H\right),(\mathrm{binaryRounds}\left(H,answer,(j+1),b\right)=\mathrm{let}c:\mathrm{Binary}:=\mathrm{binaryShift}\left(H,b\right)\mathrm{in}(\mathrm{let}g:\mathrm{Binary}:=\mathrm{answer}\left(c\right)\mathrm{in}(\mathrm{let}t:\mathrm{BinaryJoint}\left(H\right)\times \mathrm{List}\left(\mathrm{Binary}\times \mathrm{Binary}\right):=\mathrm{binaryRounds}\left(H,answer,j,\mathrm{binaryAdvance}\left(H,b,g\right)\right)\mathrm{in}((\mathrm{fst}\left(t\right),\mathrm{cons}\left((c,g),\mathrm{snd}\left(t\right)\right))))))))))$$

Formalization. D5/S3/Arith/FibonacciAtomic/SourceCoordinates/CommonDirectionScheduler.binaryRounds (✓ std3).

Source. Repository-derived.

Commentary.

Encode each natural local field and every complete reply with Nat.digits 2, least significant digit first; zero has the empty encoding. A finite association list has one binary triple per public prime-factor key. decodeJoint looks up that finite table. binaryShift emits the binary encoding of the bounded CRT shift; binaryAdvance decodes the full incoming reply and commits the next encoded table. binaryRounds iterates these operations by structural recursion with an explicit finite round count. Precisely, Binary=List(N), BinaryAxis=Binary x Binary x Binary, and BinaryJoint(H)=List(PrimeIndex(H) x BinaryAxis). digits(n)=Nat.digits(2,n) and ofDigits(c)=Nat.ofDigits(2,c); the latter is the sum of c[i]*2^i over list positions, including lists with digits above one. encodeAxis(a) applies digits to level(a), residue(a), trial(a); decodeAxis applies ofDigits to the three fields. encodeJoint(H,a) is the ascending list of all public prime keys paired with encodeAxis(a(p)). decodeJoint(H,b)(p) decodes the first record with key p in b, using (nil,nil,nil) when p is absent. Thus arbitrary binary tables, not only encoded valid histories, have a defined meaning. binaryShift(H,b)=digits(shift(H,decodeJoint(H,b))) and binaryAdvance(H,b,g)=encodeJoint(H,advanceAll(H,decodeJoint(H,b), ofDigits(g))). card(primeFactors(H)) counts distinct prime keys.

Theorem 1.9 (The binary refinement preserves every finite execution).

$$\forall H:\mathbb{N},(\forall answer:\mathbb{N}\to \mathbb{N},(\forall j:\mathbb{N},(\forall a:\mathrm{Joint}\left(H\right),((\mathrm{binaryRounds}\left(H,((c:\mathrm{Binary})\mapsto \mathrm{digits}\left(\mathrm{answer}\left(\mathrm{ofDigits}\left(c\right)\right)\right)),j,\mathrm{encodeJoint}\left(H,a\right)\right)=(\mathrm{encodeJoint}\left(H,\mathrm{fst}\left(\mathrm{rounds}\left(H,answer,j,a\right)\right)\right),\mathrm{map}\left(((t:\mathbb{N}\times \mathbb{N})\mapsto (\mathrm{digits}\left(\mathrm{fst}\left(t\right)\right),\mathrm{digits}\left(\mathrm{snd}\left(t\right)\right))),\mathrm{snd}\left(\mathrm{rounds}\left(H,answer,j,a\right)\right)\right))\wedge \mathrm{decodeJoint}\left(H,\mathrm{encodeJoint}\left(H,a\right)\right)=a\wedge \mathrm{length}\left(\mathrm{encodeJoint}\left(H,a\right)\right)=\mathrm{card}\left(\mathrm{primeFactors}\left(H\right)\right)\wedge \forall n:\mathbb{N},(\forall d:\mathbb{N},((d\in \mathrm{digits}\left(n\right))⟹(d<2))))))))$$

Proof. Machine-checked in Lean as D5/S3/Arith/FibonacciAtomic/SourceCoordinates/CommonDirectionScheduler.finite_binary_execution (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every natural public H, including H=0, every total scalar reply function, every finite j and every local table, binaryRounds on encoded inputs equals the encoded numeric execution, including its entire ordered shift/reply tape. Decoding an encoded table is exact, the table length is the number of prime divisors, and every encoded digit is below two. There is no positivity restriction on replies or source coordinates. The all-horizon identity applies in particular to both B-round stages with the actual compiler replies.

Nat.ofDigits_digits gives exact field and reply round trips. Finite-table lookup recovers the encoded record for each public prime key. The local binary update therefore commutes with the numeric update, and induction on j transports the entire chronological execution. This proves a finite effective representation. It supplies no numerical bit-work or bit-space bound. Factoring H, bounded shift search, binary arithmetic, word emission, tape storage, service work and backing are still charged resources under the original public finite-computation premises. Only paid reads are optimized.

References

• Truth anchor: D5/S3/Arith/FibonacciAtomic/SourceCoordinates/CommonDirectionScheduler.Axis
• Truth anchor: D5/S3/Arith/FibonacciAtomic/SourceCoordinates/CommonDirectionScheduler.advance
• Truth anchor: D5/S3/Arith/FibonacciAtomic/SourceCoordinates/CommonDirectionScheduler.binaryRounds
• Truth anchor: D5/S3/Arith/FibonacciAtomic/SourceCoordinates/CommonDirectionScheduler.decode
• Truth anchor: D5/S3/Arith/FibonacciAtomic/SourceCoordinates/CommonDirectionScheduler.effective_scheduler
• Truth anchor: D5/S3/Arith/FibonacciAtomic/SourceCoordinates/CommonDirectionScheduler.finite_binary_execution
• Truth anchor: D5/S3/Arith/FibonacciAtomic/SourceCoordinates/CommonDirectionScheduler.rounds
• Truth anchor: D5/S3/Arith/FibonacciAtomic/SourceCoordinates/CommonDirectionScheduler.schedule
• Truth anchor: D5/S3/Arith/FibonacciAtomic/SourceCoordinates/CommonDirectionScheduler.shift
• Dependency: D5/S3/Arith/FibonacciAtomic/GraftAffineClosure
• Dependency: D5/S3/Arith/FibonacciAtomic/SourceCoordinates/PositiveProbeCompiler
• Dependency: D5/S3/Arith/FibonacciAtomic/TerminalGcdAcquisitionCost