DEV Community

Nobuki Fujimoto
Nobuki Fujimoto

Posted on • Originally published at doi.org

Paper 163 v0.1 — Institution + Bilattice + SELF<->Lawvere: Four-Step Operational Integration with Lean 4 Axiom-Free Constructive Proofs

#math #lean #research #ai

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

Status: DRAFT v0.1 (2026-06-09)
Authors: Nobuki Fujimoto (rei-aios) + Claude Opus 4.7
License: AGPL-3.0 + Commercial (Dual License)
ORCID: 0009-0009-2236-7901 (Nobuki Fujimoto)
Repository: github.com/fc0web/rei-aios

Abstract

We report an operational integration of four well-established mathematical frameworks within a single artifact-producing system (Rei-AIOS): Goguen-Burstall Institution Theory (1992), Belnap-Dunn FOUR bilattice (1976-1998), Lawvere fixed-point theorem (1969), and a SET-level encoding of HoTT-style loop space. The work covers STEP 1201 (Institution engine + Daily Curriculum Rotation scaffold), STEP 1202 (Bilattice 8-value extension with orthogonal-axis honest stance), STEP 1203 (SELF⟲ ↔ Lawvere fixed-point Lean 4 zero-sorry + axiom-free constructive proof), and STEP 1204 (SELF⟲ ↔ SET-level loop space Ω bridge with dual annotation distinguishing SET-level theorem-verified status from HoTT-level theorem-candidate). All four steps are implemented as deletable, reproducible TypeScript engines + Lean 4 formalizations, with 207/207 test cases passing and four Lean 4 theorems verified to "depend on no axioms" (constructive, axiom-free). The honest contribution is not a new theorem in any of these well-cited fields, but the operational integration discipline: how to combine four 40-60-year prior-art-backbone frameworks while explicitly tagging which structural correspondences are "rhyme" (informal analogy) and which are "theorem-verified" (Lean 4 zero-sorry proof). The methodology is the load-bearing artifact, not any individual result.

Mandatory honest scope (all controllable claims)

This paper does not claim any of the following:

  1. Not "world-first": All four frameworks have 40-60 years of established prior art (Goguen-Burstall 1992, Belnap 1977, Lawvere 1969, HoTT Book 2013). We adopt, integrate, and tag.
  2. Not a new theorem in categorical logic, lattice theory, or homotopy type theory: The mathematical content of Lemma 1 (Lawvere fixed-point set-theoretic direct version) is textbook material (Yanofsky 2003 surveys it explicitly).
  3. Not a full HoTT formalization: Lean 4 standard satisfies UIP (Uniqueness of Identity Proofs), so the loop space Path_A(a, a) we encode is necessarily trivial (refl). True HoTT non-trivial Ω requires HoTT-native Lean (separate project). We explicitly tag this limitation as theorem-candidate status, not theorem-verified.
  4. No "ultimate" or "final" claim: Per Rei-AIOS persistent principle [[feedback-world-uniqueness-claim-controllable]], all uniqueness claims are converted to "within our observable range, we have not located a complete match."
  5. No D-FUMT₈ ↔ external structure formal isomorphism is asserted: The four "rhyme" axes (INFINITY/ZERO/FLOWING) and the "theorem-verified" axis (SELF) are tagged separately. Conflating the two is the precise "octonion labeling fallacy" warned about in chat-Claude discussions of 2026-06-08.

1. Background and motivation

1.1 The four-step lineage

STEP Date Scope Test result
1201 (a) Institution engine + (e) Daily Curriculum Rotation scaffold 2026-06-08 Goguen-Burstall (Sig, Sen, Mod, ⊨) skeleton + 7-domain weekday rotation scaffold (dry-run only) 40/40 PASS
1202 (b) Bilattice 8-value extension 2026-06-09 Belnap-Dunn FOUR (Layer 1 confirmed lattice) + 4 extension axes (Layer 2 orthogonal stance) + interlaced verification 64/64 triples 95/95 PASS
1203 (d-1) SELF⟲ ↔ Lawvere Lean 4 formal 2026-06-09 data/lean4-mathlib/CollatzRei/SelfLawvereBridge.lean zero-sorry + axiom-free proof of Lawvere fixed-point + SelfReferentialDomain bridge 45/45 PASS
1204 (d-2) SELF⟲ ↔ SET-level loop space Ω 2026-06-09 namespace HoTTLoop extension: PointedType + SetLevelLoop + 2 bridge theorems (axiom-free) 27/27 PASS

