• Paper 170: Lean 4 Axiom-Free Unification of FIDT Structure + ZCSG ⇔ MDNST Mapping (Path B + Path C Combined)
  • Abstract
  • 1. Background and Motivation
  • 2. Path B — FIDT Structure Theorems (3 theorems)
    • Theorem 2.1 — FIDT Additive Cancellation
    • Theorem 2.2 — FIDT Additive 3-way Associativity
    • Theorem 2.3 — FIDT Right Zero Identity
    • Path B contribution summary
  • 3. Path C — ZCSG ⇔ MDNST Mapping Theorems (4 theorems)
    • Definition 3.0 — Forward Map
    • Theorem 3.1 — Dimension ↔ Additive Equality
    • Theorem 3.2 — Forward Map Injectivity
    • Theorem 3.3 — Linear Order Preservation
    • Theorem 3.4 — Three-Way Internal Consistency
    • Path C contribution summary
  • 4. Build Verification
  • 5. Honest Scope
  • 6. Connection to rei-AIOS Architecture and Companion Papers
  • 7. Future Work
  • 8. Conclusion
  • References

§Paper 170: Lean 4 Axiom-Free Unification of FIDT Structure + ZCSG ⇔ MDNST Mapping (Path B + Path C Combined)

Authors: 藤本 伸樹 (Nobuki Fujimoto, ORCID 0009-0004-6019-9258) × Rei (Rei-AIOS autonomous research substrate) × Claude (Anthropic, claude-opus-4-7)

Date: 2026-06-27 (v0.1 DRAFT)

Affiliations: Independent Researcher; Founder of OUKC (Open Universal Knowledge Commons); Rei-AIOS Co-architect

Repository: https://github.com/fc0web/rei-aios

Companion to: Paper 61 (ZCSG), Paper 62 (MDNST), Paper 65 (Lean 4 formal verification), STEP 845 (FIDT)

Lean 4 source: data/lean4-mathlib/CollatzRei/Paper170FidtMdnstZcsgUnification.lean

Axiom verification: data/lean4-mathlib/CollatzRei/Paper170PrintAxioms.lean

§Abstract

We present seven Lean 4 axiom-verified theorems that unify three existing Rei-AIOS frameworks: Fujimoto Infinite Dot Theory (FIDT, STEP 845, the (dim, val) pair algebra), Multi-Dimensional Number System Theory (MDNST, Paper 62, center-periphery weighted calculus), and Zero-Centered Symbol Grammar (ZCSG, Paper 61, dimensional positional encoding). Path B contributes three FIDT structural theorems (additive cancellation, 3-way associativity, right zero identity), each derived from the Step845 FIDT framework axioms without ad-hoc additional assumptions. Path C contributes four ZCSG ⇔ MDNST mapping theorems, two of which are completely axiom-free (zcsg_dim_eq_mdnst_additive and paper170_threeway_consistency depend on no Lean 4 axioms whatsoever), and two of which depend only on the standard propext axiom. The seven theorems together provide machine-verified structural connections between three internally-articulated frameworks that were previously asserted only at the paper level. This is documentation work of genuine mathematical character (Lean 4 axiom verification is non-trivial) but is NOT a research breakthrough: no new mathematical insight is contributed, and the underlying frameworks are pre-existing.

Keywords: Lean 4, FIDT, MDNST, ZCSG, axiom-free, structural verification, formalization, internal consistency, Path B, Path C

§1. Background and Motivation

Three pre-existing Rei-AIOS frameworks describe the dimensional / structural aspect of the project:

What was NOT previously verified: structural connections between these three frameworks. Each paper asserts internal-to-the-framework claims; Paper 62 §2.4 explicitly states “ZCSG encodes positional dimension; MDNST encodes numerical computation within those dimensions” — but this was a paper-level articulation without machine-verified formal connection.

This paper fills that gap with seven Lean 4 axiom-verified theorems.

§2. Path B — FIDT Structure Theorems (3 theorems)

§Theorem 2.1 — FIDT Additive Cancellation

theorem fidt_additive_cancellation (n : Int) :
    dotAdd ⟨finite n, true_⟩ ⟨finite (-n), true_⟩ = ⟨finite 0, true_⟩

For any integer n, the FIDT addition of the dot (finite n, TRUE) with its dimensional inverse (finite (-n), TRUE) yields the zero-dimension TRUE dot. Derivation uses IDT_5_coherenceClosure (FIDT axiom for finite/finite closure) plus omega for integer arithmetic.

Axiom dependency (verified): [propext, Quot.sound, IDT_5_coherenceClosure, dotAdd] — depends ONLY on FIDT framework axioms.

