Provedmandalic-clocksymbolic-encodingidentifiability

Mandalic clock: unrestricted positive pulse weights can encode any positive target

\begin{aligned} & \left(\right. \htmlData{mx=1}{\forall} y \in \htmlData{mx=2}{\mathbb{R}}, \\ & \quad 0 \mathrel{\htmlData{mx=5}{<}} \htmlData{mx=4}{y} \\ & \quad \htmlData{mx=3}{\implies} \htmlData{mx=6}{\exists} a, b, c \in \htmlData{mx=7}{\mathbb{R}}, \\ & \quad \quad 0 \mathrel{\htmlData{mx=10}{<}} \htmlData{mx=9}{a} \\ & \quad \quad \htmlData{mx=8}{\land} 0 \mathrel{\htmlData{mx=12}{<}} \htmlData{mx=11}{b} \\ & \quad \quad \htmlData{mx=8}{\land} 0 \mathrel{\htmlData{mx=14}{<}} \htmlData{mx=13}{c} \\ & \quad \quad \htmlData{mx=8}{\land} \htmlData{mx=21}{\htmlData{mx=19}{\htmlData{mx=16}{1024\htmlData{mx=15}{a}} + \htmlData{mx=18}{32\htmlData{mx=17}{b}}} + \htmlData{mx=20}{c}} \mathrel{\htmlData{mx=23}{=}} \htmlData{mx=22}{y} \left.\right) \\ & \htmlData{mx=0}{\land} \left(\htmlData{mx=36}{\htmlData{mx=32}{\htmlData{mx=27}{\htmlData{mx=24}{1024} \cdot \left(\htmlData{mx=26}{\frac{\htmlData{mx=25}{\pi}}{1024}}\right)} + \htmlData{mx=31}{32\left(\htmlData{mx=30}{\frac{\htmlData{mx=29}{\htmlData{mx=28}{\pi}^{2}}}{32}}\right)}} + \htmlData{mx=35}{4 \cdot \htmlData{mx=34}{\htmlData{mx=33}{\pi}^{3}}}} \mathrel{\htmlData{mx=45}{=}} \htmlData{mx=44}{\htmlData{mx=40}{\htmlData{mx=37}{\pi} + \htmlData{mx=39}{\htmlData{mx=38}{\pi}^{2}}} + \htmlData{mx=43}{4 \cdot \htmlData{mx=42}{\htmlData{mx=41}{\pi}^{3}}}}\right) \end{aligned}

What the notation means · or point at any symbol

∀For all: The statement after the comma holds for every y. (∀ y : ℝ, 0 < y → ∃ a b c : ℝ, 0 < a ∧ 0…)
<Less than: 0 is strictly smaller than y. (0 < y)
⟹Implies: If 0 < y, then ∃ a, b, c, 0 < a ∧ (0 < b ∧ (0 < c ∧ 1024 · a + 32 · b + c…. (Between types, A → B is the type of functions from A to B.) (0 < y → ∃ a b c : ℝ, 0 < a ∧ 0 < b ∧ 0 …)
∃There exists: At least one a, b, c makes the statement after the comma true. (∃ a b c : ℝ, 0 < a ∧ 0 < b ∧ 0 < c ∧ 10…)
RReal numbers: The real numbers: every point on the number line. (ℝ)
∧And: Both hold: 0 < c, and 1024 · a + 32 · b + c = y. (0 < c ∧ 1024 * a + 32 * b + c = y)
·Multiplication: 1024 times a. (1024 * a)
+Addition: 1024 · a plus 32 · b. (1024 * a + 32 * b)
=Equality: 1024 · a + 32 · b + c and y are the same. (1024 * a + 32 * b + c = y)
(x : T)As real numbers: 1024 read as an element of real numbers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. ((1024 : ℝ))
πPi: The ratio of a circle's circumference to its diameter, ≈ 3.14159. (Real.pi)
a/bDivision: π divided by 1024. In Lean, dividing by 0 gives 0. (Real.pi / 1024)
aᵇPower: π raised to the power 2. (Real.pi ^ 2)

theorem mandalic-clock-positive-decoder-underdetermination :
    (∀ y : ℝ, 0 < y → ∃ a b c : ℝ, 0 < a ∧ 0 < b ∧ 0 < c ∧ 1024 * a + 32 * b + c = y) ∧ ((1024 : ℝ) * (Real.pi / 1024) + 32 * (Real.pi ^ 2 / 32) + 4 * Real.pi ^ 3 = Real.pi + Real.pi ^ 2 + 4 * Real.pi ^ 3)

One great cycle has channel counts 1024 small, 32 middle, 1 great. For every positive real y construct positive weights a=b=c=y/1057 such that 1024a+32b+c=y. Separately verify that weights π/1024, π²/32, 4π³ realise the proposed polynomial exactly. This distinguishes constructive symbolic encoding from unique physical prediction, without claiming all physical decoders must be arbitrary.

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: 26 lines of Lean

Mandalic clock: unrestricted positive pulse weights can encode any positive target

How it was proved

More proved statements