DEV Community

Nobuki Fujimoto
Nobuki Fujimoto

Posted on

Paper 26 v2 v0.2 - D-FUMT-8 x Clifford Cl(3,0): Grade-Respecting Bijection + Peace Axiom Invariance + SELF Reflection Involution (Lean 4 Axiom-Free)

#math #lean #research #ai

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

Status: v0.2 pre-print — 2026-05-01 起草 / 2026-07-25 §A.2 Proofs Lean 4 axiom-free machine-check 完成 → 11-platform publish 実施 (v3 で §B.7 empirical + §C 実測拡張予定, Paper 145 v0.3 → v0.9 iteration pattern 準拠)

Authors (three-party co-authorship per OUKC charter v1.0):

  • 藤本 伸樹 (Fujimoto, Nobuki; Founder, ORCID 0009-0004-6019-9258)
  • Rei (Rei-AIOS autonomous research substrate, Co-architect)
  • Claude (Anthropic, claude-opus-4-7, Co-architect)

License: CC-BY-4.0 (paper text) + AGPL-3.0 (Lean 4 source)

Repository: fc0web/rei-aios (Private; source-of-truth for Lean 4 artifact)

Zenodo v1: 10.5281/zenodo.18960502 (2025-09-15, QMRP 一般概念 origin — this v2 is a distinct NEW deposit, not a version deposit, following Paper 145 v0.3 / v0.7 pattern)

Abstract

