Module lean 

Lean 4 kernel export (NDJSON 3.1) as an input surface of the LOGOS kernel.

This is one more reader beside term_parser, command_parser and literate_parser: it builds LOGOS kernel terms from Lean’s exported declarations and hands every declaration to the kernel, which re-decides it. The reader is untrusted; its verdicts are the kernel’s. Unsupported declaration families are declined, never counted as invalid proofs. User names are encoded structurally. Nat and quotient identities are reserved and admitted only through their checked canonical declarations.

Modules

emit

LOGOS source for an imported Lean environment: one literate .lg document — prose headings, literate English forms where they express a declaration exactly, kernel vernacular for the rest — plus the correspondence between Lean and LOGOS names. The document is reparsed and rechecked in a fresh context before anyone may publish it.

intake

Intake: the strict front door of a Lean → LOGOS result.

native_decide

native_decide, re-proved by the LOGOS kernel’s own evaluation.

package

The portable proof package (logos-lean-package/1 and /2) and its replay.

pipeline

The Lean → LOGOS pipeline, one named stage at a time, and the benchmark protocol’s dispatch.

receipt

The stages a Lean → LOGOS result passes through, named separately so that no result is ever one unexplained “verified” Boolean (competition rule R1). The names are the contract’s wire names.

reference

The reference translator: a deliberately small, unoptimized reading of a Lean export’s declaration TYPES into kernel terms, sharing no code with the production reader’s conversion, sharing or caching machinery. It is the independent oracle a result’s statement is compared against (competition rule R8): a faulty production translation and a faulty emitter cannot agree with it by construction.

taint

The taint path of every assumption a refused result rests on: the declarations through which the target reaches it.

Structs

DeclarationAudit

ImportReport

ImportRequest

How import_with imports.

ImportedContext

Owned imported artifacts keep the importer’s stack discipline when released.

InternalHelper

Checked conservative definitions introduced to preserve source DAG sharing.

MetadataLoss

Reason

A refusal’s code and message, and where it arose when that is known. Dereferences to the message, so a reason reads as the text the reader has always reported.

RuntimeDeclaration

Source-only runtime metadata. No corresponding axiom or body enters Context.

Enums

DiagnosticCode

Why the reader (or the intake around it) refused. Stable across releases: the wire name is DiagnosticCode::as_str, and a renamed wire name is a protocol break.

Outcome

The outcome of a logos-lean-result/1 document, with the contract’s exit code.

RetainSource

Which checked declarations an import copies out, type and body, beyond what the context keeps. A theorem’s or opaque’s proof is opaque in the context; only retention keeps it.

Verdict

The kernel’s decision on an input it did not accept. Reject: the input is wrong. Decline: the input may be right, but this reader does not accept it (and never approximates it).

Functions

check_str

check_str_with_declaration_audit

check_str_with_report

import

Import the export and return its checked context: no audit, nothing retained, Lean’s binder names carried.

import_audited

import_audited_retaining

Import with the declaration audit, retaining the checked type and body of every named declaration that has one — a target and its dependency closure (intake::Intake::closure). Nothing outside names is copied: retention costs the closure, never the whole environment.

import_audited_retaining_source

Import and additionally retain the checked type and body of one named declaration, including an opaque theorem’s proof. Only that declaration is copied; every other import retains nothing extra.

import_retaining_closure

The pipeline’s import of target: audited, retaining target’s dependency closure, with target as the retained_source.

import_with

Import as request asks. This is LOGOS’s import surface: every native_decide step is read as its re-derivation by kernel evaluation and listed in the report’s native_decisions (native_decide); the Arena protocol (check_str) reads the export exactly as exported.

lean_binder_name

The Lean binder name an imported binder carries, when the import kept one.

lean_type

run_cli

The Lean Kernel Arena benchmark protocol: one input path, ACCEPT on stdout and exit 0 on acceptance, exit 1 on rejection, exit 2 on decline. Kept byte-for-byte for benchmark consumers.