Fresh Coarse Divergence and Saturated Shared Histories

Abstract

Coarse-observable actual tree strategies separate distinct nonconflicting positives at a fresh nonleaf query, forcing saturated shared histories to incur two nonleaf payments on one input.

Sources, addresses, four-valued replies, globally correct strategies, terminal histories and paid sets are the original actual-tree objects. A strategy terminates correctly on every finite source from the same empty initial history. No uniform fuel bound, source description, or finite-family promise is assumed. The coarse readout is the existing leafLabel: alpha is some(true), beta is some(false), while branch and absent both give none. L(W) denotes the existing leafAddresses(W).

Definition 1.1 (Coarse reply map).

Lean statement: D5/S3/Arith/FibonacciAtomic/ActualCoarseReadoutHistory.kappa

Formalization. D5/S3/Arith/FibonacciAtomic/ActualCoarseReadoutHistory.kappa (✓ std3).

Source. Repository-derived.

Commentary.

Kappa sends alpha to some(true), beta to some(false), and both branch and absent to none. The reply carrier is Option Bool.

Definition 1.2 (Chronological coarse histories).

Lean statement: D5/S3/Arith/FibonacciAtomic/ActualCoarseReadoutHistory.kappa_hist

Formalization. D5/S3/Arith/FibonacciAtomic/ActualCoarseReadoutHistory.kappa_hist (✓ std3).

Source. Repository-derived.

Commentary.

KappaHist maps each original report to its address and coarse reply. It preserves order, length and repeated requests. The coarse history carrier H is the existing dependent history type over Address with constant response type Option Bool.

Coarse observability uses Function.FactorsThrough(p, kappaHist): p(a)=p(b) whenever kappaHist(a)=kappaHist(b), for all raw histories a and b, including histories not reached on any source. The strategy, execution and fee definitions are the original actual-tree objects.

Theorem 1.3 (Fresh divergence and saturated nonleaf excess).

$$\forall pi:\mathrm{Strategy}\left(\right),((\mathrm{FactorsThrough}\left(\mathrm{policy}\left(pi\right),\mathrm{kappaHist}\left(\right)\right))⟹(\forall U:\mathrm{Source}\left(\right),(\forall V:\mathrm{Source}\left(\right),(\forall h:H,(((\mathrm{Positive}\left(U\right))\wedge (\mathrm{Positive}\left(V\right))\wedge (U\ne V)\wedge (\mathrm{NC}\left(U,V\right))\wedge (\mathrm{prefix}\left(h,T\left(pi,U\right)\right))\wedge (\mathrm{prefix}\left(h,T\left(pi,V\right)\right)))⟹(\exists s:H,(\exists q:\mathrm{Address}\left(\right),((\mathrm{prefix}\left(\mathrm{concat}\left(\mathrm{concat}\left(h,s\right),\mathrm{one}\left(\mathrm{report}\left(q,\mathrm{leafLabel}\left(U,q\right)\right)\right)\right),T\left(pi,U\right)\right))\wedge (\mathrm{prefix}\left(\mathrm{concat}\left(\mathrm{concat}\left(h,s\right),\mathrm{one}\left(\mathrm{report}\left(q,\mathrm{leafLabel}\left(V,q\right)\right)\right)\right),T\left(pi,V\right)\right))\wedge (\mathrm{leafLabel}\left(U,q\right)\ne \mathrm{leafLabel}\left(V,q\right))\wedge (\neg (q\in A\left(\mathrm{concat}\left(h,s\right)\right)))\wedge ((\neg (q\in L\left(U\right)))\vee (\neg (q\in L\left(V\right))))\wedge (((\mathrm{nonempty}\left(\mathrm{diff}\left(A\left(h\right),L\left(U\right)\right)\right))\wedge (\mathrm{nonempty}\left(\mathrm{diff}\left(A\left(h\right),L\left(V\right)\right)\right)))⟹((2\le \mathrm{card}\left(\mathrm{diff}\left(J\left(pi,U\right),L\left(U\right)\right)\right))\vee (2\le \mathrm{card}\left(\mathrm{diff}\left(J\left(pi,V\right),L\left(V\right)\right)\right))))))))))))$$

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

Source. Repository-derived.

Commentary.

In the formula, T(pi,W)=kappaHist(terminal(pi,W).history), J(pi,W)=paid(terminal(pi,W).history), and A(g) is the finite set of addresses occurring in the coarse history g. concat is chronological list concatenation, report(q,r) is the dependent address-response pair, and one(a) is the singleton list. prefix means List.IsPrefix; diff is finite-set difference; card and nonempty have their ordinary finite-set meanings. Positive is membership in the third native Fibonacci substitution image, and NC is the existing Nonconflict predicate. FactorsThrough is Function.FactorsThrough, applied to the raw policy and kappaHist.

For any common coarse terminal prefix h, the history s extends it to a first differing coarse reply. Coarse observability synchronizes the query at each matching step. Complete compulsory leaf acquisition and literal frontier rigidity rule out identical coarse terminal histories. A repeated address has already fixed its truthful reply on both inputs, so the separating query is fresh. Nonconflict excludes differing labels at a shared leaf. If both inputs have already paid a nonleaf on h, the input for which the fresh query is a nonleaf therefore has two distinct nonleaf payments.

A common raw history cannot replace a common coarse history: branch and absent may already differ while their coarse reports remain equal. The theorem concerns saturated shared histories and the minimal coarse interface. Joint completion, fallback and cache contracts, finite-family pruning, and endpoint classifications are outside its statement.

References

• Truth anchor: D5/S3/Arith/FibonacciAtomic/ActualCoarseReadoutHistory.kappa
• Truth anchor: D5/S3/Arith/FibonacciAtomic/ActualCoarseReadoutHistory.kappa_hist
• Truth anchor: D5/S3/Arith/FibonacciAtomic/ActualCoarseReadoutHistory.shared_history_obstruction
• Dependency: D5/S3/Arith/FibonacciAtomic/ActualImageSevenLeafSeparation