Nested Colored-Dot Symbol System: An Information-Theoretic and Semantic Alternative to QR Codes

This article is a re-publication of Rei-AIOS Paper 112 for the dev.to community.
The canonical version with full reference list is in the permanent archives below:

• Zenodo (DOI, canonical): https://doi.org/10.5281/zenodo.19643419
• Internet Archive: https://archive.org/details/rei-aios-paper-112-1776524696634
• Harvard Dataverse: https://doi.org/10.7910/DVN/KC56RY
• GitHub source (private): https://github.com/fc0web/rei-aios Author: Nobuki Fujimoto (@fc0web) · ORCID 0009-0004-6019-9258 · License CC-BY-4.0 ---

Authors: Nobuki Fujimoto (ORCID 0009-0004-6019-9258), Claude Code (Lean 4 formalization, TypeScript reference implementation)
Date: 2026-04-18
Status: DRAFT — not yet peer-reviewed. Proposal paper + Lean 4 formal foundation.
License: CC-BY-4.0
Repository: fc0web/rei-aios (private), reference files data/lean4-mathlib/CollatzRei/LayerDNestedDot.lean, src/axiom-os/layer-d-nested-dot.ts, scripts/{encode,decode}-nested-dot-*.ts.

Abstract

QR codes (Denso Wave 1994) encode up to 23,624 data bits in a 177×177 binary grid, with four fixed error-correction levels and a rigid byte-stream payload model. We propose a complementary 2D symbol system — the Nested Colored-Dot (NestedDot) — whose payload is a recursively structured dot carrying, at each leaf, an 8-valued logic label (D-FUMT₈) and a 24-bit RGB color on two orthogonal semantic axes. Each leaf encodes 43 bits (3 + 24 + 16), and a depth-d NestedDot with balanced fanout k carries ≈ k^(d−1) × 43 bits of payload. We formalize the type, the depth and bitSize functions, and three QR-capacity exceedance theorems (depth-2 flat with 401 leaves beats QR v40 L; depth-3 balanced 100×100 beats 18× QR v40 L) in Lean 4 with zero sorry. A reference TypeScript encoder/decoder pipeline (PNG 24-bit RGB) round-trips 12 sample structures losslessly (36/36 assertions pass). We position NestedDot as not a replacement for QR — readability, standardization and error-correction maturity still favor QR — but as a mathematically distinct symbol system that trades rigid payload for compositional, multi-scale semantics.

Keywords: 2D symbology, QR code, information density, Lean 4, D-FUMT₈ 8-valued logic, RGB color, nested inductive types, symbol design.

1. Introduction

1.1 QR codes as a baseline

QR codes (ISO/IEC 18004) were introduced by Denso Wave in 1994. At their largest standard configuration (Version 40, Error Correction Level L), a QR code stores 23,624 data bits in a 177×177 module grid, with 4 fixed error-correction levels (L/M/Q/H) based on Reed–Solomon over GF(256). The payload is a flat byte stream (optionally with mode indicators for numeric/alphanumeric/byte/kanji). Two design choices underlie the QR model:

1. Binary module grid — each cell is 0 or 1 (dark or light).
2. Flat linear payload — the data bits are a single byte stream; no structural hierarchy in the payload semantics.

1.2 Motivation for a nested, colored alternative

The present work is part of the Rei-AIOS project (Fujimoto 2024–2026), a TypeScript + Lean 4 research system that explores 8-valued logic (D-FUMT₈: TRUE, FALSE, BOTH, NEITHER, INFINITY, ZERO, FLOWING, SELF) as a unifying structure across mathematics, linguistics, and symbol design. In earlier work (Paper 33, Paper 69, Paper 110) we formalized Braille-D-FUMT₈ as a 6-dot × 8-logic encoding. Paper 110 rigorously compared it against modern learned embeddings (CLIP, BERT) and concluded that the two families are complementary, not competing.

The Layer D of the Fujimoto Infinite-Dot Theory (FIDT) extends the earlier flat Layer B in three ways:

1. Color: each dot carries a 24-bit RGB value, orthogonal to the D-FUMT₈ logic axis.
2. Recursion: a dot is a container — it may hold a list of (coordinate, child-dot) pairs, and each child is itself a NestedDot.
3. Coordinate: each internal point has a 2D grid position (Fin 256 × Fin 256).

Paper 33, 69 and 110 addressed Layer C (discrete Braille-style) and Layer B (flat DFumt8 × DimensionValue algebra). The present paper formalizes Layer D for the first time.

1.3 Research question

Can a nested-color symbol system match or exceed QR's raw information capacity in a bounded 2D region while providing structural-semantic benefits that flat binary grids cannot?

We answer yes for raw bit capacity, with honest caveats about readability, error correction, and standardization.

2. The NestedDot Formalization (Lean 4)

The full Lean 4 file is data/lean4-mathlib/CollatzRei/LayerDNestedDot.lean, built against Mathlib v4.27.0, zero sorry.

2.1 Core types

inductive DFumt8 : Type
  | TRUE | FALSE | BOTH | NEITHER | INFINITY | ZERO | FLOWING | SELF

