6 Fine-scale mixing (§6)
Proposition 1.14: the Syracuse law is asymptotically equidistributed at fine scales,
Deduced from the character-sum decay Prop 1.17 (node 7.11, the head of the §7 crux “X-chain”) by Plancherel on \(\mathbb {Z}/3^n\mathbb {Z}\). The §6 machinery around it: Lemma 6.2 (\(F_n\) injective), Cor 6.3 (\(3\)-adic separation of the offsets), the event \(E\) (6.2), the stopping time \(k\), and the Plancherel step.
Campaign estimate: 0 treadmill laps; risk done (100% confidence the node completes as stated).
🏆 COMPLETE and judge-verified (2026-07-14, HEAD 49b32c7): #print axioms fine_scale_mixing \(= [\texttt{propext}, \texttt{Classical.choice}, \texttt{Quot.sound}]\), no sorryAx. The node collapsed to a single tail estimate via two machine-checked identities — mainHigh_eq_restrictedDensity (mainHigh is the Syracuse pushforward restricted to mainEvent) and sum_abs_syracZ_sub_mainHigh_eq (\(\sum _Y|\texttt{syracZ}-\texttt{mainHigh}| = \mathbb {P}(\neg \texttt{mainEvent})\), an equality) — after which \(\texttt{globalGood} \subseteq \texttt{mainEvent}\) and the (6.3) union bound over the three deviation tails (\(g_1,g_2,g_3\)) closed error_l1_high_bound, itself axiom-clean. hbudget discharged from the tight window (lRange_hbudget); the \(A'\)-absorption at \(C_A=30\) shown, not asserted (osc_mainHigh_bound).