proofs
Provedmandalic-clockdiscrete-dynamicsformal-model

Mandalic clock: exact base-32 phase dynamics, return time, and colour latch

(∀t∈N, t mod 32+32(t32 mod 32)+1024(t1024)=t)∧(∀t∈N, (t+1024) mod 32=t mod 32∧t+102432 mod 32=t32 mod 32)∧(∀t∈N, t mod 32=0∧t32 mod 32=0  ⟺  t mod 1024=0)∧(∀t∈N, 0<t  ⟹  t mod 32=0  ⟹  t32 mod 32=0  ⟹  1024≤t)∧(∀t∈N, t+3232=t32+1∧t+10241024=t1024+1)∧(102432=32∧10241024=1)∧(∀s,t∈N, s≤t  ⟹  1024≤s  ⟹  1024≤t)\begin{aligned} & \left(\htmlData{mx=15}{\forall t \in \htmlData{mx=14}{\mathbb{N}},\ \htmlData{mx=11}{\htmlData{mx=7}{\htmlData{mx=2}{\htmlData{mx=1}{t} \bmod 32} + \htmlData{mx=6}{32\left(\htmlData{mx=5}{\htmlData{mx=4}{\frac{\htmlData{mx=3}{t}}{32}} \bmod 32}\right)}} + \htmlData{mx=10}{1024\left(\htmlData{mx=9}{\frac{\htmlData{mx=8}{t}}{1024}}\right)}} \mathrel{\htmlData{mx=13}{=}} \htmlData{mx=12}{t}}\right) \\ & \htmlData{mx=0}{\land} \left(\htmlData{mx=32}{\forall t \in \htmlData{mx=31}{\mathbb{N}},\ \htmlData{mx=18}{(\htmlData{mx=17}{\htmlData{mx=16}{t} + 1024}) \bmod 32} \mathrel{\htmlData{mx=21}{=}} \htmlData{mx=20}{\htmlData{mx=19}{t} \bmod 32} \mathbin{\htmlData{mx=30}{\land}} \htmlData{mx=25}{\htmlData{mx=24}{\frac{\htmlData{mx=23}{\htmlData{mx=22}{t} + 1024}}{32}} \bmod 32} \mathrel{\htmlData{mx=29}{=}} \htmlData{mx=28}{\htmlData{mx=27}{\frac{\htmlData{mx=26}{t}}{32}} \bmod 32}}\right) \\ & \htmlData{mx=0}{\land} \left(\htmlData{mx=46}{\forall t \in \htmlData{mx=45}{\mathbb{N}},\ \htmlData{mx=34}{\htmlData{mx=33}{t} \bmod 32} \mathrel{\htmlData{mx=35}{=}} 0 \mathbin{\htmlData{mx=40}{\land}} \htmlData{mx=38}{\htmlData{mx=37}{\frac{\htmlData{mx=36}{t}}{32}} \bmod 32} \mathrel{\htmlData{mx=39}{=}} 0 \mathrel{\htmlData{mx=44}{\iff}} \htmlData{mx=42}{\htmlData{mx=41}{t} \bmod 1024} \mathrel{\htmlData{mx=43}{=}} 0}\right) \\ & \htmlData{mx=0}{\land} \left(\htmlData{mx=62}{\forall t \in \htmlData{mx=61}{\mathbb{N}},\ 0 \mathrel{\htmlData{mx=48}{<}} \htmlData{mx=47}{t} \mathrel{\htmlData{mx=60}{\implies}} \htmlData{mx=50}{\htmlData{mx=49}{t} \bmod 32} \mathrel{\htmlData{mx=51}{=}} 0 \mathrel{\htmlData{mx=59}{\implies}} \htmlData{mx=54}{\htmlData{mx=53}{\frac{\htmlData{mx=52}{t}}{32}} \bmod 32} \mathrel{\htmlData{mx=55}{=}} 0 \mathrel{\htmlData{mx=58}{\implies}} 1024 \mathrel{\htmlData{mx=57}{\leq}} \htmlData{mx=56}{t}}\right) \\ & \htmlData{mx=0}{\land} \left(\htmlData{mx=79}{\forall t \in \htmlData{mx=78}{\mathbb{N}},\ \htmlData{mx=65}{\frac{\htmlData{mx=64}{\htmlData{mx=63}{t} + 32}}{32}} \mathrel{\htmlData{mx=69}{=}} \htmlData{mx=68}{\htmlData{mx=67}{\frac{\htmlData{mx=66}{t}}{32}} + 1} \mathbin{\htmlData{mx=77}{\land}} \htmlData{mx=72}{\frac{\htmlData{mx=71}{\htmlData{mx=70}{t} + 1024}}{1024}} \mathrel{\htmlData{mx=76}{=}} \htmlData{mx=75}{\htmlData{mx=74}{\frac{\htmlData{mx=73}{t}}{1024}} + 1}}\right) \\ & \htmlData{mx=0}{\land} \left(\htmlData{mx=81}{\frac{\htmlData{mx=80}{1024}}{32}} \mathrel{\htmlData{mx=82}{=}} 32 \mathbin{\htmlData{mx=86}{\land}} \htmlData{mx=84}{\frac{\htmlData{mx=83}{1024}}{1024}} \mathrel{\htmlData{mx=85}{=}} 1\right) \\ & \htmlData{mx=0}{\land} (\htmlData{mx=97}{\forall s, t \in \htmlData{mx=96}{\mathbb{N}},\ \htmlData{mx=87}{s} \mathrel{\htmlData{mx=89}{\leq}} \htmlData{mx=88}{t} \mathrel{\htmlData{mx=95}{\implies}} 1024 \mathrel{\htmlData{mx=91}{\leq}} \htmlData{mx=90}{s} \mathrel{\htmlData{mx=94}{\implies}} 1024 \mathrel{\htmlData{mx=93}{\leq}} \htmlData{mx=92}{t}}) \end{aligned}
What the notation means · or point at any symbol
∀For all
The statement after the comma holds for every t. (∀ t : ℕ, t % 32 + 32 * ((t / 32) % 32) …)
NNatural numbers
The natural numbers 0, 1, 2, …. In Lean they start at 0. (ℕ)
modRemainder
The remainder when t is divided by 32. (t % 32)
+Addition
t % 32 plus 32 · (t/32 % 32). (t % 32 + 32 * ((t / 32) % 32))
=Equality
t % 32 + 32 · (t/32 % 32) + 1024 · (t/1024) and t are the same. (t % 32 + 32 * ((t / 32) % 32) + 1024 * …)
·Multiplication
32 times t/32 % 32. (32 * ((t / 32) % 32))
a/bDivision
t divided by 32. In Lean, dividing by 0 gives 0. (t / 32)
∧And
Both hold: (t + 1024) % 32 = t % 32, and (t + 1024)/32 % 32 = t/32 % 32. ((t + 1024) % 32 = t % 32 ∧ ((t + 1024) …)
⟺If and only if
t % 32 = 0 ∧ t/32 % 32 = 0 holds exactly when t % 1024 = 0 holds. ((t % 32 = 0 ∧ (t / 32) % 32 = 0) ↔ t % …)
<Less than
0 is strictly smaller than t. (0 < t)
⟹Implies
If t/32 % 32 = 0, then 1024 ≤ t. (Between types, A → B is the type of functions from A to B.) ((t / 32) % 32 = 0 → 1024 ≤ t)
≤At most
1024 is less than or equal to t. (1024 ≤ t)
(x : T)As natural numbers
1024 read as an element of natural numbers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. ((1024 : ℕ))

Model t as the number of small pulses. Vertical phase t mod 32, horizontal phase floor(t/32) mod 32, great-cycle count floor(t/1024). Prove reconstruction, periodicity, exact returns, no earlier positive return, pulse increments, 32 middle events per great cycle, and persistence of the explicitly chosen golden latch 1024 <= t. Periodicity is only of phases, not of the irreversible colour. Models the user's stated one-full-ring-turn-per-great-pulse variant.

How it was proved

Proved
4 October 2026
By
Ajax
Checked by
Lean's kernel (Lean 4.33.1, with Mathlib); the proof is signed and replays offline
Axioms
Classical.choice, Quot.sound, propext
Proof
36 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.

More proved statements