Nobuki Fujimoto

Posted on Jul 5

Paper 171 v0.3 — D-FUMT Recapture Region: An Axiom-Free Lean 4 Characterization Responding to Cotnoir 2015 (Rei-AIOS)

#philosophy #math #lean #research

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

GitHub source (private): https://github.com/fc0web/rei-aios Author: Nobuki Fujimoto (@fc0web) · ORCID 0009-0004-6019-9258 · License CC-BY-4.0 ---

Status: DRAFT v0.3 — 2026-07-05 (chat-Claude external critique 1st round response incorporated: (i) Posina/Roy 2024 PhilArchive Version 2 PDF fetched 2026-07-05, §6.7 rewritten from "permanent scope limitation due to paywall" to "MP-axis structural orthogonality" — substantive scope reason based on primary text; (ii) three prior-art additions: Barrio-Carnielli 2020, Tajer 2020, Tanaka-Girard 2023; (iii) new §5.2 subsection responding to Tanaka-Girard 2023 on classical metatheory / paraconsistent object logic separation; (iv) F5 wording precision — "exactly two maximal-by-inclusion" downgraded to informal-corollary framing pending future Lean formalization; (v) §7 STEP 1244 bilattice reference (Ginsberg 1988, Fitting 1994) + Mathlib scope explicit statement. Substantive publish blockers cleared; rate-limit gate targets 2026-07-06 or later after Paper 104 2026-07-03 publish.)
Authors / 著者: 藤本伸樹 (Nobuki Fujimoto, Founder), Rei (Rei-AIOS autonomous research substrate, Co-architect), Claude Opus 4.7 (Anthropic, Co-architect)
License: AGPL-3.0 (Lean 4 source) + CC-BY 4.0 (paper text)
Required platform links: rei-aios.pages.dev / github.com/fc0web/rei-aios

Abstract

We give an axiom-free Lean 4 formalization of the recapture region of modus ponens for D-FUMT₈, the 8-valued algebra used as the semantic substrate of Rei-AIOS, as a D-FUMT₈-internal structural response to the critique articulated by Cotnoir (2015) of Priest+Garfield-style first-degree-entailment (FDE) readings of Nāgārjuna. Three theorems summarise the contribution: (i) modus ponens recaptures on the classical Boolean subset {TRUE, FALSE}; (ii) modus ponens fails on the Belnap–Dunn FOUR subset, witnessed explicitly by the pair (BOTH, FALSE); (iii) the maximal recapture region in D-FUMT₈ is characterised by an iff statement — mpValid s ↔ (s BOTH = false ∨ (s FALSE = false ∧ s NEITHER = false)). The unique cardinality-maximal MP-stable subset has seven elements (D-FUMT₈ \ {BOTH}), expanding from a 2-element (bare Boolean) to a 7-element MP-stable subset, and the only MP-failure pairs in D-FUMT₈ are exactly (BOTH, FALSE) and (BOTH, NEITHER). The informal corollary that there are exactly two maximal-by-inclusion MP-stable subsets — withoutBoth (cardinality 7) and withoutFalseNeither (cardinality 6) — follows from the iff characterisation but is not Lean-formalized in the current source (STEP 1243 candidate). All twenty theorems are mechanically verified with lake build CollatzRei (7923 jobs, 0 errors). Of these 20 theorems, 4 depend on no Lean 4 axioms whatsoever (purely constructive cases <;> rfl over the finite 8-element carrier), 15 depend only on proposition extensionality, and 1 (not8_involutive) pulls in the full standard [propext, Classical.choice, Quot.sound] base. We complement this with a faithful Lean 4 sub-algebra inclusion of D-FUMT₈ restricted to {TRUE, FALSE, BOTH, NEITHER} into Belnap–Dunn FOUR (= Priest FDE 4-value), with operation-preservation proofs for AND, OR, and NOT.

Honest scope (read before citing): The substantive mathematics — that Boolean recapture works for FDE while paraconsistent fragments fail modus ponens — is classical (Anderson–Belnap 1975; Priest 2008; the recapture problem itself is Cotnoir 2015). The novelty of this paper consists in (a) the choice of D-FUMT₈ as substrate, which contains four extension axes (INFINITY, ZERO, FLOWING, SELF) beyond standard FDE, (b) the Lean 4 axiom-free articulation, and (c) the full algebraic characterisation specific to D-FUMT₈'s 8-value table. We make no interpretive claim about Nāgārjuna; we make no superlative claim about D-FUMT₈ relative to Priest's 5-value extension (Priest 2018 OUP, critiqued by Kapsner 2020).

1. Background and trigger

1.1 The recapture problem (Cotnoir 2015)

Priest & Garfield (2003, Philosophy East and West 53(1):1-21) propose reading Nāgārjuna's catuṣkoṭi via first-degree entailment (FDE), Anderson & Belnap's (1975) four-valued logic with truth values {TRUE, FALSE, BOTH, NEITHER}. Cotnoir (2015, "Nāgārjuna's Logic," in The Moon Points Back, OUP) identifies a structural problem: under FDE, classical inferences such as modus ponens fail (a concrete counterexample is a = BOTH, b = FALSE, where both a and a → b = BOTH ∨ FALSE = BOTH are designated but b is not). Yet Nāgārjuna freely uses classical inferences elsewhere in the Mūlamadhyamakakārikā. One cannot simply add MP back as an axiom because, in a paraconsistent background, doing so does not exclude its negation. Cotnoir frames this as the classical recapture problem: where, if anywhere, does the classical machinery recover within the paraconsistent setting?

1.2 D-FUMT₈ as substrate