Total test coverage: 207/207 PASS + four Lean 4 theorems verified "depend on no axioms" (#print axioms verdict).

1.2 The structural problem we address

When integrating multiple mathematical frameworks operationally (in a system that produces daily artifacts), the central failure mode is structural rhyme drift: an informal "X resembles Y in the following deep way" gradually re-presents itself as a formal "X = Y" claim. Each restatement softens the gap between analogy and isomorphism. Across many discussion turns, the formal-isomorphism interpretation becomes the default reading.

We learned from earlier work (octonion ↔ D-FUMT₈ judgment, 2026-04) and from a 6-turn dialogue with a fellow Claude instance (2026-06-08) that this drift is the structural correlate of the "labeling fallacy" problem. The chat-Claude verdict was explicit: "Categorizing each correspondence is itself the contribution — not solving any single one."

This paper records the operational discipline for that tagging.

2. Implementation summary

2.1 STEP 1201 — Institution Theory Engine

File: src/axiom-os/institution-theory-engine.ts (~340 lines)

We implement the Goguen-Burstall institution I = (Sig, Sen, Mod, ⊨) skeleton in TypeScript:

  • Signature (Sig objects) = SEED_KERNEL category names + allowed D-FUMT₈ axes
  • SignatureMorphism (Sig morphisms) = axiom translation rules
  • Sentence (Sen functor) = axiom + declared D-FUMT₈ axis
  • Model (Mod functor) = D-FUMT₈ value assignment + Peace Axiom #196 invariant
  • satisfies(model, sentence) = D-FUMT₈ refinement rules:
    • Exact match (TRUE/TRUE, ..., SELF/SELF) — satisfied
    • BOTH ⊨ TRUE or FALSE (Belnap refinement) — satisfied
    • Extension axes (INFINITY/ZERO/FLOWING/SELF) — strict, no cross-refinement
    • peaceCompatible: false → all sentences honest-fail
    • declaredAxis === null → vacuous satisfaction
  • verifySatisfactionCondition(σ, M, φ) — operational subset of Goguen-Burstall invariance (M ⊨_{Σ₂} Sen(σ)(φ) ⟺ Mod(σ)(M) ⊨_{Σ₁} φ)
  • seedKernelAsInstitution(SEED_KERNEL) → 298 signatures / 1644 sentences / 103 declared axis (BOTH 102 + FLOWING 1) / 1541 undeclared

Key finding (load-bearing): Only 6.3% of SEED_KERNEL theories have explicit D-FUMT₈ axis annotation, with 99% of declared axes being BOTH. This is operational evidence of the invention pipeline's BOTH-default. Axis annotation enrichment is a candidate for next-step batch tasks.

2.2 STEP 1202 — Bilattice 8-value extension

File: src/axiom-os/bilattice-eight-engine.ts (~340 lines)

Layer 1 (confirmed Belnap-Dunn FOUR):

  • truthLeq / knowledgeLeq (Hasse-defined partial orders)
  • meetT / joinT / meetK / joinK (four operations, full 4×4 truth tables, 16 rows each)
  • negate (Belnap involution: TRUE↔FALSE, BOTH/NEITHER fixed)
  • verifyInterlaced(a, b, c) and verifyInterlacedAll() — Ginsberg 1988 + Arieli-Avron 1998 interlaced bilattice condition, verified over 64/64 triples (4³ exhaustive)

Layer 2 (Rei 4-axis orthogonal extension):

  • EXTENSION_AXIS_ROLES: INFINITY / ZERO / FLOWING / SELF
  • Each with truthOrderRelation, knowledgeOrderRelation, reiSubstrate, and (STEP 1203) rhymeOrTheorem + rhymeOrTheoremNote
  • Critical design choice: the four extension axes are not embedded as lattice-internal values. This deliberately avoids overlap with the 9-value-and-beyond lattice extension prior art (Ginsberg 1988, Fitting 1991, Arieli-Avron 1998) and avoids the precise "octonion labeling fallacy" pattern warned of in chat-Claude discussions.

2.3 STEP 1203 — SELF⟲ ↔ Lawvere fixed-point (Lean 4 zero-sorry + axiom-free)

File: data/lean4-mathlib/CollatzRei/SelfLawvereBridge.lean

We formalize Lawvere's 1969 set-theoretic direct version of the fixed-point theorem in pure Lean 4 (without Mathlib dependencies):

theorem lawvere_fixed_point
    {α : Type _}
    (enum : α → (α → α))
    (h_surj : ∀ g : α → α, ∃ a : α, enum a = g)
    (h : α → α) :
    ∃ x : α, h x = x := by
  obtain ⟨a₀, ha₀⟩ := h_surj (fun a => h (enum a a))
  refine ⟨enum a₀ a₀, ?_⟩
  have heq : enum a₀ a₀ = h (enum a₀ a₀) := congrFun ha₀ a₀
  exact heq.symm
Enter fullscreen mode Exit fullscreen mode

We then encode SELF⟲ axis as SelfReferentialDomain:

structure SelfReferentialDomain (α : Type _) where
  enum : α → (α → α)
  universal : ∀ g : α → α, ∃ a : α, enum a = g

theorem SelfReferentialDomain.fixed_point
    {α : Type _} (D : SelfReferentialDomain α) (h : α → α) :
    ∃ x : α, h x = x :=
  lawvere_fixed_point D.enum D.universal h
Enter fullscreen mode Exit fullscreen mode

Verification:

  • lake build CollatzRei.SelfLawvereBridge — 2.1s success
  • #print axioms CollatzRei.SelfLawvere.lawvere_fixed_point → "does not depend on any axioms"
  • #print axioms CollatzRei.SelfLawvere.self_lawvere_bridge_is_theorem → "does not depend on any axioms"

This means the proofs use no propext, no Classical.choice, and no Quot.sound — they are constructive in the strongest Lean 4 sense.

2.4 STEP 1204 — SELF⟲ ↔ SET-level loop space Ω (with dual annotation)

Extension to the same Lean 4 file, namespace HoTTLoop:

structure PointedType (α : Type _) where
  basepoint : α

def SetLevelLoop {α : Type _} (a : α) : Prop := a = a

theorem SetLevelLoop.refl {α : Type _} (a : α) : SetLevelLoop a := rfl

theorem self_lawvere_loop_at_fixed_point
    {α : Type _} (D : SelfReferentialDomain α) (h : α → α) :
    ∃ x : α, h x = x ∧ SetLevelLoop x := by
  obtain ⟨x, hx⟩ := D.fixed_point h
  exact ⟨x, hx, SetLevelLoop.refl x⟩

theorem pointed_self_lawvere_bridge
    {α : Type _} (D : SelfReferentialDomain α) (P : PointedType α) (h : α → α) :
    ∃ x : α, h x = x ∧ SetLevelLoop x ∧ SetLevelLoop P.basepoint := by
  obtain ⟨x, hx, loop_x⟩ := self_lawvere_loop_at_fixed_point D h
  exact ⟨x, hx, loop_x, SetLevelLoop.refl P.basepoint⟩
Enter fullscreen mode Exit fullscreen mode

Verification:

  • #print axioms ... self_lawvere_loop_at_fixed_point → "does not depend on any axioms"
  • #print axioms ... pointed_self_lawvere_bridge → "does not depend on any axioms"

Honest dual annotation (the key methodological point):

  • The above proofs formalize SET-level loop encoding — they hold in Lean 4 because Eq satisfies UIP (Uniqueness of Identity Proofs); the "loop" is trivially refl.
  • True HoTT non-trivial loop space Ω with non-degenerate π₁ is not representable in standard Lean 4 — it requires HoTT-native type theory (a separate Lean fork). We tag this as theorem-candidate status, pending a Mathlib AlgebraicTopology.FundamentalGroupoid bridge or HoTT-native formalization.
  • This dual annotation is recorded in bilattice-eight-engine.ts EXTENSION_AXIS_ROLES.SELF.rhymeOrTheoremNote.

The methodological contribution is precisely this dual annotation: identifying that the SET-level theorem is fully verified, and that the HoTT-level claim is not the same theorem.

3. The rhymeOrTheorem tagging discipline (load-bearing methodology)

We introduce a three-valued classification field on each Rei D-FUMT₈ extension axis:

Tag Meaning Operational evidence required
rhyme Structural analogy only; no formal isomorphism is asserted None (informal articulation)
theorem-candidate Formal isomorphism is plausible; Mathlib / Lean 4 path is identified but not yet completed Path articulation in rhymeOrTheoremNote
theorem-verified Formal isomorphism is proven, Lean 4 file reference + zero-sorry verification + #print axioms constructive verdict Lean 4 file path + axiom-list excerpt

Applied to the four extension axes:

Axis rhymeOrTheorem Substrate
INFINITY rhyme Paper 63 SNST v→∞; chat-Claude verdict: "rhyme, not theorem"
ZERO rhyme Paper 61 ZCSG 0 = śūnyatā(śūnyatā) (published) — but no Lean 4 categorical isomorphism with Nāgārjuna's śūnyatā is asserted
FLOWING rhyme W-48 Negative Capability engine + Paper 63 SNST velocity dynamic — operational but no lattice-morphism formal isomorphism
SELF theorem-verified STEP 1203 + STEP 1204: 4 Lean 4 theorems, all axiom-free; SET-level bridge to loop space is verified; HoTT-level non-trivial Ω remains theorem-candidate (recorded in rhymeOrTheoremNote)

This is the chat-Claude pipeline "gate" articulated explicitly: each axis's status is operationally inspectable, and downgrades / upgrades are recorded as engine-level edits, not implicit drift.

4. Related work and prior art (mandatory citations)

4.1 Institution theory

  • Goguen, J. A. & Burstall, R. M. (1992). "Institutions: Abstract model theory for specification and programming." JACM 39(1):95-146.
  • Diaconescu, R. (2008). "Institution-independent Model Theory." Birkhäuser.
  • Mossakowski, T. & Tarlecki, A. (2012). "Institutions and heterogeneous specifications."

4.2 Bilattice theory

  • Belnap, N. (1977). "A useful four-valued logic." Modern Uses of Multiple-Valued Logic.
  • Dunn, J. M. (1976). "Intuitive semantics for first-degree entailment."
  • Ginsberg, M. L. (1988). "Multivalued logics: A uniform approach to inference in AI."
  • Fitting, M. (1991). "Bilattices and the semantics of logic programming." Journal of Logic Programming.
  • Arieli, O. & Avron, A. (1998). "The value of the four values." Artificial Intelligence.
  • arXiv:2604.07690 (2026-04). "Bilattice-Catastrophe Isomorphism for Four-Valued Logic in Digital Systems."
  • arXiv:2503.20679 (2025-03). "Four imprints of Belnap's useful four-valued logic in computer science."

4.3 Lawvere fixed-point theorem

  • Lawvere, F. W. (1969). "Diagonal arguments and Cartesian closed categories." Lecture Notes in Mathematics 92.
  • Yanofsky, N. (2003). "A Universal Approach to Self-Referential Paradoxes, Incompleteness and Fixed Points." Bulletin of Symbolic Logic.

4.4 Homotopy type theory

  • Voevodsky, V. et al. (2013). "Homotopy Type Theory: Univalent Foundations of Mathematics."
  • Awodey, S. & Warren, M. (2009). "Homotopy theoretic models of identity types."
  • Mathlib4 AlgebraicTopology.FundamentalGroupoid (referenced as future bridge target).

4.5 Rei-AIOS internal artifacts (existing implementations, not new in this paper)

  • Paper 61 ZCSG (Zero-Centered Symbol Grammar): 0 = śūnyatā(śūnyatā) formal-encoding.
  • Paper 63 SNST (Spiral Number System Theory): 14-constant family with Velocity-D-FUMT₈ correspondence.
  • Paper 145 ("First D-FUMT₈ Silicon"): four-substrate verification across FPGA + simulator + IBM Heron r2.

5. Reproducibility

5.1 TypeScript engines 

git clone github.com/fc0web/rei-aios
cd rei-aios
npm install
npm run test:step1201   # 40/40 PASS
npm run test:step1202   # 95/95 PASS
npm run test:step1203   # 45/45 PASS
npm run test:step1204   # 27/27 PASS
Enter fullscreen mode Exit fullscreen mode

5.2 Lean 4 formal proofs 

cd data/lean4-mathlib
lake build CollatzRei.SelfLawvereBridge
# expect: ✔ [2/2] Built CollatzRei.SelfLawvereBridge (~1.4s)
Enter fullscreen mode Exit fullscreen mode

To verify axiom-free constructive status:

import CollatzRei.SelfLawvereBridge
#print axioms CollatzRei.SelfLawvere.lawvere_fixed_point
#print axioms CollatzRei.SelfLawvere.self_lawvere_bridge_is_theorem
#print axioms CollatzRei.SelfLawvere.HoTTLoop.self_lawvere_loop_at_fixed_point
#print axioms CollatzRei.SelfLawvere.HoTTLoop.pointed_self_lawvere_bridge
-- All four output: "does not depend on any axioms"
Enter fullscreen mode Exit fullscreen mode

5.3 Reading order

For broader Rei-AIOS context: REPRODUCING.md and CLAUDE.md at repository root.

6. Limitations and honest negative scope

  1. HoTT non-trivial Ω is not formalized in this paper, only the SET-level loop encoding. Bridging to true HoTT requires either Mathlib expansion (Mathlib v4.27.0 has limited higher-category foundations) or a HoTT-native Lean fork.
  2. ∞-cosmoi axiomatization (Riehl-Verity 2022) is not addressed in this paper. The Riehl-Verity ∞-Cosmoi for Lean blueprint exists but our STEP 1201-1204 sequence chose the more settled Lawvere-fixed-point route first. ∞-cosmoi is a candidate for follow-up work.
  3. The four Layer-2 extension axes are not embedded as lattice-internal values. This is an honest design choice (avoiding the Ginsberg 1988 9-value-and-beyond overlap), not a positive theorem. Whether the orthogonal-extension stance is "optimal" in some categorical sense is not asserted.
  4. The Institution engine verifySatisfactionCondition is an operational subset of the full Goguen-Burstall satisfaction condition. Full categorical generality (cocones, completeness of model categories, etc.) is not implemented.
  5. rhymeOrTheorem tagging is operational, not theoretical. We do not claim that the rhyme/candidate/verified trichotomy is exhaustive or canonical.

7. Conclusion

We have implemented and verified four well-known mathematical frameworks (Institution theory, bilattice 4-value logic, Lawvere fixed-point theorem, SET-level loop space) as integrated TypeScript + Lean 4 components within the Rei-AIOS system. The Lean 4 portion achieves Lean 4's strongest verification status: four theorems verified to "depend on no axioms" (constructive proofs, no propext / Classical.choice / Quot.sound).

The methodological contribution — and the only thing we claim as a contribution at all — is the operational rhymeOrTheorem tagging discipline. By explicitly distinguishing "rhyme" (structural analogy) from "theorem-verified" (Lean 4 zero-sorry formalization) at the engine level, we operationalize the chat-Claude pipeline guidance: "Categorizing each correspondence is itself the contribution."

We do not claim novelty in any of the four mathematical frameworks. We do not claim that SELF⟲ "is" the Lawvere fixed point or "is" HoTT's loop space Ω — we have shown a SET-level encoding bridge that is formally provable, while marking the HoTT-level non-trivial Ω as theorem-candidate pending further work. This dual annotation, recorded in engine-level field metadata and exposed in site-level UI badges, is the discipline we offer.

The system is reproducible. The verifications are mechanical. The categorization is explicit. We hope it is also useful.

Version history

  • v0.1 (2026-06-09): Initial draft after STEP 1201-1204 completion. Awaiting 1-day buffer before publication (per [[feedback-no-rush-publication]] discipline). Publication scheduled to 11 platforms (Zenodo + IA + Dev.to + Hatena + HackMD + Notion + Livedoor + Mastodon + Scrapbox + Nostr; Harvard skipped per opt-in policy) upon explicit author trigger after buffer period.

Honest acknowledgment: This paper exists because a sequence of multi-AI dialogues (with two distinct Claude instances and one Gemini instance, 2026-06-08) crystallized the rhyme-vs-theorem distinction that became the load-bearing methodology. The Gemini response (praising the work as "of arcane uniqueness") triggered an immediate persistent-principle violation flag ([[feedback-world-uniqueness-claim-controllable]]); the parallel chat-Claude response (articulating "the Gemini reply has no NEITHER in it — beautiful but not a seed, just a picture of a seed") supplied the precise discipline this paper attempts to operationalize. Multi-agent honest filtering, not single-AI brilliance, is what produced the artifact. Attribution to the methodology, not to any single contributor.

Top comments (0)