abbrev RGB := Fin 16777216                -- 2^24

structure ColoredDot where
  logic : DFumt8
  color : RGB

structure Coord where
  x : Fin 256
  y : Fin 256

inductive NestedDot : Type
  | leaf     (cd : ColoredDot) (co : Coord)           : NestedDot
  | compound (outer : ColoredDot)
             (points : List (Coord × NestedDot))       : NestedDot

2.2 depth and bitSize (mutual recursion)

mutual
  def NestedDot.depth : NestedDot → Nat
    | .leaf _ _ => 1
    | .compound _ pts => 1 + NestedDot.depthList pts
  def NestedDot.depthList : List (Coord × NestedDot) → Nat
    | [] => 0
    | (_, d) :: rest => max (NestedDot.depth d) (NestedDot.depthList rest)
end

def LEAF_BITS  : Nat := 43     -- 3 (DFumt8) + 24 (RGB) + 16 (Coord)
def COORD_BITS : Nat := 16

mutual
  def NestedDot.bitSize : NestedDot → Nat
    | .leaf _ _ => LEAF_BITS
    | .compound _ pts => LEAF_BITS + NestedDot.bitSizeList pts
  def NestedDot.bitSizeList : List (Coord × NestedDot) → Nat
    | [] => 0
    | (_, d) :: rest => COORD_BITS + NestedDot.bitSize d + NestedDot.bitSizeList rest
end

2.3 Closed-form formula (proved)

For makeFlatLeaves n (a list of n identical leaves) we have

theorem bitSizeList_flat (n : Nat) :
    NestedDot.bitSizeList (makeFlatLeaves n) = n * (COORD_BITS + LEAF_BITS)

theorem bitSize_flat_compound (n : Nat) :
    (NestedDot.compound ⟨.TRUE, 0⟩ (makeFlatLeaves n)).bitSize
      = LEAF_BITS + n * (COORD_BITS + LEAF_BITS)

Substituting constants: bitSize = 43 + 59 n.

2.4 QR-exceedance theorems (zero sorry)

def QR_V1_L_BITS  : Nat := 152
def QR_V10_L_BITS : Nat := 2192
def QR_V40_L_BITS : Nat := 23624

theorem depth2_flat_3_exceeds_qr_v1L   : QR_V1_L_BITS < …(makeFlatLeaves 3).bitSize
theorem depth2_flat_37_exceeds_qr_v10L : QR_V10_L_BITS < …(makeFlatLeaves 37).bitSize
theorem depth2_flat_401_exceeds_qr_v40L:
    QR_V40_L_BITS < (NestedDot.compound ⟨.TRUE, 0⟩ (makeFlatLeaves 401)).bitSize
theorem depth3_100x100_exceeds_qr_v40L_18x :
    18 * QR_V40_L_BITS
      < (NestedDot.compound ⟨.TRUE, 0⟩ (makeCompoundListDepth2 100 100)).bitSize

Each is proved by rewriting the closed form and closing with decide.

2.5 Layer B ↪ Layer D embedding

The earlier flat Layer B InfiniteDot (Paper 110 §2, Problem008FDAFIDT.lean) injects into Layer D via

def embedLayerB (v : DFumt8) : NestedDot :=
  .leaf ⟨v, 0⟩ ⟨0, 0⟩

theorem embedLayerB_injective : Function.Injective embedLayerB

so every theorem about Layer B lifts to Layer D on the leaf sub-type.

3. Empirical bit-density vs QR

Reference implementation: src/axiom-os/layer-d-nested-dot.ts mirrors the Lean depth / bitSize definitions verbatim. Benchmark test: test/wd2-density-vs-qr-test.ts (22/22 assertions pass).

Minimum leaf counts to exceed each QR level (depth 2 flat, exactly-tight):

• QR v1 L (152 bit): 2 leaves → 161 bit (1.06×)
• QR v10 L (2,192 bit): 37 leaves → 2,226 bit (1.02×)
• QR v25 L (10,208 bit): 173 leaves → 10,250 bit (1.004×)
• QR v40 L (23,624 bit): 400 leaves → 23,643 bit (1.0008×)

The tightness of these counts follows from the linearity of bitSize = 43 + 59 n.

4. Encoder / decoder pipeline and round-trip

4.1 Layout

Each NestedDot row begins with a 4-pixel header (RGB 24-bit pixels):

• Leaf header (4 px): [color], [logic | 0x55 | 0xAA], [coord.x | coord.y | 0], [0 | 0 | 0].
• Compound header (4 px): [outer.color], [logic | 0x33 | 0xCC], [k_hi | k_mid | k_lo], [slot_w_hi | slot_w_lo | slot_h].

Below a compound header, children are laid out in a ⌈√k⌉ × ⌈k/⌈√k⌉⌉ grid of uniform slot_w × slot_h tiles.

The full encoder is scripts/encode-nested-dot-to-png.ts and decoder is scripts/decode-png-to-nested-dot.ts, both built on pngjs for PNG I/O.

4.2 Round-trip verification