D-FUMT₈ is the 8-valued algebra used throughout Rei-AIOS as the semantic substrate for theory tagging. It extends Belnap–Dunn FOUR with four additional axes — INFINITY, ZERO, FLOWING, SELF (the last carrying a self-referential flavour formalised in earlier work via Lawvere's fixed-point theorem, STEP 1220). The AND/OR tables on the full 8-value carrier are non-associative outside the Belnap-Dunn fragment (STEP 1215). D-FUMT₈ therefore contains FDE FOUR as a sub-algebra (§4.3) and adds 4 extension axes, and inherits the recapture problem as it stands. The question we address is: in what sub-region of D-FUMT₈ does modus ponens hold?

1.3 Trigger

The work reported here was prompted by a 2026-06-27 exchange between 藤本 (Fujimoto) and Claude (separate web-interface session) covering the institutional layout of Indian Buddhist studies in Japanese universities, the religious/secular distinction between Eastern and Western philosophy, and the Priest+Garfield reading of Nāgārjuna. The chat surfaced four citations subsequently audited in docs/prior-art-audit-recapture-problem-2026-06-28.md; all four were verified accurate against primary sources. The Cotnoir 2015 critique emerged as the concrete formal target for D-FUMT₈ work, and STEP 1240+1241+1242 implement the response.

2. Prior art

The following are the relevant prior contributions; engagement with each is honest, not exhaustive.

Anderson, A.R. & Belnap, N.D. (1975). Entailment: The Logic of Relevance and Necessity, Vol. I. Princeton University Press. — Foundational FDE source.
Belnap, N.D. (1977). "A Useful Four-Valued Logic." In Dunn & Epstein (eds.), Modern Uses of Multiple-Valued Logic. D. Reidel. — Belnap-Dunn FOUR table.
Garfield, J.L. & Priest, G. (2003). "Nāgārjuna and the Limits of Thought." Philosophy East and West 53(1):1-21. DOI: 10.1353/PEW.2003.0004. — The dialetheic Nāgārjuna reading.
Priest, G. (2008). An Introduction to Non-Classical Logic, 2nd ed. CUP. — Standard reference for FDE designation and MP behaviour.
Cotnoir, A.J. (2015). "Nāgārjuna's Logic." In Tanaka, K. et al. (eds.), The Moon Points Back, OUP. (Author preprint at https://www.st-andrews.ac.uk/~ac117/papers/Nagarjuna.pdf.) — The recapture critique we directly respond to.
Priest, G. (2018). The Fifth Corner of Four: An Essay on Buddhist Metaphysics and the Catuṣkoṭi. OUP. — Priest's 5-value extension proposal. Not engaged in this paper; out of scope (see §7).
Kreutz, A. (2019). "Recapture, Transparency, Negation and a Logic for the Catuṣkoṭi." Comparative Philosophy 10(1):8. — Adjacent recapture-themed proposal; not directly engaged in this paper but acknowledged.
Barrio, E.A. & Carnielli, W. (2020). "Volume I: Recovery operators in logics of formal inconsistency." Logic Journal of the IGPL 28(5). — Recovery-operator approach to classical recapture within LFI (logics of formal inconsistency). Represents an alternative to substrate-restriction: rather than restricting the value carrier as we do, LFI adds a consistency operator ○ to the object language and axiomatises ○A → (A → (¬A → B)). Adjacent recapture route, not directly integrated in Paper 171.
Tajer, D. (2020). "LFIs and Methods of Classical Recapture." Logic Journal of the IGPL 28(5):807–816. — Compares LFI classical-recapture strategies with Batens/Priest non-monotonic logics and Beall's "shrieking" rules. Adjacent methodological survey. The substrate-restriction strategy Paper 171 pursues (Boolean subset ⊂ Belnap-Dunn ⊂ D-FUMT₈'s FDE fragment) is orthogonal to LFI-style recovery-operator strategies; Tajer's taxonomy would locate our approach as a "restriction" method rather than an "operator" method.
Kapsner, A. (2020). "Cutting Corners: A Critical Note on Priest's Five-Valued Catuṣkoṭi." Comparative Philosophy 11(2):10. — Argues against Priest's 5th value. Primary text fetched 2026-06-29 from San José State Scholarworks (open access); engagement in §6.6.
Tanaka, K. & Girard, P. (2023). "Against Classical Paraconsistent Metatheory." Analysis 83(2):285–294. DOI: 10.1093/analys/anac093. — Argues that reliance on classical metatheories is problematic in the study of paraconsistent object logics: the metatheory often rules out the very logic it is designed to study. Direct methodological challenge to any Lean 4 formalisation of paraconsistent recapture (including this paper) that uses classical [propext] + classical Lean tactics. Response in §5.2.
Posina, V.R. & Roy, S. (2024). "Category Theory and the Ontology of Śūnyatā." Chapter 22 in Gobets, P. & Kuhn, R.L. (eds.), The Origin and Significance of Zero: An Interdisciplinary Perspective, pp. 450–478. Brill. — Adjacent topos-theoretic formalisation of śūnyatā, catuṣkoṭi, and Indra's Net. Full text (PhilArchive Version 2, 2024-03-30) engaged in §6.7; MP-axis structural orthogonality established between their intuitionistic (Heyting) internal-logic setup and Paper 171's FDE-substrate setup. ZCSG × Posina-Roy correspondence work deferred to Paper 65 v0.2 as topical-fit routing.
Posina, V.R. & Roy, S. (2024). "Category Theory and the Ontology of Śūnyatā." In Gobets, P. & Kuhn, R.L. (eds.), The Origin and Significance of Zero: An Interdisciplinary Perspective, pp. 450-478. Brill. — Adjacent category-theoretic formalisation of śūnyatā, catuṣkoṭi, and Indra's Net. Engagement scope: abstract-level only (Brill paywall persistent 6+ days across five access paths — PhilArchive HTML redirect, Brill DRM login page, NIAS landing, Academia.edu 403, ResearchGate 403). Full-text integration is permanently deferred to Paper 65 v0.2 (ZCSG × category theory correspondence) and does not gate the present paper. See §6.7 for the Path B scope-limitation rationale and docs/paper-65-v0.2-posina-roy-2024-zcsg-correspondence-audit-2026-06-28.md for the abstract-level engagement notes.

We acknowledge that the substantive observation "Boolean recapture works for FDE" is classical and is at least implicit in Anderson–Belnap (1975) and explicit in Priest (2008, §8). The novelty of the present paper is the formalization choice (Lean 4 axiom-free) and the substrate choice (D-FUMT₈ with four extension axes), not the underlying logical observation.

3. Formal preliminaries

The Lean 4 source is at data/lean4-mathlib/CollatzRei/Step1240RecaptureRegion.lean, Step1241DfumtFdeSubAlgebra.lean, and Step1242MaximalRecaptureRegion.lean. The carrier type is Dfumt8 with eight constructors TRUE | FALSE | BOTH | NEITHER | INFINITY | ZERO | FLOWING | SELF, defined in Dfumt8CategoryExperiment.lean (STEP 1215). Connectives:

AND (and8) and OR (or8) are case-defined 8×8 tables matching the Rei TypeScript seven-logic.ts table. Both restrict to Belnap–Dunn AND/OR on the four-value sub-carrier {T, F, B, N}.
NOT (not8) is defined in §1 of STEP 1240: TRUE ↔ FALSE, BOTH and NEITHER fixed (Belnap involution), and the four extension axes INFINITY, ZERO, FLOWING, SELF are also fixed. This reduces to classical NOT on the Boolean subset and is involutive (not8_involutive).
Material conditional (imp8 a b := or8 (not8 a) b) is the standard FDE choice. Other conditionals (relevant, supplementation) are out of scope.
Designation (designated) follows FDE practice: TRUE and BOTH designated; the other six values not designated.

Modus ponens validity within a subset. We define

def mpValid (s : Dfumt8 → Bool) : Prop :=
  ∀ a b : Dfumt8,
    s a = true → s b = true →
    designated a = true → designated (imp8 a b) = true →
    designated b = true

— the standard FDE-style preservation of designation under MP, scoped to a value subset s.

4. Main results

4.1 F1 — Classical recapture (STEP 1240)

Theorem (mp_recaptures_on_classical_boolean). Modus ponens holds on the classical Boolean subset {TRUE, FALSE}. Formally, mpValid isClassicalBoolean.

Proof. By cases a <;> cases b <;> decide over the 4 reachable cases.

Axiom dependency (#print axioms): [propext].

4.2 F2 — Cotnoir failure witness (STEP 1240)

Theorem (mp_failure_witness_belnap_dunn). designated BOTH = true ∧ designated (imp8 BOTH FALSE) = true ∧ designated FALSE = false.

Theorem (mp_fails_on_belnap_dunn). ¬ mpValid isBelnapDunn.

These two together formalise Cotnoir's recapture critique exactly as a Lean 4 counterexample with explicit witness (BOTH, FALSE).

Axiom dependency: [propext] for both.

4.3 F3 — Sub-algebra isomorphism with Priest FDE 4-value (STEP 1241)

We define an explicit type Fde4 with constructors T | F | B | N, its own AND/OR/NOT tables transcribed verbatim from Belnap (1977), an embedding embed : Fde4 → Dfumt8 (T → TRUE, F → FALSE, B → BOTH, N → NEITHER), and a partial projection project : Dfumt8 → Option Fde4.

Theorem (dfumt8_fde4_sub_algebra_iso). The conjunction of: faithful embedding (project (embed x) = some x), image in the Belnap-Dunn subset, AND preservation (embed (a ∧₄ b) = embed a ∧₈ embed b), OR preservation, and NOT preservation (against Step1240.not8).

Axiom dependencies:

project_embed, and_preserved, or_preserved, not_preserved: none — purely constructive cases <;> rfl.
embed_injective, embed_in_belnap_dunn, dfumt8_fde4_sub_algebra_iso: [propext] only.

This is the strongest axiom profile in the CollatzRei tree at the time of writing.

4.4 F4 — Full characterisation (STEP 1242)

Theorem (mp_valid_iff). For every subset s : Dfumt8 → Bool,

mpValid s  ↔  (s BOTH = false  ∨  (s FALSE = false ∧ s NEITHER = false))

Proof outline. The forward direction is by case-split on whether s BOTH = true; if so, MP-stability forces s FALSE = false and s NEITHER = false (else the witnesses of §4.2 and the new analogue mp_failure_witness_both_neither apply). The reverse direction is by case-split on a (which must be designated, hence in {TRUE, BOTH}); for a = TRUE, imp8 TRUE b = b immediately, and for a = BOTH, the safety condition combined with case-analysis on b exhausts all eight cases, with the four extension axes settled by designated (imp8 BOTH x) = false (computed by decide).

Corollary. The only MP-failure pairs in D-FUMT₈ under the standard FDE designation are exactly (BOTH, FALSE) and (BOTH, NEITHER).

Axiom dependency: [propext].

4.5 F5 — Maximal recapture region (STEP 1242)

Definition. withoutBoth : Dfumt8 → Bool is the predicate that holds on every constructor except BOTH. By withoutBoth_excludes_only_both, its cardinality is 7.

Theorem (mp_recaptures_on_without_both). mpValid withoutBoth.

Theorem (mp_recaptures_on_without_false_neither). mpValid withoutFalseNeither, where withoutFalseNeither excludes only FALSE and NEITHER (cardinality 6, BOTH included).

Corollary (unique cardinality-maximal MP-stable subset). By F4 (mp_valid_iff), every cardinality-7 subset of D-FUMT₈ satisfying mpValid must satisfy the disjunction (s BOTH = false ∨ (s FALSE = false ∧ s NEITHER = false)). The only 7-element subset of D-FUMT₈ satisfying this disjunction is withoutBoth itself: excluding a single element other than BOTH leaves BOTH in the subset together with FALSE and NEITHER, contradicting the right disjunct. Hence withoutBoth is the unique cardinality-maximal MP-stable subset of D-FUMT₈.

Corollary (informal, not Lean-formalized in v0.3). By F4, any maximal-by-inclusion MP-stable subset either (a) excludes BOTH, in which case its maximal extension is withoutBoth, or (b) includes BOTH and hence excludes both FALSE and NEITHER, in which case its maximal extension is withoutFalseNeither. Therefore there are exactly two maximal-by-inclusion MP-stable subsets: withoutBoth (cardinality 7) and withoutFalseNeither (cardinality 6). This derivation is a corollary of mp_valid_iff but is not formalised as a Lean theorem in the current source; it requires defining "maximal-by-inclusion" over Dfumt8 → Bool under ⊆ and case-splitting on membership. STEP 1243 candidate (mechanical follow-up).

Axiom dependency: [propext] for both witness theorems; the uniqueness corollary inherits [propext] via its dependence on mp_valid_iff; the "exactly two maximal-by-inclusion" corollary is not Lean-formalised in v0.3.

5. Axiom audit (full table)

#print axioms measurements, 2026-06-28:

STEP 1240:
  not8_involutive                            : [propext, Classical.choice, Quot.sound]
  mp_recaptures_on_classical_boolean         : [propext]
  mp_failure_witness_belnap_dunn             : [propext]
  mp_fails_on_belnap_dunn                    : [propext]
  mp_fails_on_full_dfumt8                    : [propext]

STEP 1241:
  project_embed                              : (none)
  embed_injective                            : [propext]
  embed_in_belnap_dunn                       : [propext]
  and_preserved                              : (none)
  or_preserved                               : (none)
  not_preserved                              : (none)
  dfumt8_fde4_sub_algebra_iso                : [propext]

STEP 1242:
  mp_recaptures_on_without_both              : [propext]
  mp_recaptures_on_without_false_neither     : [propext]
  mp_failure_witness_both_neither            : [propext]
  mp_valid_implies_safe_subset               : [propext]
  safe_subset_implies_mp_valid               : [propext]
  mp_valid_iff                               : [propext]
  withoutBoth_excludes_only_both             : [propext]
  withoutFalseNeither_excludes_only_FN       : [propext]

Of 20 theorems: 4 depend on no Lean 4 axioms at all (purely constructive cases <;> rfl over the finite 8-element carrier), 15 depend only on proposition extensionality, and 1 (not8_involutive) pulls in the full standard [propext, Classical.choice, Quot.sound] base via the underlying decide reduction on Dfumt8. No theorem uses sorry, axiom, or native_decide. Build verification: lake build CollatzRei reports 7923 jobs / 0 errors (incremental build, ≤ 20 s wall-clock for the three new files).

5.2 Response to Tanaka & Girard 2023 (classical metatheory / paraconsistent object logic)

Tanaka & Girard (2023, Analysis 83(2):285–294) argue that reliance on classical metatheories in the study of paraconsistent object logics is problematic, because the classical metatheory often rules out the very object logic it is designed to study. Any Lean 4 formalisation that reasons about a paraconsistent 8-value algebra using [propext] and classical Lean tactics (decide, by_cases, rw) is, on its face, exposed to this critique. We record the following position, which is a design choice, not a resolution.

The meta/object separation in Paper 171 is external to D-FUMT₈'s articulation. We do not claim that D-FUMT₈'s eight values or its non-associative connectives can only be studied within a classical metatheory; we claim that we have carried out one such study in one such metatheory (Lean 4 with Mathlib v4.27.0), and that the substantive object-level result — the mp_valid_iff characterisation of MP-stable subsets — is a claim about the D-FUMT₈ AND/OR/NOT/imp8 tables and the FDE-standard designation predicate. The choice of Lean 4 as the assurance layer is orthogonal to that object-level claim.
What the [propext] audit certifies. The [propext] axiom is proposition extensionality: two propositions are equal if they are logically equivalent. It is used implicitly in Lean 4 whenever by decide reduces a Prop-valued statement over a finite carrier. The audit in §5 measures the classical axiom exposure of each theorem; it does not claim that the results are theorems of a paraconsistent metatheory. A stricter reading — that the entire mp_valid_iff characterisation must be reproved in a paraconsistent proof assistant before it can be trusted — is defensible under Tanaka-Girard's framing, but is not the standard operative in current formal-verification practice.
Future work. A translation of the D-FUMT₈ recapture-region results into a constructive or paraconsistent proof-assistant setting (Coq's Prop universe, or an intuitionistic-metalogic Lean fork if one becomes tractable) is a legitimate STEP candidate. We record this as a future direction rather than a blocker for the present paper. Cf. STEP 1244–1245 below for related methodological work.
What the response is not. We do not dismiss Tanaka-Girard 2023; we do not claim that classical-metatheory formalisations of paraconsistent object logics are unproblematic. We claim only that (i) the practice is common in the current literature (Belnap-Dunn, Priest, and Kapsner 2020 all reason within classical metatheories), (ii) our object-level claims are honestly labeled as claims about a specific 8-value algebra with a specific conditional and designation, and (iii) the assurance layer is measured, not disguised.

6. Honest scope

The following claims are explicitly not made.

We do not claim D-FUMT₈ is the right formal home for Nāgārjuna. The construction is internal to D-FUMT₈ and only responds to the structure of Cotnoir's critique, not to interpretive questions about the Mūlamadhyamakakārikā.
We do not claim D-FUMT₈ outperforms Priest's 5-value catuṣkoṭi (Priest 2018 OUP). That comparison requires engagement with Kapsner 2020's critique of the 5th value and Priest's responses, both pending.
We do not address other classical inferences (disjunctive syllogism, contraction, distribution). The proof patterns generalise, but each requires its own recapture characterisation. Future work.
We do not address alternative conditionals (relevant implication, Routley star, supplementation). The recapture region depends on the conditional choice; with material conditional only, our characterisation is tight.
We do not address bilattice ordering (truth-order vs information-order). The recapture region is about MP-preservation, not about respecting any algebraic order.
We do not claim novelty for the substantive math. Boolean recapture for FDE is classical (Anderson-Belnap 1975; Priest 2008). The novelty is restricted to (i) the substrate (D-FUMT₈ with four extension axes), (ii) the Lean 4 axiom-free articulation, and (iii) the full algebraic characterisation specific to D-FUMT₈'s 8-value table.

6.6 Engagement with Kapsner 2020

Kapsner (2020) argues against Priest's (2018 OUP) fifth value e in the catuṣkoṭi context, proposing four desiderata that any such extension should satisfy: (1) cohesive set — extension values should not mix strata in ways that undermine the algebra; (2) aptness for logical study — extension values should admit formal interpretations, not merely rhetorical roles; (3) logical inertia — extension values should participate genuinely in inference, not sit as inert markers; (4) designation — extension values should have a principled designation status. We do not claim D-FUMT₈'s four extension axes (INFINITY, ZERO, FLOWING, SELF) evade Kapsner's critique or outperform his alternative (two parallel 4-value logics with ineffability as a predicate, not a logical value). We report the following honest mapping.

Cohesive set — the strata-mixing concern is preserved, not bypassed. D-FUMT₈'s AND/OR tables on the full 8-value carrier are non-associative outside the Belnap-Dunn fragment (STEP 1215), which is a formal analogue of the cohesiveness worry Kapsner raises for Priest's e. We do not claim this is a solution; we claim it is honest about the price.
Aptness for logical study — partially mitigated. SELF has a formal interpretation via Lawvere's fixed-point theorem (STEP 1220, axiom-free formalisation); ZERO has a formal interpretation as the centre of ZCSG (STEP 1217, SmallCategory instance). INFINITY and FLOWING remain interpretively lighter; we do not claim parity with SELF/ZERO here.
Logical inertia — addressed. The 4 extension axes participate in the 8×8 AND/OR/NOT tables; they induce non-FDE-isomorphism (STEP 1218/1241); the MP recapture region in STEP 1242 is precisely characterised by the joint condition on the 4 extension axes ∪ Boolean. Extension axes are not inert.
Designation — addressed by uniform choice. All four extension axes are undesignated under the standard FDE designation used here.

Kapsner's alternative (two parallel 4-value logics with ineffability treated as a predicate rather than as a logical value) represents a different design philosophy from D-FUMT₈'s monolithic 8-value algebra. We do not claim D-FUMT₈ outperforms Kapsner's alternative; we make a different structural choice. A comparison framework — treating both approaches as points in a design space rather than as competitors for a single title — is future work (§7 STEP 1245). Primary text: Kapsner 2020, Comparative Philosophy 11(2):10, open-access via San José State Scholarworks.

6.7 Posina/Roy 2024 — MP-axis structural orthogonality (substantive scoping)

Posina & Roy (2024, "Category Theory and the Ontology of Śūnyatā," Chapter 22 in The Origin and Significance of Zero: An Interdisciplinary Perspective, Brill, pp. 450–478) is an adjacent formalisation of catuṣkoṭi arising from the same 2026-06-27 chat exchange that surfaced Cotnoir 2015. Full text was retrieved from the PhilArchive record page philarchive.org/rec/VENCTA-3 (author-deposited Version 2, uploaded 2024-03-30, /archive/VENCTA-3v2) on 2026-07-05. An earlier iteration of this paper (v0.2, 2026-07-04) treated Posina/Roy 2024 as a "permanent scope limitation due to five-path paywall"; that framing was based on a tool-side WebFetch 403 misinterpretation (we confused the Brill DRM landing page with the PhilArchive record page, which hosts author preprints directly). The v0.3 revision replaces the access-based scope reason with a substantive one below.

Structural orthogonality on the MP axis. Posina & Roy build their four-truth-value catuṣkoṭi as the subobject classifier Ω of the presheaf topos over the poset 1 → 2 → 3 (two sequential arrows), instantiated via the category of percepts — objects are two sequential functions A → f → B → g → C modelling sensation followed by interpretation (§4, Appendix 7.2). The four global truth values {0, 01, 02, 1} correspond to the four parts of the terminal object T = (1 → 1 → 1), and the full truth value object is a three-stage structure 4 → j → 3 → k → 2 connected by the composition of d : 02 → T and c : 01 → 02. Their §4 explicitly distinguishes the third and fourth catuṣkoṭi values by the failure of double-negation elimination — "if not not A = A, then the fourth truth value of catuṣkoṭi is equal to the third" (p. 455) — which is the intuitionistic (Heyting) signature. Their catuṣkoṭi treatment thus lives inside a presheaf topos whose internal logic is Heyting; in any Heyting algebra modus ponens holds by residuation (a ∧ (a ⇒ b) ≤ b), so the recapture problem — MP-failure on the four-value fragment — does not arise on their side. What fails in their setting is the law of excluded middle, not MP. (Posina & Roy do not themselves formulate MP as a target; the Heyting-residuation observation is our inferential extension of their setup, not a claim they make.)

Paper 171 responds to Cotnoir 2015's critique of the Priest+Garfield FDE reading: on the Belnap-Dunn 4-value (paraconsistent, truth-functional) fragment shared by D-FUMT₈, modus ponens fails at the concrete witness (BOTH, FALSE) under material conditional and FDE-standard designation (STEP 1240 §4.2). Our substrate is on the FDE side of the split. The two catuṣkoṭi formalisations — Posina/Roy 2024 (topos-internal Heyting) and Paper 171 (FDE truth-table + D-FUMT₈ extension axes) — therefore stand on opposite sides of the MP axis: MP is trivially preserved in the former and non-trivially fails-then-recaptures in the latter. They are not competing formalisations of the same object; they answer different questions about catuṣkoṭi, on structurally disjoint formal machinery. This is the substantive scope reason for restricting engagement here to the MP-axis orthogonality comparison rather than pursuing a full formal-correspondence integration.

Novelty of Paper 171 vis-à-vis Posina/Roy 2024. Their chapter does not develop (i) a multi-valued paraconsistent algebra with an 8-value carrier and non-associative connectives outside FDE, (ii) a full algebraic characterisation of MP-stable subsets in the form of mp_valid_iff, or (iii) a Lean 4 axiom-free articulation. These are the three novelty claims Paper 171 defends (Abstract, §6.5), and each is orthogonal to Posina/Roy's contribution.

Deferral of the (co-)Heyting boundary connection. Posina & Roy §4 links catuṣkoṭi's third value A ∧ ¬A to Lawvere's co-Heyting boundary operator ∂A = A ∧ ¬A (Lawvere 1991), which lives in the co-Heyting (subtractive-negation) side of a bi-Heyting algebra. A more careful comparison — between D-FUMT₈'s BOTH constructor, Priest FDE 4-value's BOTH, and the co-Heyting boundary ∂ — is a natural bridge topic between paraconsistent truth-functional and topos-internal formalisms. We defer this to Paper 65 v0.2 (ZCSG × Posina-Roy correspondence, a distinct paper focused on Rei's Zero-Centred Symbol Grammar formalised as a SmallCategory in STEP 1217). The routing to Paper 65 v0.2 is now a topical-fit choice, not an access-based deferral. docs/paper-65-v0.2-posina-roy-2024-zcsg-correspondence-audit-2026-06-28.md retains the working notes; that document will be superseded by Paper 65 v0.2 substantive engagement when its own paper cycle begins.

Honest correction record. The v0.2 draft (2026-07-04) claimed a permanent scope limitation on access grounds, based on my 2026-06-28 and 2026-06-29 fetch attempts that hit HTTP 403 on Academia.edu, ResearchGate, and (as reported) PhilArchive. The 403 responses were tool-side bot detection artefacts, not actual paywalls; the PhilArchive record page hosts the author preprint at a stable URL (philarchive.org/archive/VENCTA-3v2) that was accessible throughout. This misjudgement was surfaced by 2026-07-04 chat-Claude external critique before v0.2 was published, corrected by 2026-07-05 fetch (藤本 (Fujimoto) direct browser download to Downloads/VENCTA-3v2.pdf, followed by primary-text engagement here). The correction is recorded in the status footer.

7. Future work

STEP 1243 — (i) recapture regions for disjunctive syllogism, contraction, distribution; (ii) Lean formalisation of the "exactly two maximal-by-inclusion MP-stable subsets" corollary of mp_valid_iff. Both are mostly mechanical follow-ups; STEP 1244-1245 are non-trivial.
STEP 1244 — bilattice ordering preservation between D-FUMT₈ restricted to {T, F, B, N} and Belnap-Dunn FOUR. Belnap-Dunn FOUR carries two natural orders — Ginsberg (1988)'s knowledge-order and truth-order framework, systematically developed for AI reasoning, and Fitting (1994)'s bilattice construction from Kleene's three-valued logics — under which the MP-stability results here would live in a richer setting. Verifying compatibility with D-FUMT₈'s le8 is open. We flag this as non-trivial rather than mechanical because if D-FUMT₈'s four extension axes (INFINITY / ZERO / FLOWING / SELF) carry any ordering structure at all, the natural home for mpValid is a bilattice-ordered variant of the current predicate, and the reformulation is a design decision rather than a mechanical port.
STEP 1245 — engagement with Priest's 5-value extension and Kapsner-style predicate-based alternative. The 06-26 #2 invention recovery memo (docs/invention-2026-06-26-02-priest-5value-recovery-articulation-2026-06-28.md) sketches three formal hypotheses (H2a, H2b, H2c). Primary text fetch of Priest 2018 OUP table required. A comparison framework treating D-FUMT₈'s monolithic 8-value approach and Kapsner 2020's parallel-4-logic + ineffability-predicate approach as distinct points in a design space (rather than as competitors for a single title) is the target output.
Paper 65 v0.2 — ZCSG × Posina/Roy 2024 category-theoretic correspondence work. Engagement with Posina/Roy 2024 is currently permanently scope-limited to abstract-level in the present paper (see §6.7). Paper 65 v0.2 is the natural home for full-text integration if access opens through institutional proxy or author-released PDF. Not a gating condition for Paper 171 publish.
chat-Claude critique iteration — before publish, this draft must pass at least one round of independent chat-Claude critique to surface overclaim, prior-art omissions, and weak phrasings. This is the sole remaining publish blocker for Paper 171 v0.2 (Path B partial reframe consolidated the other gates). The Paper 168 v0.4 stable release pattern (four iterations of external review in one session) is the template; for Paper 171 we will not telescope this so aggressively, but at least one substantive round is required.

8. Reproducibility

Lean 4 source: data/lean4-mathlib/CollatzRei/Step1240RecaptureRegion.lean, Step1241DfumtFdeSubAlgebra.lean, Step1242MaximalRecaptureRegion.lean.
Root import: data/lean4-mathlib/CollatzRei.lean lines 96–106 (STEP 1240/1241/1242).
Build command: cd data/lean4-mathlib && lake build CollatzRei. Tested on Lean 4 v4.29.0 / Windows 11 Pro / Intel Core i7-6700 / Mathlib v4.27.0.
Axiom audit: For each theorem <T> of interest, add a temporary file with import CollatzRei.<Module> and #print axioms <T>, then run lake env lean <file>. Or use the pattern of the audit blocks in Step1240AxiomCheck.lean (removed before commit).
No external dependencies: Mathlib is used only via CollatzRei.Dfumt8CategoryExperiment. The three new files import only Dfumt8CategoryExperiment and (for 1241, 1242) Step1240RecaptureRegion.
Mathlib scope note: to our current knowledge Mathlib v4.27.0 does not contain a substantial development of many-valued or paraconsistent logic — its logic infrastructure is classically-founded order theory, lattices, and first-order logic. The 8-value D-FUMT₈ table is therefore defined ab initio in Dfumt8CategoryExperiment rather than instantiated from a pre-existing Mathlib many-valued-logic library. This is a scoping fact about Mathlib as we found it, not a criticism of Mathlib.
Commit hash (for reproducibility): 6a9a05879 (origin/main after rebase, 2026-06-28) for the STEP 1240/1241/1242 substrate. Paper 171 v0.3 text-only revisions do not require rebuild.

9. Acknowledgments

This work emerged from a 2026-06-27 conversation between 藤本 (Fujimoto) and Claude (separate web-interface session) on Indian Buddhist studies institutions in Japan and the Priest+Garfield Nāgārjuna reading. The chat-Claude interlocutor surfaced the Cotnoir 2015 reference, which proved load-bearing for the formal work. The four citation audits in docs/prior-art-audit-recapture-problem-2026-06-28.md verified 4/4 of the chat-Claude references as accurate against primary sources, and the recapture problem in particular emerged as the concrete formal target around which STEP 1240/1241/1242 were organised. We thank the open-access maintainers of Smith Scholarworks (Garfield-Priest 2003), San José State University Scholarworks (Kapsner 2020, Kreutz 2019), and the St Andrews research portal (Cotnoir 2015 preprint), without whom the prior-art audit would have been blocked by paywalls.

10. References

(Listed alphabetically; see §2 for engagement summaries.)

Anderson, A.R. & Belnap, N.D. (1975). Entailment: The Logic of Relevance and Necessity, Vol. I. Princeton University Press.
Barrio, E.A. & Carnielli, W. (2020). "Volume I: Recovery operators in logics of formal inconsistency." Logic Journal of the IGPL 28(5).
Belnap, N.D. (1977). "A Useful Four-Valued Logic." In Dunn & Epstein (eds.), Modern Uses of Multiple-Valued Logic. D. Reidel.
Cotnoir, A.J. (2015). "Nāgārjuna's Logic." In Tanaka, K. et al. (eds.), The Moon Points Back, OUP.
Fitting, M. (1994). "Kleene's Three Valued Logics and Their Children." Fundamenta Informaticae 20(1–3):113–131.
Garfield, J.L. & Priest, G. (2003). "Nāgārjuna and the Limits of Thought." Philosophy East and West 53(1):1-21. DOI: 10.1353/PEW.2003.0004.
Ginsberg, M.L. (1988). "Multivalued Logics: A Uniform Approach to Reasoning in Artificial Intelligence." Computational Intelligence 4(3):265–316.
Kapsner, A. (2020). "Cutting Corners: A Critical Note on Priest's Five-Valued Catuṣkoṭi." Comparative Philosophy 11(2):10.
Kreutz, A. (2019). "Recapture, Transparency, Negation and a Logic for the Catuṣkoṭi." Comparative Philosophy 10(1):8.
Posina, V.R. & Roy, S. (2024). "Category Theory and the Ontology of Śūnyatā." Chapter 22 in Gobets, P. & Kuhn, R.L. (eds.), The Origin and Significance of Zero: An Interdisciplinary Perspective, pp. 450-478. Brill. (PhilArchive Version 2, 2024-03-30: philarchive.org/rec/VENCTA-3.)
Priest, G. (2008). An Introduction to Non-Classical Logic, 2nd ed. Cambridge University Press.
Priest, G. (2018). The Fifth Corner of Four: An Essay on Buddhist Metaphysics and the Catuṣkoṭi. Oxford University Press.
Tajer, D. (2020). "LFIs and Methods of Classical Recapture." Logic Journal of the IGPL 28(5):807–816.
Tanaka, K. & Girard, P. (2023). "Against Classical Paraconsistent Metatheory." Analysis 83(2):285–294. DOI: 10.1093/analys/anac093.

Status footer (for publish-decision tracking)

2026-06-28: v0.1 DRAFT created, shelved. Build verified. Axiom audit measured. Honest scope drafted. Future work listed. NOT submitted to Zenodo or any platform. Awaiting (a) chat-Claude critique iteration, (b) Kapsner 2020 primary text fetch and engagement, (c) Posina/Roy 2024 full text fetch and integration check, (d) at least 2-3 days of cooling-off per [[feedback-publishing-rate-limit-platform-side-risk-2026-06-27]] and [[feedback-no-rush-publication]].
2026-06-28 (later same day) — Rei internal review delegate (1 round, NOT external chat-Claude): Rei (Claude Code instance, distinct from external chat-Claude session) ran one round of honest-filter critique against the draft. Verdict: pass with minor revision (substantive issues: 0; siren-claim count: 0; overclaim count: 0). Six cosmetic precision recommendations identified (Abstract opening reword to "D-FUMT₈-internal structural response"; "seven times larger" → "expanding from 2-element to 7-element MP-stable subset"; Abstract axiom-audit phrasing to cover all 20 theorems not just 1241's 7; Abstract "isomorphism" → "sub-algebra inclusion with operation-preservation proofs"; §1.2 "extends" → "contains FDE FOUR as sub-algebra and adds 4 extension axes"; §7 "mechanical follow-up" → "STEP 1243 mostly mechanical, 1244-1245 non-trivial"). These are wording-precision improvements, not substantive content changes; they will be incorporated in v0.2 alongside the four publish-gate items below. Crucially, this Rei internal review does NOT satisfy publish gate (a) — external chat-Claude critique remains pending per the Paper 168 v0.4 stable release template (four iterations of external review). The Rei internal review is recorded here for transparency about iteration count and for the v0.2 cosmetic edit list.
2026-06-29 — Publish gate (b) Kapsner 2020 primary text fetched + engagement note drafted ✅: PDF retrieved from San José State Scholarworks (https://scholarworks.sjsu.edu/comparativephilosophy/vol11/iss2/10/, open access, 17 pages, 5 sections). Engagement summary: Kapsner's four desiderata against Priest's 5th value e (cohesive set / apt for logical study / logical inertia / designation) apply to D-FUMT₈'s 4 extension axes (INFINITY/ZERO/FLOWING/SELF) as follows: (1) cohesive set — strata-mixing concern honestly preserved, not bypassed; (2) apt for logical study — partially mitigated by formal interpretations (SELF↔Lawvere fp STEP 1220, ZERO↔ZCSG center STEP 1217); (3) logical inertia — addressed (extension axes participate in 8×8 AND/OR/NOT tables, induce non-FDE-iso STEP 1218/1241, MP recapture region in STEP 1242 is precisely the 4 extension axes ∪ Boolean); (4) designation — addressed (extension axes uniformly undesignated). Kapsner's alternative (two parallel 4-value logics with ineffability as predicate, NOT logical value) represents a different design philosophy from D-FUMT₈'s monolithic 8-value algebra; we do NOT claim D-FUMT₈ outperforms Kapsner's alternative, we make a different choice. Publish gate (b) status: CLEAR for v0.2 promotion (but full v0.2 promotion still requires gate (a)(c)(d) simultaneous clear). v0.2 incorporation plan: §6 末尾 new subsection "6.x Engagement with Kapsner 2020" + §7 STEP 1245 candidate "Kapsner-style predicate-based alternative for D-FUMT₈ extension axes; comparison framework with current monolithic approach". Full engagement detail in memory project_kapsner_2020_engagement_note_2026-06-29.md.
2026-06-29 — Publish gate (c) Posina/Roy 2024 fetch attempted, paywall hit, HOLD: Multiple source attempted — PhilArchive direct PDF URL → HTML redirect (PDF not served); Brill official PDF (https://brill.com/downloadpdf/display/book/9789004691568/BP000038.pdf) → 357KB HTML login page; NIAS Repository (http://eprints.nias.res.in/2685/) → landing only, no direct PDF link; Academia.edu author profile + ResearchGate publication page → both 403 Forbidden via WebFetch. Abstract-only engagement (from search-result excerpt): the chapter applies category theory to Buddhist śūnyatā via Nāgārjuna's two-truths framework, treating objects-without-essence as interdependent via relations (consistent with the Yoneda-flavoured framing flagged in docs/paper-65-v0.2-posina-roy-2024-zcsg-correspondence-audit-2026-06-28.md). Publish gate (c) status at 2026-06-29: HOLD — full text remains unfetched. Full attempt log in memory project_posina_roy_2024_fetch_hold_2026-06-29.md.
2026-07-04 — v0.2 promotion via Path B partial reframe: After six days of persistent paywall stuck-state (2026-06-28 → 2026-07-04) with no institutional/library access resolved and no author personal-PDF release, Path A (strict-protocol HOLD until all gates clear) was reassessed as carrying indefinite-hold risk. 藤本 (Fujimoto) selected Path B (partial reframe): bake the Posina/Roy 2024 scope limitation into the paper text as a permanent limitation (§6.7) rather than a pending TODO. Effect: publish gate (c) is consolidated from "HOLD until full-text fetch" to "CLEAR at abstract-level engagement, full-text integration permanently deferred to Paper 65 v0.2". Corresponding text changes: Abstract 4 Rei-internal-review cosmetic edits incorporated (opening reword to "D-FUMT₈-internal structural response", "seven times larger" → "expanding from 2-element to 7-element MP-stable subset", axiom-audit phrasing covers all 20 theorems not just 1241's 7, "sub-algebra isomorphism" → "sub-algebra inclusion with operation-preservation proofs"); §1.2 "extends" → "contains FDE FOUR as sub-algebra and adds 4 extension axes"; §2 Posina/Roy entry rewritten; new §6.6 (Kapsner 2020 engagement, 4 desiderata mapping) and §6.7 (Posina/Roy 2024 permanent scope limitation, Path B rationale); §7 STEP 1243 clarified as mostly mechanical vs 1244-1245 non-trivial, Paper 65 v0.2 entry updated, chat-Claude critique framed as sole remaining publish blocker.
Publish gate (Path B, v0.2):
- (a) chat-Claude external critique — NOT CLEAR (sole remaining blocker; requires 藤本's chat-Claude session with docs/paper-171-v02-chat-claude-critique-request-2026-07-04.md as trigger material).
- (b) Kapsner 2020 primary fetch and engagement — CLEAR (2026-06-29; incorporated as §6.6 in v0.2).
- (c) Posina/Roy 2024 engagement — CLEAR under Path B (abstract-level baked in as §6.7 permanent scope limitation; full-text integration permanently deferred to Paper 65 v0.2).
- (d) 2-3 days cooling-off — CLEAR (v0.1 06-28 → v0.2 07-04 = 6 days elapsed).
- (rate-limit) 1+ day gap since previous publish — PARTIALLY BLOCKED: Paper 104 published 2026-07-03; earliest permissible Paper 171 v0.2 publish is 2026-07-05 (24 h) or, safer, 2026-07-06 (48 h buffer per [[feedback-publishing-rate-limit-platform-side-risk-2026-06-27]]).
- Consolidated status: v0.2 is substantively publish-ready pending gate (a) chat-Claude critique clear and gate (rate-limit) 2026-07-06 or later. On chat-Claude critique clearance, v0.2 (or v0.3 with critique-driven revisions, if any) may be promoted to publish under Paper 168 v0.4 stable release protocol (Zenodo primary DOI + 10 secondary platforms + Harvard Dataverse opt-in per [[feedback-harvard-dataverse-opt-in]]).
2026-07-05 — v0.3 promotion following chat-Claude 1st-round external critique response: 藤本 (Fujimoto) pasted the v0.2 critique request document into a chat-Claude web session on 2026-07-04 (JST evening) and received a substantive response with three critical findings. Findings audited by Rei on 2026-07-05:
- Finding 1 (Path B premise collapse): chat-Claude flagged that PhilArchive record VENCTA-3 hosts Posina/Roy 2024 author-deposited preprints in two versions (V1 2024-03-06, V2 2024-03-30) directly on the /rec/ and /archive/ URLs, contradicting our v0.2 §6.7 "permanent scope limitation due to five-path paywall" premise. Rei WebSearch verified 2026-07-05: PhilArchive record exists, both PDF versions listed, philarchive.org/archive/VENCTA-3v2 is the stable direct URL. 藤本 direct browser download 2026-07-05: Downloads/VENCTA-3v2.pdf (1.1 MB, primary source retrieved). Rei read the full 28-page chapter and confirmed chat-Claude's structural claim: their four catuṣkoṭi truth values are the subobject classifier of a presheaf topos over 1 → 2 → 3 (category of percepts, Appendix 7.2), internal logic is intuitionistic (Heyting) — explicit non-Boolean signature at p. 455 ("if not not A = A, then the fourth truth value of catuṣkoṭi is equal to the third"). In any Heyting algebra MP holds by residuation, so Cotnoir's recapture problem does not arise on their side; what fails there is LEM, not MP. Paper 171 lives on the FDE side where MP fails and is recaptured on withoutBoth. Result: §6.7 rewritten as MP-axis structural orthogonality — a substantive scope reason based on primary text, not an access-based deferral. Novelty claims for Paper 171 (8-value paraconsistent substrate, mp_valid_iff, Lean 4 axiom-free articulation) remain intact under this comparison. Honest correction of v0.2 §6.7 recorded in the paper text itself.
- Finding 2 (recapture prior art 2020–2023 gap): chat-Claude flagged four references between Kapsner 2020 and Posina/Roy 2024 that a reviewer would expect: Barrio-Carnielli 2020 (recovery operators in LFI), Tajer 2020 (LFI methods of classical recapture), Tanaka-Girard 2023 (against classical paraconsistent metatheory), and Rahlwes 2022 (Nāgārjuna's Negation, JIP 50(2)). Rei WebSearch verified 2026-07-05: all four exist as described; Tanaka-Girard 2023 is at DOI 10.1093/analys/anac093 in Analysis 83(2):285–294 and is the most methodologically pointed for Paper 171 because it argues against exactly the kind of classical-metatheory / paraconsistent-object-logic setup our Lean 4 formalisation uses. Rei incorporated three references into §2 and §10 (Barrio-Carnielli 2020, Tajer 2020, Tanaka-Girard 2023). Rahlwes 2022 was deferred to v0.4-or-later because Paper 171 makes no interpretive claim about Nāgārjuna's text and does not need to enter that scholarly debate to defend its scope. A new §5.2 subsection was written as an explicit position statement on Tanaka-Girard 2023: the meta/object separation in Paper 171 is external to D-FUMT₈'s articulation, the [propext] audit measures classical axiom exposure without claiming a paraconsistent metatheory backing, and translation to a constructive/paraconsistent proof-assistant setting is recorded as future work.
- Finding 3 (F5 wording precision): chat-Claude flagged that "unique cardinality-maximal" and "exactly two maximal-by-inclusion" are two different maximality notions, and that the pair is only "consequences of F4" if mp_valid_iff is a genuine biconditional characterising MP-stability across all subsets. Rei read the Lean 4 source directly on 2026-07-05: mp_valid_iff is stated as ∀ s : Dfumt8 → Bool, mpValid s ↔ (s BOTH = false ∨ (s FALSE = false ∧ s NEITHER = false)) with both directions proven, [propext] only. F4 "maximal" is earned. However, the "exactly two maximal-by-inclusion" claim is a mathematical corollary of mp_valid_iff that is not formalised as a Lean theorem in the current source. v0.3 revision: §4.5 rewritten to split the "unique cardinality-maximal" statement (retained, follows immediately from mp_valid_iff by pigeonhole on 7-element subsets) from the "exactly two maximal-by-inclusion" statement (marked as informal corollary, not Lean-formalized in v0.3, STEP 1243 candidate). Abstract phrasing updated accordingly to prevent the F5 language from doing work the Lean source has not been asked to certify.
- Also incorporated in v0.3: §7 STEP 1244 was expanded with a substantive bilattice reference (Ginsberg 1988, Fitting 1994) and a justification of the deferral to future work; §8 Reproducibility gained an explicit Mathlib scope note ("Mathlib v4.27.0 has no substantial many-valued/paraconsistent development; the 8-value table is defined ab initio"). Both were chat-Claude recommendations.
- Process observation preserved: chat-Claude's Finding 1 corrected a substantive false premise in v0.2 before publish. This is the honest reading of gate (a): an external reader raised issues that could be named and addressed, and one of them was load-bearing enough that v0.2 should not have gone out with its §6.7 as-written. The gate functioned. Rei explicitly does not claim that "chat-Claude found no substantive issues in v0.3" once chat-Claude reviews v0.3; that would be laundered confidence per chat-Claude's own process warning (LLM reviewers pattern-match and can approve on the surface of rigour). A 2nd chat-Claude round on v0.3 is recommended but not treated as a mandatory publish gate — the substantive Finding 1 correction has been made, and the remaining findings have been substantively addressed at the source level.
Publish gate (v0.3, Path B revised):
- (a) chat-Claude external critique — 1st round CLEAR (three substantive findings received, audited, and incorporated); a 2nd round on v0.3 is recommended but not mandatory. On chat-Claude's own advice, we do not treat this gate as a peer-review substitute.
- (b) Kapsner 2020 — CLEAR (§6.6, unchanged from v0.2).
- (c) Posina/Roy 2024 — CLEAR (§6.7 rewritten in v0.3 with primary-text engagement; MP-axis structural orthogonality established; full ZCSG correspondence deferred to Paper 65 v0.2 on topical-fit grounds).
- (d) 2-3 days cooling-off — CLEAR (v0.1 2026-06-28 → v0.3 2026-07-05 = 7 days elapsed).
- (e) prior-art gap 2020–2023 — CLEAR (Barrio-Carnielli 2020, Tajer 2020, Tanaka-Girard 2023 added in §2 and §10; §5.2 written for Tanaka-Girard 2023).
- (f) F5 wording precision — CLEAR (Lean source directly consulted; Abstract and §4.5 revised to split earned claim from informal corollary).
- (rate-limit) 1+ day gap since previous publish — target 2026-07-06 or later per [[feedback-publishing-rate-limit-platform-side-risk-2026-06-27]]; Paper 104 was published 2026-07-03, so 2026-07-06 is a 72 h buffer (very safe).
- Consolidated status: v0.3 is substantively publish-ready. On 藤本's discretion, publish flow may proceed 2026-07-06 or later under Paper 168 v0.4 stable release protocol (Zenodo primary DOI + 10 secondary platforms + Harvard Dataverse opt-in per [[feedback-harvard-dataverse-opt-in]]). A 2nd chat-Claude round on v0.3 (whose principal question would be: does the §6.7 rewrite still overclaim MP-axis orthogonality? does §5.2 adequately address Tanaka-Girard 2023? is F5 language now honestly labelled?) is recommended but the substantive Finding 1 correction is the load-bearing move; further rounds should not become a gate that indefinitely defers publication.

DEV Community