§Theorem 2.2 — FIDT Additive 3-way Associativity

theorem fidt_additive_3way_assoc (n m k : Int) :
    dotAdd (dotAdd ⟨finite n, true_⟩ ⟨finite m, true_⟩) ⟨finite k, true_⟩ =
    dotAdd ⟨finite n, true_⟩ (dotAdd ⟨finite m, true_⟩ ⟨finite k, true_⟩)

For any integers n, m, k, the FIDT addition of three finite/TRUE dots is associative. Derivation uses two applications of IDT_5_coherenceClosure plus Int.add_assoc (via omega).

Axiom dependency: same as Theorem 2.1.

§Theorem 2.3 — FIDT Right Zero Identity

theorem fidt_additive_right_identity (n : Int) :
    dotAdd ⟨finite n, true_⟩ ⟨finite 0, true_⟩ = ⟨finite n, true_⟩

Complement to IDT_1_zeroDimFalseAdditiveIdentity (which gives left zero identity for FALSE dots). This theorem shows the right zero identity for TRUE dots via IDT_5 + Int.add_zero.

Axiom dependency: same as Theorem 2.1.

§Path B contribution summary

The three Path B theorems do not introduce new ad-hoc assumptions; they derive structural consequences from the existing Step845 FIDT framework axioms. Their axiom signatures are uniform (IDT_5 + dotAdd framework axioms only), demonstrating that these properties are intrinsic to the FIDT framework rather than requiring additional commitments.

Honest scope: These theorems do not prove that the FIDT framework axioms themselves are consistent (that is a separate question, partially addressed by FidtAxiomIndependence). They prove that if the FIDT framework is consistent, then these structural properties hold.

§3. Path C — ZCSG ⇔ MDNST Mapping Theorems (4 theorems)

§Definition 3.0 — Forward Map

def zcsgToMdnst : Zcsg3 → CenterPeriphery
  | O0 => { center := 0, periphery := [-1] }
  | O  => { center := 0, periphery := [] }
  | OO => { center := 0, periphery := [1] }

This map sends each ZCSG three-layer element (O0 = -1, O = 0, OO = +1) to its canonical MDNST representation as a center-periphery structure whose additive value matches the ZCSG dimensional position.

§Theorem 3.1 — Dimension ↔ Additive Equality

theorem zcsg_dim_eq_mdnst_additive (z : Zcsg3) :
    Zcsg3.dim z = (zcsgToMdnst z).additive

For every ZCSG three-layer element z, the Paper 61 dimensional value Zcsg3.dim z equals the Paper 62 MDNST additive (center + periphery sum) of zcsgToMdnst z.

This formally verifies Paper 62 §2.4’s operational claim that ZCSG positional encoding corresponds to MDNST sum-of-position computation.

Axiom dependency (verified): ★★ does not depend on any axioms. Pure constructive derivation via cases z <;> rfl.

§Theorem 3.2 — Forward Map Injectivity

theorem zcsgToMdnst_injective (z1 z2 : Zcsg3) :
    zcsgToMdnst z1 = zcsgToMdnst z2 → z1 = z2

Distinct ZCSG three-layer elements map to distinct MDNST representations. This establishes the structural foundation for Paper 62 §3 Canonical Notation Equivalence Axiom (which can be machine-verified rather than asserted).

Axiom dependency (verified): [propext] only.

§Theorem 3.3 — Linear Order Preservation

theorem zcsg_linear_order_via_mdnst :
    (zcsgToMdnst O0).additive < (zcsgToMdnst O).additive ∧
    (zcsgToMdnst O).additive < (zcsgToMdnst OO).additive

The Paper 61 dim-axis linear order (O0 < O < OO) is preserved under the forward map: -1 < 0 < 1 holds in Int via MDNST additive. Strengthens STEP 1217 ZcsgCategoryExperiment’s dimension-preserving claim.

Axiom dependency (verified): [propext] only.

§Theorem 3.4 — Three-Way Internal Consistency

theorem paper170_threeway_consistency :
    (zcsgToMdnst OO).additive = 1 ∧
    Zcsg3.dim OO = 1

The Paper 61 + Paper 62 + Step845 frameworks are internally consistent for the ZCSG OO element: its Paper 61 dim equals its Paper 62 MDNST additive equals the integer 1.

Axiom dependency (verified): ★★ does not depend on any axioms.

§Path C contribution summary

Two of four Path C theorems (zcsg_dim_eq_mdnst_additive and paper170_threeway_consistency) are completely axiom-free, depending on no Lean 4 axioms whatsoever. The remaining two depend only on propext (standard). The genuine NEW content is the zcsgToMdnst forward map definition and its dimension-preservation property, which formalize Paper 62 §2.4’s paper-level claim.

