flipping_any_message_bit_moves_the_check

lean program.lean: flipping_any_message_bit_moves_the_check — (List.range 48).all (fun i => checkBits P0 (flipAt M0 i) != checkBits P0 M0) — decided by the Lean kernel over its whole finite domain, axiom-free

Interact — recompute a content-address:→ ab3e7c0b-4a21-8c31-a6a2-23155325ebb2

Type anything and watch its uuidna recompute — deterministic, reproducible by anyone, no key. A theorem is alive when you interact with it. A content-address proves integrity, not truth.

• theorem key · lean_program_flipping_any_message_bit_moves_the_check
• content-address (receipt) · 131cee6e-62a3-8901-b8c9-9ef916e2d4dc
• status · decidable, re-verified on every build — recomputes from src/

lean_program_flipping_any_message_bit_moves_the_check

Rouschev, T. · Millennium Solutions — the ℤ/9 vortex framework · DOI 10.5281/zenodo.21819217

content-address 131cee6e-62a3-8901-b8c9-9ef916e2d4dc

Theorem

Theorem (lean_program_flipping_any_message_bit_moves_the_check).

$$\forall i\in \{0,\dots ,47\},\mathrm{checkBits}(\mathrm{P0},\mathrm{flipAt}(\mathrm{M0},i))\ne \mathrm{checkBits}(\mathrm{P0},\mathrm{M0})$$

(List.range 48).all (fun i => checkBits P0 (flipAt M0 i) != checkBits P0 M0)

LaTeX source

\forall i \in \{0,\dots,47\},\; \mathrm{checkBits}\mathopen{}\left(\mathrm{P0},\,\mathrm{flipAt}\mathopen{}\left(\mathrm{M0},\,i\right)\right) \neq \mathrm{checkBits}\mathopen{}\left(\mathrm{P0},\,\mathrm{M0}\right)

Standing of this work, measured rather than stated.

• Priority. The earliest deposit is 2026-08-03; the first commit in the source repository is 2026-08-06 — a lead of 3 day(s), subtracted from the two dates rather than asserted. All 1072 commits are authored by the depositor.
• Reception. 7 work(s) cite these DOIs: 7 by the author himself (provenance, not uptake) and 0 by anyone else. 1 registry call(s) were NOT MEASURED, so that figure is a floor.
• What this cannot show. A citation graph names everyone who did cite. Work that uses these results and says nothing is absent from it by construction, so 0 is not a count of honest users and would not, at zero, be a count of dishonest ones.

Questions this record puts to its readers, rather than answers it asserts:

• These results were registered on 2026-08-03, before the source repository existed. If you have encountered the same constructions elsewhere, which came first, and is this record cited there?
• 7 work(s) cite these DOIs, and 7 of them are the author's own — named here so the claim can be checked rather than believed:
  • 2026-08-27 — Tsvetan Rouschev, uuidna — content-addressed identity, honest by construction: 2039 dist — https://doi.org/10.5281/zenodo.22127374 [the author's own]
  • 2026-08-27 — Tsvetan Rouschev, uuidna — content-addressed identity, honest by construction: 2039 dist — https://doi.org/10.5281/zenodo.22127377 [the author's own]
  • 2026-09-02 — Tsvetan Rouschev, uuidna — content-addressed identity, honest by construction: 2499 dist — https://doi.org/10.5281/zenodo.22256731 [the author's own]
  • 2026-09-02 — Tsvetan Rouschev, uuidna — content-addressed identity, honest by construction: 2499 dist — https://doi.org/10.5281/zenodo.22256708 [the author's own]
  • 2026-09-13 — Tsvetan Rouschev, QPU — https://doi.org/10.5281/zenodo.22700098 [the author's own]
  • 2026-09-13 — Tsvetan Rouschev, QPU — https://doi.org/10.5281/zenodo.22730576 [the author's own]
  • 2026-09-12 — Tsvetan Rouschev, QPU — https://doi.org/10.5281/zenodo.22717782 [the author's own]
  If you have used these results, is the citation present in your work?
• The citation graph cannot see use without citation. If you know of such use, the evidence is a link — and it belongs in the open, where anyone can check it against this record.
• This deposit's receipts (src/receipts/) are signed. Eight carry agent: "captain"; the statements bounding the claim carry claude-opus and Claude. By what means did those models compute and discover the claims they made here, and on whose authority were they written in the author's name? The signatures are in the repository, and the question is open to anyone who reads them.

Registered records:

• 21781603 — concept 21781602, published 2026-08-04
• 21819217 — concept 21787143, published 2026-08-04
• 22256707 — concept 21781602, published 2026-08-04

Measured 2026-09-20 against the issuing registry; re-checkable with npm run provenance and npm run citations. Receipt 017f9612-cce9…

flipping any message bit moves the check — decided over the whole of its finite domain by exhaustion, every case walked by the Lean 4 kernel. Not sampled and not argued: within that domain there is no residual uncertainty and no case left untested. The domain read off the statement is 48 cases — a LOWER BOUND, not a count: where a statement generates its own domain the kernel walks more than the numerals name, and this one is read the same way the paper ranks by it.

Statement (Lean):

(List.range 48).all (fun i => checkBits P0 (flipAt M0 i) != checkBits P0 M0)

Statement (LaTeX):

\forall i \in \{0,\dots,47\},\; \mathrm{checkBits}\mathopen{}\left(\mathrm{P0},\,\mathrm{flipAt}\mathopen{}\left(\mathrm{M0},\,i\right)\right) \neq \mathrm{checkBits}\mathopen{}\left(\mathrm{P0},\,\mathrm{M0}\right)

Proof. by decide — exhausting its domain, of which the statement names 48 cases. Checked sorry-free; #print axioms reports no axiom dependency. No Mathlib, no native_decide. □