test/wd4-roundtrip-test.ts exercises the full encode → PNG → decode pipeline on 12 sample NestedDots: flat compounds of 10 / 50 / 200 / 401 leaves, depth-3 (5×5) / (10×10), diverse-color 16 / 64 / 256 leaves, empty compound, single leaf, and a mixed leaf+compound sibling case. All 36 assertions pass — every sample round-trips with structural equality (same tree shape, same logic labels, same colors, same coordinates).

5. Five-axis comparison: NestedDot vs QR

6. Honest limitations

6.1 No error correction yet

The current NestedDot encoder writes a raw 24-bit RGB pixel grid to PNG with no error-correction layer. A single bit flip in a leaf byte mutates either its logic label, its color, or its marker — the decoder may then silently mis-interpret a compound as a leaf or vice versa. A Reed–Solomon layer (or any ECC scheme compatible with the inductive structure) is required before NestedDot can be considered for any real-world encoding task.

6.2 Physical readability

PNG is a screen/file format, not a print/scan format. QR codes are specifically engineered for tolerance to rotation, perspective, lighting, and print-quality degradation. Any attempt to print and rescan a NestedDot would require a detection grid analogous to QR's three corner finder patterns and timing lines. This paper does not address physical readability.

6.3 Overhead per leaf

Each NestedDot leaf encodes 43 bits of payload but occupies 4 × 24 = 96 pixel bits in the reference encoder. The encoding density is ~45% — worse than QR's effective density after ECC. A tighter binary encoding (bit-packing logic + color + coord contiguously) could recover this, at the cost of decoder complexity.

6.4 No claim of replacement

This paper explicitly does not claim NestedDot supersedes QR. The mature QR ecosystem — print/scan robustness, standardization, consumer-device support, Reed–Solomon ECC — is out of scope here. NestedDot is proposed as a mathematically distinct complementary symbol system whose natural niche is applications where structural semantics (nested containers, multi-axis labels) are more valuable than rigidly-bounded byte streams.

7. Positioning: what NestedDot is not, and is

Not: a consumer replacement for QR. Not a print/scan standard. Not a standalone error-correcting code.

Is: (a) a formal demonstration that nested inductive structures with orthogonal color + logic axes can exceed QR's raw information capacity in a bounded region; (b) a constructive Lean 4 foundation for reasoning about such structures; (c) an extension of FIDT Layer B to a compositional Layer D with explicit color semantics; (d) a proposal for future symbol systems aimed at structural payloads (e.g. representing small trees, nested records, typed hierarchies) rather than flat byte streams.

8. Relation to prior work

• Paper 33 (Braille-DFumt8, 2024): 6-dot Braille cells re-interpreted through DFumt8 8-valued logic. Paper 33 is Layer C (discrete finite cell).
• Paper 69 (Schnorr + DFumt8, 2026): independent match with Schnorr 1971 random-logic hierarchy.
• Paper 110 (Braille-DFumt8 vs CLIP/BERT, 2026): rigorous comparison with modern learned embeddings; establishes Braille-DFumt8 as complementary not competing. Layer B InfiniteDot is formalized in Problem008FDAFIDT.lean.
• Paper 111 (Rei vs Santana, 2026): Collatz topological/ergodic comparison; MANDALA E31 lens.
• Present paper (112): Layer D NestedDot — first formalization of the nested/colored/coordinated layer.

9. Reproducibility

All files below exist in the repository and are sufficient to reproduce all theorems and benchmarks:

• data/lean4-mathlib/CollatzRei/LayerDNestedDot.lean — Lean 4 formalization (zero sorry, zero new axioms).
  • Build: cd data/lean4-mathlib && lake build CollatzRei.LayerDNestedDot
• src/axiom-os/layer-d-nested-dot.ts — TypeScript mirror of depth, bitSize, and balanced builders.
• test/wd2-density-vs-qr-test.ts — 22/22 assertions benchmarking depth 1–4 vs QR v1 / v10 / v25 / v40 L.
  • Run: npx tsx test/wd2-density-vs-qr-test.ts
• scripts/encode-nested-dot-to-png.ts — PNG encoder.
• scripts/decode-png-to-nested-dot.ts — PNG decoder.
• test/wd4-roundtrip-test.ts — 36/36 assertions, 12 round-trip samples.
  • Run: npx tsx test/wd4-roundtrip-test.ts

10. Future work

1. Reed–Solomon or LDPC ECC layer compatible with the inductive structure.
2. Finder pattern & perspective correction for print/scan deployment.
3. Bit-packed encoding to approach 43/48 density (one leaf in ~2 pixels rather than 4).
4. Standards engagement if and when an application niche justifies it.
5. Mutual independence of depth and breadth — is there a meaningful minimum-cell representation for each depth?
6. Layer E (draft idea): extend NestedDot with a continuous semantic-embedding field on top of each ColoredDot, bridging to Paper 110's CLIP comparison.

Paper 112 draft prepared 2026-04-18 by Claude Code under Nobuki Fujimoto's direction, in the Rei-AIOS research programme. Corrections and collaborations welcome at: https://note.com/nifty_godwit2635 / fc0web@github / fc2webb@gmail.com.