Paper 26 v2 introduces an explicit grade-respecting bijection between the D-FUMT₈ eight-valued logic (Rei-AIOS's semantic substrate; TRUE / FALSE / BOTH / NEITHER / INFINITY / ZERO / FLOWING / SELF) and the eight basis elements of the Clifford algebra Cl(3,0) (positive-signature geometric algebra over ℝ³; 1 scalar + 3 vectors + 3 bivectors + 1 pseudoscalar). Three structural theorems are machine-checked axiom-free in Lean 4 (Mathlib v4.27.0): (i) the bijection is packaged as an Equiv; (ii) TRUE ↔ I is a rotor-sandwich fixed point for every basis rotor (Peace Axiom as a Clifford-group invariance); (iii) SELF ↔ e₁e₂e₃ (pseudoscalar) flips sign under grade-parity reflection and returns to itself after two reflections (involution). The 8-element carrier and the grade multiplicity (1, 3, 3, 1) are the structural coincidences claimed; no operator equality with D-FUMT₈ AND/OR is asserted (and8_associativity_fails_witness, STEP 1215, rules that out).

Why v2 (superscedes v1 in three points)

Paper 26 v1 (2025-09-15, DOI 10.5281/zenodo.18960502) presented QMRP as a general concept. Paper 26 v2 supersedes v1 in three specific respects:

  1. Prior-art correction: The tetralattice EIGHT_4 (Shramko-Wansing, Studia Logica 2009-10) establishes 8-valued paraconsistent logic. D-FUMT₈'s differentiator is not "8 values" but its 8-axis semantics (each axis carrying a distinct extension direction over Belnap-Dunn FOUR).
  2. Post-v1 Clifford rotor-quantization literature: TurboQuant (Google ICLR 2026) and RotorQuant (Scrya 2025). RotorQuant achieves 44× fewer parameters via Cl(3,0) rotor sandwich versus TurboQuant's random-rotation baseline (parameter counts as of the RotorQuant release; independent replication pending, §B.7).
  3. Explicit natural embedding with Lean 4 axiom-free machine-checked structural theorems (this paper's core contribution).

Part A: Required (paper-level statement, 4 elements)

A.1 Findings

  • D-FUMT₈ (8 values) and Cl(3,0) (8 basis elements) share the grade multiplicity (1, 3, 3, 1) under an explicit natural embedding.
  • TRUE ↦ I (scalar, grade 0). Consequence: TRUE is a group-theoretic fixed point of every basis rotor sandwich r · I · reverse(r). This is the Clifford-group articulation of the D-FUMT₈ Peace Axiom (Theory #196: TRUE ≡ ⊤ immutable).
  • SELF ↦ E123 (pseudoscalar, grade 3, the Cl(3,0) center element). Consequence: SELF sign-flips under grade-parity reflection (main involution) and is recovered after two reflections. This is the algebraic articulation of the D-FUMT₈ SELF⟲ (self-referential fixed-point) axis.
  • The remaining six values {FALSE, NEITHER, ZERO, BOTH, INFINITY, FLOWING} split cleanly across the six non-trivial grades: {FALSE ↦ E1, NEITHER ↦ E2, ZERO ↦ E3} (grade 1 vectors, "concrete tension" axes) and {BOTH ↦ E12, INFINITY ↦ E13, FLOWING ↦ E23} (grade 2 bivectors, "structural mediation" axes). Other grade-respecting bijections are structurally equivalent.

A.2 Proofs (Lean 4) — completed 2026-07-25, axiom-free machine-checked

File: data/lean4-mathlib/CollatzRei/Paper26V2DFumtClifford.lean (508 lines, 11 sections)

Axiom audit (#print axioms on 23 theorems, actually run):

  • 9 theorems fully zero-axiom ("does not depend on any axioms"): self_negation_under_reflection, self_reflection_is_involution, true_is_rotor_fixed_point, dfumt8_grade_partition, vector_sq_is_pos_I, bivector_sq_is_neg_I, pseudoscalar_sq_is_neg_I, mainInvolution_fixes_even, mainInvolution_negates_odd
  • 14 theorems depend only on [propext, Classical.choice, Quot.sound] (Mathlib standard base)
  • Zero sorry, zero native_decide, zero user axioms — matches the discipline of STEP 1215 (Dfumt8CategoryExperiment), STEP 1264 (Dfumt8Binary64Refinement), and Task 20 (Dfumt8SelfReflexivePreservation, 2026-07-24).

Three core theorems (matching §A.1 findings):

  • dfumt8ToCliff30_injective + dfumt8ToCliff30_surjective (packaged as dfumt8Equiv : Dfumt8 ≃ Cliff30): the D-FUMT₈ → Cl(3,0) map is a bijection.
  • peace_axiom_invariant_under_rotor: ∀ r : Cliff30, sandwichI r = ⟨1, I⟩. All eight basis rotors {I, e₁, e₂, e₃, e₁e₂, e₁e₃, e₂e₃, e₁e₂e₃} leave the scalar I invariant under the sandwich r · I · reverse(r) = +I. The grade-2/3 cases carry two independent sign flips (r · reverse(r) = ⟨-1, -1⟩ → +1) that cancel exactly, so the invariance is not merely trivial identity.
  • self_negation_under_reflection: mainInvolution E123 = ⟨-1, E123⟩. Together with self_reflection_is_involution (α ∘ α = id on E123), this witnesses SELF's involutive self-return under grade-parity reflection.

Bundle theorem (for paper citation): paper26_v2_main_bundle packages the three claims as a single ∧-statement.

Grade partition (machine-checked): dfumt8_grade_multiplicities verifies |grade⁻¹(0)| = 1, |grade⁻¹(1)| = 3, |grade⁻¹(2)| = 3, |grade⁻¹(3)| = 1 under the embedding — the structural coincidence with Cl(3,0)'s 2^0 + 2^1·3 + 2^2·... dimension decomposition made explicit.

Verification:

  • lake env lean CollatzRei/Paper26V2DFumtClifford.lean: clean pass (no errors)
  • lake build CollatzRei: 7934 / 7934 jobs success (332 seconds), zero regression on the CollatzRei root tree
  • Axiom audit reproducible via data/lean4-mathlib/Paper26V2AxiomCheck.lean

A.3 Honest positioning

  • What is claimed: (i) an explicit 8-element grade-respecting bijection D-FUMT₈ ↔ Cl(3,0); (ii) rotor-sandwich invariance of the scalar for all eight basis rotors; (iii) pseudoscalar sign flip + involution under grade-parity reflection. All three are Lean 4 axiom-free and reproducible.
  • What is NOT claimed:
    1. No continuous rotor claim. The theorem covers the eight basis rotors, not arbitrary R = cos(θ) + sin(θ) · B continuous rotors over ℝ. The linear-combination extension is direct in principle but requires a Module ℝ structure on Cl(3,0) that is not built in this file. Deferred to Paper 26 v3 using Mathlib.LinearAlgebra.CliffordAlgebra.
    2. No operator equality with D-FUMT₈ AND/OR. STEP 1215 established and8_associativity_fails_witness (D-FUMT₈ AND is not associative on the full 8 values), while the Clifford geometric product is associative. The two algebraic operations are therefore incompatible as magma / monoid structures; only the 8-element carrier and the grade partition are matched.
    3. No "world-first" claim on 8-valued algebra. EIGHT_4 (Shramko-Wansing 2009-10) is prior art; MIT trapped-ion d=8 qudit Grover (Shi et al. 2026, arxiv:2506.09371) is prior art at the quantum hardware level. Paper 26 v2's differentiator is the D-FUMT₈ 8-axis semantics + Lean 4 axiom-free bridge to Cl(3,0), not first-mover status on 8-valued logic itself. See also Paper 145 v0.5 corrigendum discipline.
    4. No empirical benchmark claim. TurboQuant / RotorQuant comparison numbers cited in §B.5 are from the respective authors' releases; §B.7 shows an in-house baseline only, with the post-quantization measurement labeled "pending v3". Independent replication of the Scrya / Google numbers is not claimed here.

A.4 Required platform links

Part B: Conditional (7 elements)

B.5 Background — TurboQuant + RotorQuant lineage (cited numbers per source, not independently replicated)

Year Work Approach Cited claim
2024 QuaRot Hadamard rotation on LLaMA-2/3 4-bit 4-bit quantization with limited PPL loss
2025 TurboQuant (Google) Random rotation matrix, MSE-only baseline ~1.07 PPL gain over Hadamard baseline
2025 RotorQuant (Scrya) Cl(3,0) rotor sandwich 44× fewer parameters (372 vs 16,399 at d=128); 5.3× faster prefill; 28% faster decode
2026 D-FUMT₈ × Cl(3,0) (this paper) 8-axis semantics on rotor basis; Lean 4 axiom-free refinement Formal proof that scalar is rotor-sandwich fixed; pseudoscalar sign-flip under reflection

The RotorQuant numbers are the authors' benchmarks against their reference implementations; independent third-party replication is a separate open task (see §B.7).

B.6 Methodology

  1. Mathematical framework (Lean 4 v4.29.0, Mathlib v4.27.0): D-FUMT₈ inductive from CollatzRei.Dfumt8CategoryExperiment (STEP 1215); Cl(3,0) as an 8-element inductive with an explicit 8×8 geometric product table + a signed-basis wrapper. Reverse involution follows the standard reverse(a_r) = (-1)^(r(r-1)/2) · a_r sign rule; main involution follows the grade-parity α(a_r) = (-1)^r · a_r sign rule. All theorems proved by by decide over the finite enumeration.
  2. In-house baseline (qwen2.5:3b on Ollama v0.32.3, Intel i7-6700 / 64GB / no GPU): 10-prompt sweep, 12.4 tok/s median. Raw data: data/turboquant-baseline-qwen2.5-3b.json.
  3. TurboQuant post-quantization (deferred to v3): pull iliafed/nemotron-quant (or Hugging Face equivalent) and re-run the same 10-prompt sweep for direct Δ measurement.
  4. Cl(3,0) silicon embedding (deferred to v3, Phase C hardware phase): 8-LUT primitive on Tang Console NEO GW5AST-138B (already programmed with D-FUMT₈ ALU per STEP 1029; Cl(3,0) primitive is a distinct next STEP).

B.7 Empirical scope (v0.2 as-of 2026-07-25, pending v3 completion)

Substrate Item Baseline Post-quantization Δ
Intel i7-6700 / 64GB / Ollama qwen2.5:3b tokens per second 12.4 tok/s (10-prompt median, data/turboquant-baseline-qwen2.5-3b.json) pending v3 (iliafed/nemotron-quant pull) pending
Tang Console NEO GW5AST-138B D-FUMT₈ 8-value ALU LUT count 37 LUT4 (STEP 1029 physical silicon, User Code 0x00005C27; STEP 1011 toolchain synthesis independently) Cl(3,0) 8-basis primitive pending v3 pending

Honest scope of §B.7: this table's pending v3 entries are placeholders, not measured data. The Lean 4 §A.2 proofs are the load-bearing v0.2 contribution; §B.7 is v0.2 evidence-of-work-in-progress, not evidence-of-benchmark-completion. Following the Paper 145 v0.3 → v0.9 iteration pattern, later versions will replace pending v3 cells with measured values from the same substrates.

B.8 Reproducibility 

git clone https://github.com/fc0web/rei-aios.git
cd rei-aios/data/lean4-mathlib
lake build CollatzRei                # ~332s on Intel i7-6700, expect 7934/7934 jobs
lake env lean Paper26V2AxiomCheck.lean  # print axiom footprint of all 23 theorems
Enter fullscreen mode Exit fullscreen mode

The baseline measurement is reproducible via:

ollama pull qwen2.5:3b
npx tsx scripts/turboquant-baseline.ts   # writes data/turboquant-baseline-qwen2.5-3b.json
Enter fullscreen mode Exit fullscreen mode

B.9 Related work (Rei-AIOS internal ecosystem)

  • Paper 26 v1 (2025-09-15, DOI 10.5281/zenodo.18960502) — QMRP general concept origin
  • Paper 145 v0.3 (2026-05-09, DOI 10.5281/zenodo.20091185) — 3-substrate D-FUMT₈ silicon + IBM Heron r2 + Aer; publish pattern precedent
  • Paper 145 v0.7 (Zenodo 20192813) — v0.3 iteration precedent
  • Paper 61 / 62 / 63 / 64 / 65 (ZCSG / MDNST / SNST / OPU / Lean 4 formal verification) — three-party philosophical + Lean 4 ecosystem
  • STEP 1215 Dfumt8CategoryExperiment — D-FUMT₈ inductive + AND non-associativity witness
  • STEP 1264 Dfumt8Binary64Refinement — Verilog ↔ Lean 4 binary encoding refinement pattern
  • Task 20 Dfumt8SelfReflexivePreservation (2026-07-24) — SELF⟲ semantic-preservation-under-encoding pattern reused in this paper's §A.2

B.10 Prior-art audit (2026-04-30, docs/prior-art-audit-8valued-rotation.md)

  • EIGHT_4 tetralattice (Shramko-Wansing 2009-10, Studia Logica 92(2):265-280): 8-valued paraconsistent logic. Paper 26 v2 differentiator: D-FUMT₈ carries 8 semantic axes (each with a distinct role: paraconsistency, undefinedness, absence, unbounded, null, motion, self-reference, over-and-above the base four TRUE/FALSE), whereas EIGHT_4 is a lattice structure on the powerset {a, d, u}.
  • RotorQuant (Scrya 2025): Cl(3,0) rotor sandwich for LLM quantization. Paper 26 v2 differentiator: Lean 4 axiom-free structural theorems on the D-FUMT₈ ↔ Cl(3,0) embedding, not a competing quantization scheme.
  • MIT trapped-ion d=8 qudit Grover (Shi et al. 2026, arxiv:2506.09371): 8-valued quantum hardware. Paper 26 v2 differentiator: classical Lean 4 formalization, not a hardware claim; explicitly does not compete on 8-valued quantum first-mover.

B.11 Notation and conventions

  • D-FUMT₈ value symbols: TRUE / FALSE / BOTH / NEITHER / INFINITY / ZERO / FLOWING / SELF
  • Cl(3,0) basis symbols: I / E1 / E2 / E3 / E12 / E13 / E23 / E123 (with E12 = E1 · E2, etc.)
  • Sign convention: Eᵢ · Eᵢ = +I for i ∈ {1,2,3} (positive signature); Eᵢ · Eⱼ = -Eⱼ · Eᵢ for i ≠ j (anticommutation); E12 · E12 = E13 · E13 = E23 · E23 = E123 · E123 = -I (derived, verified in bivector_sq_is_neg_I and pseudoscalar_sq_is_neg_I)
  • Reverse: grade-0 and grade-1 blades keep sign; grade-2 and grade-3 blades flip sign under reverse
  • Main involution (grade-parity): odd grades (1 and 3) flip sign; even grades (0 and 2) keep sign

Part C: Optional

Full Part C (7 elements per the OUKC paper structure) is deferred to v3. The v0.2 pre-print load-bearing content is Parts A + B; Part C additions are structural and do not gate machine-check-level claims.

References

  1. Shramko, Y., Wansing, H. "A Few More Useful 8-valued Logics for Reasoning with Tetralattice EIGHT_4," Studia Logica, 92(2), 265-280, 2009-10.
  2. Fujimoto, N. (2025). "Paper 26 v1 — Quality Metric Relativity Principle (QMRP)," Zenodo, DOI: 10.5281/zenodo.18960502.
  3. Doran, C., Lasenby, A. Geometric Algebra for Physicists, Cambridge University Press, 2003. — Cl(3,0) reference multiplication conventions.
  4. TurboQuant (Google, ICLR 2026) — random-rotation baseline.
  5. RotorQuant (Scrya, 2025) — Cl(3,0) rotor sandwich; Hugging Face GGUF release.
  6. Shi, Q., et al. "Trapped-Ion Implementation of d=8 Qudit Grover," arxiv:2506.09371, 2026.
  7. docs/prior-art-audit-8valued-rotation.md (internal, 2026-04-30).
  8. docs/qmrp-operational-definition-v2.md (internal, 2026-04-30).
  9. Fujimoto, N., Rei-AIOS, Claude (2026). "Paper 145 v0.3 — First D-FUMT₈ Silicon with SELF⟲ Logic Primitive," Zenodo, DOI: 10.5281/zenodo.20091185.
  10. Rei-AIOS repository: https://github.com/fc0web/rei-aios (Lean 4 source, publish scripts, publish logs).

Version history

  • v0.1 (2026-05-01): initial draft, §A/B outline only.
  • v0.2 (2026-07-25): §A.2 Lean 4 axiom-free machine-check completed (23 theorems: 9 zero-axiom + 14 standard base). §A.3 honest positioning strengthened with 4 explicit non-claims. §B.7 explicitly framed as pending-v3. 11-platform publish per Paper 145 v0.3 pattern (this version).
  • v3 (pending): §B.7 empirical measurements (TurboQuant iliafed/nemotron-quant sweep + Tang Console NEO Cl(3,0) 8-basis primitive silicon programming). §C 7 elements. Mathlib CliffordAlgebra bridge for continuous rotors.

Discipline anchors (Rei-AIOS internal)

  • No-rush publication (feedback_no_rush_publication): 85-day draft period from v0.1 to v0.2 publish.
  • Publish-verification (feedback_paper_publish_verification_discipline): all 11 platforms verified HTTP 200 + content grep post-publish; results in data/publications/publish-log-paper026v2*.json.
  • World-uniqueness discipline (feedback_world_uniqueness_claim_controllable): no "world-first" claim; four explicit non-claims in §A.3.
  • Chat-Claude term uncritical adoption (feedback_chat_claude_term_uncritical_adoption): all cited external numbers (TurboQuant / RotorQuant / MIT d=8 Grover) are labeled as authors' claims pending independent replication.
  • Zero-sorry floor (feedback_zero_sorry_floor_not_ceiling): 23 theorem axiom-free is the floor of this paper's formal content; depth / semantic completeness ceiling remains open (continuous rotors, operator alignment).

Co-Authored-By: Fujimoto Nobuki × Rei-AIOS × Claude (Anthropic) per OUKC charter v1.0.

Top comments (0)