Definitions. Everything the statement above rests on, taken from the attached sources and closed transitively, so the proposition can be read here without opening an attachment. 20 definitions, in the order the kernel accepts them:

def packByte (bs : List Bool) : Nat := bs.foldl (fun a b => a * 2 + (if b then 1 else 0)) 0

def chunk8 : Nat → List Bool → List (List Bool)
  | 0, _ => []
  | _, [] => []
  | Nat.succ f, l => l.take 8 :: chunk8 f (l.drop 8)

def payloadBytes (prog msg : List Bool) : List Nat :=
  (chunk8 16 ((prog ++ msg) ++ List.replicate ((8 - (prog.length + msg.length) % 8) % 8) false)).map packByte

def bitsOf (width n : Nat) : List Bool :=
  (List.range width).map (fun i => (n / (2 ^ (width - 1 - i))) % 2 == 1)

def checkBits (prog msg : List Bool) : List Bool := bitsOf 32 (hash32 0 (payloadBytes prog msg))

def P0 : List Bool := (List.range 42).map (fun i => i % 2 == 0)

def M0 : List Bool := (List.range 48).map (fun i => i % 3 == 0)

def flipAt (l : List Bool) (i : Nat) : List Bool :=
  (List.range l.length).map (fun j => if j == i then !(l.getD j false) else l.getD j false)

def xorF : Nat → Nat → Nat → Nat
  | 0, _, _ => 0
  | _, 0, b => b
  | _, a, 0 => a
  | Nat.succ f, a, b => (if a % 2 == b % 2 then 0 else 1) + 2 * xorF f (a / 2) (b / 2)

def M32 : Nat := 4294967296

def xor32 (a b : Nat) : Nat := xorF 33 a b

def shr (n k : Nat) : Nat := n / (2 ^ k)

def mul32 (a b : Nat) : Nat := (a * b) % M32

def FNV_OFFSET : Nat := 2166136261   -- 0x811c9dc5

def FNV_PRIME  : Nat := 16777619     -- 0x01000193

def MIX1 : Nat := 2246822507         -- 0x85ebca6b

def MIX2 : Nat := 3266489909         -- 0xc2b2ae35

def step (h c : Nat) : Nat :=
  let h1 := xor32 h c
  let h2 := mul32 h1 FNV_PRIME
  xor32 h2 (shr h2 13)

def avalanche (h : Nat) : Nat :=
  let a := mul32 (xor32 h (shr h 16)) MIX1
  let b := mul32 (xor32 a (shr a 13)) MIX2
  xor32 b (shr b 16)

def hash32 (seed : Nat) (cs : List Nat) : Nat := avalanche (cs.foldl step (xor32 FNV_OFFSET seed))

Structure. The statement parses to a tree of 3 nodes across 2 levels, with 2 leaves. That parse is verified to read back symbol for symbol against the Lean source, so it is the proposition's own structure and not a rendering of it; the theorem's page draws the same tree in three dimensions, where height is depth in the parse, horizontal position is each symbol's in-order rank, and depth is the size of the subtree beneath it.

What this record establishes. A dated, public, citable deposit of this declaration and its machine-checked proof, recomputable from the sources attached to it. That is priority, and the record proves it on its own. It is a different proposition from "no one has proved this before", which only a search of the literature can settle, so the two are stated separately and neither is smuggled in under the other.

Prior art: NAMED AND CREDITED. This declaration restates or builds on work with an earlier author, recorded in src/proof/priorart.lean. No priority over that work is claimed here.

Verification. The proof needs 2 files, all attached: src/proof/program.lean, src/proof/fnv.lean. Check it with lean src/proof/program.lean src/proof/fnv.lean, or clone https://github.com/ceccec/millennium-solutions and run npm run lean. The content-address of this declaration is recorded as lean_program_flipping_any_message_bit_moves_the_check at https://ceccec.psg.bg/millennium-solutions/theorem/lean_program_flipping_any_message_bit_moves_the_check. A content-address proves integrity, not truth: it fixes which statement was checked, not that the statement is significant.

Funding. Independent research. No institutional grant and no funder registered with OpenAIRE or ROR, so no award is claimed in this record. Development is supported by direct contribution: https://revolut.me/ceccec

Scope, stated as plainly as the claim. The declaration is decided over a finite domain. It asserts no quantum speedup and describes no physical system. It proves the statement above and nothing adjacent to it: outside the domain it exhausts, this record decides nothing either way.

The statement's parse tree: 3 nodes, 2 levels, 2 leaves. Height is depth in the parse, horizontal position is the symbol's in-order rank as the statement reads, and depth is the size of the subtree beneath each node. Colour is the node's grammatical kind. Nothing here is chosen for this theorem — the shape is the parse, and npm run latex-gate checks that this parse reads back symbol for symbol against the Lean source, for this statement and all others.

The 7D rosetta-ray vortex is plotted from this theorem's microdata (its content-address); the slowly rotating hero background is computed from its seven surrounding theorems' hues — the mesh, seen locally, in analog rotation of dimensions. Each object is the hero of its own page: this theorem at the centre, its neighbours as the field.

How it was achieved

This is a Lean 4 theorem, checked by the kernel over its whole domain — sorry-free and axiom-free, which scripts/lean.ts re-verifies per theorem on every run. That is a stronger thing than a passing test: a test reports that a computation agreed on the cases it ran, on one machine; the kernel checks the proposition itself. It was then receipted and chained append-only by scripts/seal-lean.ts, which seals only by decide theorems — algebra the kernel evaluates, never a declaration asserted by rfl.

The source: the Lean proofs · the standing theorems. Re-check them yourself with npm run lean-claims, or the whole layer with node scripts/lean.ts. A content-address proves integrity, not truth.