Tagewerk XXX

Kernel-attested 2-adic divisibility placing the Markoff point (1,1,1) in the connected cage (Bellah–Dunn–Naidu–Wells 2025)

A 2025 result in a domain new to the ledger — Diophantine / arithmetic geometry, the Markoff triples — with its arithmetic core independently re-decided and kernel-attested by two independent routes. The Markoff surface is X₁²+X₂²+X₃²=3X₁X₂X₃; the Markoff mod p graph 𝒢_p has the nonzero mod p solutions as vertices and the Vieta rotations as edges, and Strong Approximation (Bourgain–Gamburd–Sarnak) hinges on connecting the reduction-fixed special point (1,1,1) to the provably connected cage. Bellah, Dunn, Naidu & Wells (arXiv:2511.23401) reduce this to a 2-adic property: the rotation order ord_p(1,1,1) is the order of A=[[0,1],[-1,3]] in GL₂(F_p) (companion matrix of T²−3T+1, discriminant 5), and Theorem 2.10 gives 2^{ν₂(p+1)} | ord_p(1,1,1) whenever p ≡ ±2 (mod 5) (so x=1 is elliptic and (5/p)=−1), while Proposition 3.3 gives ord_p(1,1,1) = π(p)/2 (half the Fibonacci Pisano period). Leibniz re-decides by exact integer arithmetic over the primes p ≡ ±2 (mod 5), including the Mersenne primes 7, 127, 524287, 2147483647 (=2³¹−1), where p+1=2ⁿ so ord = p+1 exactly. Two independent routes agree throughout: a self-contained matrix certificate (A^{p+1}=I forces ord | p+1, and A^{(p+1)/2}≠I then forces 2^{ν₂(p+1)} | ord — no exact order or external lemma needed), and the Pisano identity ord(A) = π(p)/2. A prime p ≡ ±1 (mod 5) makes x=1 hyperbolic and gives A^{p+1}≠I (the order does not divide p+1), confirming the hypothesis is load-bearing. The Lean 4.31 kernel re-decides the divisibility for a spread of primes and for the Mersenne primes up to 2³¹−1, the two-route agreement for p ∈ {7,127}, and the negative control — all plain decide, every theorem depending on no axioms; no native_decide, no sorry. Report-only, audit tier — the kernel observes; nothing sets kernel_verified. LLMs propose nothing; exact arithmetic and the kernel decide.