Apoth3osis

Support is Search — Formalized & Refuted

Machine-checked Lean 4 formalization of Gheorghiu's theorem equating Sandqvist-style base-extension support with fuel-bounded proof search for intuitionistic propositional logic — and a compiled refutation proving the standalone implication-forward schema is false on atomic-base kernels.

arXiv:2603.13018v1GitHub
74
Theorems
Machine-checked
3,391
Lines
Lean 4 proof code
11
Modules
Self-contained
0
Sorry
Zero proof holes
0
Axioms
Axiom-free
1
Refutation
imp_forward schema
>_VERIFICATION.SEAL
FORMALLY VERIFIED • LEAN 4 • MACHINE-CHECKED • APOTH3OSIS∀∃⊢→∧∨¬≡QED74 theorems • 0 sorry11 modules0 SORRY

Formal Verification Certificate

Every theorem in this project has been machine-checked by the Lean 4 kernel. No axiom is assumed without proof. No gap exists in the verification chain.

74 THEOREMS VERIFIED11 MODULES3,391 LINES0 SORRY

Support is Search • Lean 4 + Mathlib • Apoth3osis Labs

>_KEY.MATHEMATICS

Main Theorem & Refutation

The paper's central equivalence and our discovery that one direction is provably false.

THEOREM 4.6 (Proved fragment)

Supports⁡  B  φ  ⟺  SearchSupports⁡  (encodeBase⁡  B)  ⟦φ⟧\operatorname{Supports}\;B\;\varphi \iff \operatorname{SearchSupports}\;(\operatorname{encodeBase}\;B)\;\llbracket\varphi\rrbracket

Fully proved for: φ=atom⁡, ⊥, ∧\varphi = \operatorname{atom},\, \bot,\, \wedge. Forward direction proved for ∨\vee. Implication direction: refuted.

REFUTATION (Compiled Lean theorem)

¬  ImpForwardSchema⁡\neg\;\operatorname{ImpForwardSchema}

Witness: B=∅,  φ=(p→q),  ψ=qB = \emptyset,\; \varphi = (p \to q),\; \psi = q for distinct atoms p≠qp \neq q. Root cause: BaseExtends only adds atoms; the paper extends bases by adding arbitrary program clauses.

>_PAPER.PROOF.CORRESPONDENCE

Paper↔Proof Correspondence

Paper SectionProof ModuleStatusNote
Def 3.1 (Bases)Context.leanPROVEDAtomic bases (paper uses programs)
Def 3.3 (Search)Kernel.leanPROVEDFuel-bounded search kernel
Def 4.1 (CPS encoding)Encoding.leanPROVEDCPS translation IPL → Goal
Def 3.5 (Derivation)Derives.leanPROVEDExistential-fresh derivation system
Thm 4.6 (atom case)SemanticSupport.leanPROVEDFull bidirectional bridge
Thm 4.6 (bottom case)SemanticSupport.leanPROVEDFull bidirectional bridge
Thm 4.6 (conjunction)Bridge + SemanticSupportPROVEDBoth directions
Thm 4.6 (disjunction fwd)Bridge.leanPROVEDForward direction
Thm 4.6 (implication fwd)Refutation.leanREFUTEDProvably false on atomic bases
Lemma 4.4 (self-support)Derives.leanPROVEDderives_self_support_atom
Lemma 4.5 (substitution)Derives.leanPROVEDsearch_equivariant
>_PROOF.BLUEPRINT

Proof Modules

Click a module to view its definitions, theorems, and Lean 4 source.

>_DEPENDENCY.GRAPH

Module Dependencies

Hover over a module to trace its imports. The Refutation module imports only Encoding — it is a standalone diagnostic that does not depend on the bridge or semantic layers.

SyntaxIPLKernelContextEncodingDerivesBridgeSemanticSupportSupportMainRefutation
>_VERIFIED.C

Verified C Artifacts

Faithful C transpilations of the computational content. Compiled with gcc -std=c11 -Wall -Wextra.

C

syntax.c

Atom, AtomVar, Goal, Program types and substitution

.c
C

ipl.c

IPL formula inductive and Peirce's formula

.c
C

kernel.c

search/fires/searchAnyAssumption mutual recursion

.c
C

encoding.c

CPS encoding: IPL → Goal

.c
C

context.c

Base, BaseExtends, encodeBase

.c
C

refutation.c

Computational refutation witness verification

.c
Download All C (verified-c.tar.gz)
>_SAFE.RUST

Safe Rust Artifacts

Safe Rust transpilation. 16/16 tests pass, 0 warnings. cargo build && cargo test.

Rs

syntax.rs

Atom, AtomVar, Goal, Program types (3 tests)

.rs
Rs

ipl.rs

IPL formula enum and constructors (2 tests)

.rs
Rs

kernel.rs

search/fires/searchAnyAssumption (3 tests)

.rs
Rs

encoding.rs

CPS encoding with property tests (3 tests)

.rs
Rs

context.rs

Base and BaseExtends (2 tests)

.rs
Rs

refutation.rs

Refutation witness + Peirce non-searchability (3 tests)

.rs
Rs

lib.rs

Crate root module

.rs
Rs

Cargo.toml

Package manifest

.rs
Download All Rust (safe-rust.tar.gz)
>_PROVENANCE.CHAIN

Provenance Chain

1
Paper

Gheorghiu, 'Support is Search' (arXiv:2603.13018v1, March 2026)

2
Lean 4 Proofs

74 theorems, 3,391 lines, 0 sorry — Lean 4 v4.24.0 + Mathlib

3
Refutation

imp_forward_axiom_refuted : ¬ ImpForwardSchema — compiled Lean theorem

4
C Transpilation

6 files, gcc -std=c11 -Wall -Wextra verified

5
Rust Transpilation

6 modules, 16/16 tests pass, cargo build 0 warnings

>_RELATED.LINKS
arXiv:2603.13018v1

Original paper by Gheorghiu

arXiv:2210.05344

Gheorghiu & Pym — Proof-theoretic Validity to B-eS

GitHub Repository

Standalone Lean 4 package — lake build to verify

SUPPORT-IS-SEARCH | PAPER → PROOF → CODE | APOTH3OSIS