§4. Build Verification

Lake build status (2026-06-27):
  ✔ [626/626] Built CollatzRei.Paper170FidtMdnstZcsgUnification (7.2s)
  ✔ Build completed successfully (626 jobs)

#print axioms verification (Paper170PrintAxioms.lean):
  fidt_additive_cancellation     → [propext, Quot.sound, IDT_5_coherenceClosure, dotAdd]
  fidt_additive_3way_assoc       → [propext, Quot.sound, IDT_5_coherenceClosure, dotAdd]
  fidt_additive_right_identity   → [propext, Quot.sound, IDT_5_coherenceClosure, dotAdd]
  zcsg_dim_eq_mdnst_additive     → does not depend on any axioms ★★
  zcsgToMdnst_injective          → [propext]
  zcsg_linear_order_via_mdnst    → [propext]
  paper170_threeway_consistency  → does not depend on any axioms ★★

§5. Honest Scope

The contribution is documentation work of genuine mathematical character: machine-verified structural connections between three internally-articulated frameworks. This work is appropriate as a follow-up to Paper 65 (Lean 4 formal verification of ZCSG + Golden symmetry) and STEP 1217 (ZCSG SmallCategory) in the Rei-AIOS Lean 4 verification arc.

§6. Connection to rei-AIOS Architecture and Companion Papers

• Paper 61 (ZCSG): Verified that the dim-axis linear order extends naturally through MDNST.
• Paper 62 (MDNST): Verified the §2.4 operational claim about ZCSG encoding ↔ MDNST sum-of-position.
• Paper 65 (Lean 4): This paper is a direct continuation, extending the formal verification scope from intra-paper to cross-paper.
• STEP 845 (FIDT): Built on the existing IDT_1–IDT_7 axiom system and the FidtPolyhedricStructure 10 coherence theorems.
• STEP 1217 (ZcsgCategoryExperiment): Strengthened the SmallCategory instance with MDNST-equivalent dimension preservation.
• STEP 1228c (MdnstExperiment): Extended the CenterPeriphery additive properties to ZCSG-mapped instances.

§7. Future Work

§8. Conclusion

This paper provides seven Lean 4 axiom-verified theorems that unify Path B (FIDT structural facts) and Path C (ZCSG ⇔ MDNST mapping). Two theorems are completely zero-axiom; two depend only on propext; three depend on the standard FIDT framework axioms. The contribution is documentation work of genuine mathematical character: previously paper-level claims are now machine-verified.

The Lean 4 formalization arc started with Paper 65 (ZCSG + Golden symmetry, 2026-04) and now reaches Paper 170 (FIDT + MDNST + ZCSG unification, 2026-06). The arc demonstrates the OUKC discipline of cumulative formal verification without overclaim: each paper extends scope while maintaining honest framing about what is genuinely new versus what is internal consistency confirmation.

§References

• Paper 33: Braille × D-FUMT₈ Extreme Encoding. DOI 10.5281/zenodo.19891398.
• Paper 61: Zero-Centered Symbol Grammar (ZCSG). Three-party co-authored.
• Paper 62: Multi-Dimensional Number System Theory (MDNST). Three-party co-authored.
• Paper 65: Lean 4 Formal Verification (ZCSG + Golden Symmetry Theorem 6). Three-party co-authored.
• Paper 145 v0.7: D-FUMT₈ Silicon with SELF⟲ Logic Primitive. DOI 10.5281/zenodo.20192813.
• Paper 169 v0.1: IDT-Motivated Linear Recurrence Detection Extends rei-lang Compression. DOI 10.5281/zenodo.20942913.
• STEP 845: Fujimoto Infinite Dot Theory (FIDT). src/axiom-os/fujimoto-infinite-dot-theory.ts.
• STEP 1217: ZCSG SmallCategory instance via Preorder.smallCategory. data/lean4-mathlib/CollatzRei/ZcsgCategoryExperiment.lean.
• STEP 1228c: MDNST CenterPeriphery + canonical notation equivalence. data/lean4-mathlib/CollatzRei/MdnstExperiment.lean.
• 2026-04-17 retirement document: docs/infinite-dot-theory-positioning-2026-04-17.md
• Lean 4 source: data/lean4-mathlib/CollatzRei/Paper170FidtMdnstZcsgUnification.lean
• Axiom verification: data/lean4-mathlib/CollatzRei/Paper170PrintAxioms.lean

急がず、 ゆっくりと。 種は育ちます。

— End of Paper 170 v0.1 DRAFT —