# logicaffeine_kernel

> Calculus of Constructions proof kernel with inductive types, universes, quotients, a second checker and Lean 4 import

Every public module and item of `logicaffeine_kernel`, module by module, each with its one-line summary and its address. Item pages hold the full signature, documentation, trait implementations and a link to the source.

- Crate page: [logicaffeine_kernel](https://docs.logicaffeine.com/logicaffeine_kernel/)
- All items on one page: [logicaffeine_kernel/all](https://docs.logicaffeine.com/logicaffeine_kernel/all)
- Source: [src/logicaffeine_kernel/lib.rs](https://docs.logicaffeine.com/src/logicaffeine_kernel/lib.rs)
- Every crate: [llms.txt](https://docs.logicaffeine.com/llms.txt)

## logicaffeine_kernel

- [mod bitvector](https://docs.logicaffeine.com/logicaffeine_kernel/bitvector/): Bitvector reflection-symmetry decision procedure.
- [mod cc](https://docs.logicaffeine.com/logicaffeine_kernel/cc/): Congruence Closure Tactic
- [mod certificate](https://docs.logicaffeine.com/logicaffeine_kernel/certificate/): Independently re-checkable proof certificates — the De Bruijn criterion.
- [mod dag](https://docs.logicaffeine.com/logicaffeine_kernel/dag/): The kernel core: a type theory over a hash-consed expression DAG, in two modes (`tc::Theory`): Lean 4’s theory exactly, and LOGOS’s Calculus of Inductive Constructions.
- [mod elaborate](https://docs.logicaffeine.com/logicaffeine_kernel/elaborate/): R4 — the elaborator: metavariables, unification, and implicit-argument inference.
- [mod equations](https://docs.logicaffeine.com/logicaffeine_kernel/equations/): Equation lemmas — Lean’s `f.eq_def`, `f.eq_1 … f.eq_n` — the NAME a proof cites when it appeals to a definition’s behaviour, which is what `rw [f]` / `simp [f]` / `unfold f` all need.
- [mod eval](https://docs.logicaffeine.com/logicaffeine_kernel/eval/): A call-by-value evaluator for the kernel’s computational fragment — the engine behind `native_decide`.
- [mod field_algebra](https://docs.logicaffeine.com/logicaffeine_kernel/field_algebra/): Kernel algebra for the prime field 𝔽_q of ML-KEM / ML-DSA — the certified arithmetic substrate (F2 seed).
- [mod inductive_compile](https://docs.logicaffeine.com/logicaffeine_kernel/inductive_compile/): Nested-inductive compiler (K3) — the UNTRUSTED front-end for inductives that recur nested inside a container, `RTree := rnode : TList RTree → RTree`.
- [mod int_inductive](https://docs.logicaffeine.com/logicaffeine_kernel/int_inductive/): `Int` as a real inductive — Lean’s `ofNat | negSucc` with its arithmetic defined rather than assumed (`Init/Data/Int/Basic.lean:40-45`, `:78-166`). The construction, packaged so the prelude adopts it in one call; the module header carries how Lean keeps it fast anyway. `Int` as a REAL INDUCTIVE — Lean’s `ofNat | negSucc`, with its arithmetic DEFINED.
- [mod interface](https://docs.logicaffeine.com/logicaffeine_kernel/interface/): Vernacular interface for the Kernel.
- [mod lia](https://docs.logicaffeine.com/logicaffeine_kernel/lia/): Linear Integer Arithmetic via Fourier-Motzkin Elimination
- [mod observational](https://docs.logicaffeine.com/logicaffeine_kernel/observational/): Certified universe-polymorphic quotient primitives. Observational equality: `Obs.{u} A a b : SProp`, an equality over every type that computes on the weak-head normal form of `A`, with `Obs_refl`, `Obs_transp` (its elimination, into `SProp` only) and `Obs_cast` (a value carried along an equality of types), after Pujet and Tabareau’s CC^obs.
- [mod omega](https://docs.logicaffeine.com/logicaffeine_kernel/omega/): Omega Test: True Integer Arithmetic Decision Procedure
- [mod positivity](https://docs.logicaffeine.com/logicaffeine_kernel/positivity/): Strict positivity checking for inductive types.
- [mod prelude](https://docs.logicaffeine.com/logicaffeine_kernel/prelude/): Standard Library for the Kernel.
- [mod quotient](https://docs.logicaffeine.com/logicaffeine_kernel/quotient/): Certified universe-polymorphic quotient primitives for kernel importers.
- [mod recheck](https://docs.logicaffeine.com/logicaffeine_kernel/recheck/): An independent proof-term re-checker (the de Bruijn criterion taken seriously).
- [mod recursor](https://docs.logicaffeine.com/logicaffeine_kernel/recursor/): R2 — auto-derived recursors (dependent eliminators) for inductive types.
- [mod reify](https://docs.logicaffeine.com/logicaffeine_kernel/reify/): Shared reification substrate for the arithmetic decision procedures.
- [mod ring](https://docs.logicaffeine.com/logicaffeine_kernel/ring/): Ring Tactic: Polynomial Equality by Normalization
- [mod simp](https://docs.logicaffeine.com/logicaffeine_kernel/simp/): Simplifier Tactic
- [mod tactic_cert](https://docs.logicaffeine.com/logicaffeine_kernel/tactic_cert/): Independent verification of reflected ring, linear-arithmetic, and congruence goals.
- [mod tactics](https://docs.logicaffeine.com/logicaffeine_kernel/tactics/): Tactics over the kernel’s own goals: a goal state of metavariables, outside the trusted base.
- [mod term_store](https://docs.logicaffeine.com/logicaffeine_kernel/term_store/): Hash-consed term storage — the representation a kernel needs to be as fast as Lean’s.
- [mod termination](https://docs.logicaffeine.com/logicaffeine_kernel/termination/): Termination checking for fixpoints.
- [mod word_ring](https://docs.logicaffeine.com/logicaffeine_kernel/word_ring/): Kernel ring proofs for the word ring ℤ/2ⁿ (`Word8`/`Word16`/`Word32`/`Word64`).
- [struct BigInt](https://docs.logicaffeine.com/logicaffeine_kernel/struct.BigInt): An exact, arbitrary-precision integer.
- [struct Context](https://docs.logicaffeine.com/logicaffeine_kernel/struct.Context): Typing context: maps variable names to their types.
- [struct MutualInductive](https://docs.logicaffeine.com/logicaffeine_kernel/struct.MutualInductive): One member of a MUTUAL inductive block: its name, arity sort, uniform parameter count, and constructors (name + full type). Constructor types may reference ANY member of the block — that is the whole point of a mutual declaration.
- [struct SimpRule](https://docs.logicaffeine.com/logicaffeine_kernel/struct.SimpRule): The `@[simp]` registry’s compiled rule — `Context::simp_rules`/`simp_rules_for` hand these to whatever does the rewriting, already destructured into `∀x̄. lhs ⟶ rhs`. A `@[simp]` lemma COMPILED to the form a rewriter applies: `∀x̄. lhs ⟶ rhs`.
- [struct SourcePosition](https://docs.logicaffeine.com/logicaffeine_kernel/struct.SourcePosition): The transparent carrier’s payload: a binder’s kind, or where a subterm came from. A position in a source text, in Lean’s convention: the LINE is 1-based and the COLUMN is 0-based and counted in Unicode scalar values. Held in its canonical spelling, the one Lean prints a diagnostic’s position in — `file:line:column` — so a position IS its text: two positions are equal exactly when they print the same, and reading one back needs no rendering.
- [struct StructInfo](https://docs.logicaffeine.com/logicaffeine_kernel/struct.StructInfo): Metadata for a registered structure (record): its single constructor, how many leading type PARAMETERS it takes, the projection function names in field order, and the declaration shape the elaborator needs — the parameter and field telescopes, the parents recovered from a flattened field prefix, and which parameters are OUTPUTS.
- [enum Annotation](https://docs.logicaffeine.com/logicaffeine_kernel/enum.Annotation): The transparent carrier’s payload: a binder’s kind, or where a subterm came from. One piece of information about how a subterm was written. The elaborator and the interface printer read it; every kernel judgment erases it first.
- [enum ConstError](https://docs.logicaffeine.com/logicaffeine_kernel/enum.ConstError): Why a `Term::Const` reference could not be resolved. Every kernel and the reducer report the same three failures, so a reference refused by typing is never a normal form to the reducer.
- [enum KernelError](https://docs.logicaffeine.com/logicaffeine_kernel/enum.KernelError): Errors that can occur during type checking.
- [enum Literal](https://docs.logicaffeine.com/logicaffeine_kernel/enum.Literal): Primitive literal values.
- [enum MeaningChange](https://docs.logicaffeine.com/logicaffeine_kernel/enum.MeaningChange): How a refused declaration would have changed a registered name’s meaning.
- [enum Provenance](https://docs.logicaffeine.com/logicaffeine_kernel/enum.Provenance): The transparent carrier’s payload: a binder’s kind, or where a subterm came from. Where a subterm came from.
- [enum Reducibility](https://docs.logicaffeine.com/logicaffeine_kernel/enum.Reducibility): Lean’s reducibility axis, declared per constant — `Context::is_irreducible` is the predicate `reduction::Transparency::Excluding` is looking for. Lean’s REDUCIBILITY axis, declared per constant and read by the elaborator’s δ step.
- [enum StructureRefusal](https://docs.logicaffeine.com/logicaffeine_kernel/enum.StructureRefusal): Why structure η was refused. Every variant names the first condition that failed.
- [enum Term](https://docs.logicaffeine.com/logicaffeine_kernel/enum.Term): Unified term representation.
- [enum Transparency](https://docs.logicaffeine.com/logicaffeine_kernel/enum.Transparency): The δ-transparency axis (Lean’s `TransparencyMode`): `normalize_at`/`normalize_checked_at` keep an `@[irreducible]` constant folded with its body intact, while `normalize` stays the kernel’s own always-unfolding setting. How much δ a reduction is allowed — Lean’s `TransparencyMode`, narrowed to the axis that actually changes the answer.
- [enum Universe](https://docs.logicaffeine.com/logicaffeine_kernel/enum.Universe): Universe levels in the type hierarchy — a level EXPRESSION, so the kernel can be universe-POLYMORPHIC (R3). The concrete hierarchy is `Prop : Type 1 : Type 2 : …` with `Prop ≤ Type i`; on top of it, a level may mention universe VARIABLES, so one definition (`id.{u} : Π(A : Sort u). A → A`) is reusable at every level instead of duplicated per level.
- [enum Unreduced](https://docs.logicaffeine.com/logicaffeine_kernel/enum.Unreduced): Why a reduction stopped before reaching a normal form.
- [const DEFAULT_INSTANCE_PRIORITY](https://docs.logicaffeine.com/logicaffeine_kernel/constant.DEFAULT_INSTANCE_PRIORITY): Lean’s default instance priority — what `instance foo : C α := …` gets when it says no `(priority := n)`. Named rather than spelled `1000` at each site so a translator carrying a Lean source’s explicit priorities lands them on the same scale.
- [fn check_positivity_for_test](https://docs.logicaffeine.com/logicaffeine_kernel/fn.check_positivity_for_test): Strict-positivity check of a constructor type — exposed so tests can pin the paradox fence (negative occurrences rejected, positive functional fields accepted) directly.
- [fn defeq_for_test](https://docs.logicaffeine.com/logicaffeine_kernel/fn.defeq_for_test): Definitional equality of two terms — exposed for tests that pin conversion behaviour (structure eta, proof irrelevance) directly.
- [fn discard_resource_stops](https://docs.logicaffeine.com/logicaffeine_kernel/fn.discard_resource_stops): Whether a verdict depended on kernel work that stopped for want of a resource: a conversion that says “not equal” decided nothing when one of its reductions ran out of budget. Run `f` WITHOUT letting its resource stops reach the enclosing observation — for work whose answer the verdict does not use (a debug differential that re-decides a pair already decided).
- [fn infer_type](https://docs.logicaffeine.com/logicaffeine_kernel/fn.infer_type): Infer the type of a term in a context.
- [fn instantiate_codomain](https://docs.logicaffeine.com/logicaffeine_kernel/fn.instantiate_codomain): Substitute `replacement` for `var` in `body`, WRITING IT ONCE when copying it would blow the result up.
- [fn instantiate_universes](https://docs.logicaffeine.com/logicaffeine_kernel/fn.instantiate_universes): Instantiate universe variables throughout a term: substitute every `Sort`’s level by `subst`. This specializes a universe-POLYMORPHIC term (`λA:Sort u. …`) to a concrete level (`u := Type 0`), yielding an ordinary term the kernel checks as-is — so one definition is reused at every level instead of duplicated.
- [fn int_lit](https://docs.logicaffeine.com/logicaffeine_kernel/fn.int_lit): The canonical `Literal` for an integer: `Int(i64)` when it fits (the fast, common path), otherwise the arbitrary-precision `BigInt`. This is the ONLY sanctioned way to build an integer literal from a `BigInt` result, guaranteeing the one-representation-per-value invariant on which definitional equality of literals rests.
- [fn is_subtype](https://docs.logicaffeine.com/logicaffeine_kernel/fn.is_subtype): Check if type `a` is a subtype of type `b` (cumulativity).
- [fn lit_bigint](https://docs.logicaffeine.com/logicaffeine_kernel/fn.lit_bigint): The `BigInt` value of an integer literal, promoting a machine `Int` — for arithmetic that must run in arbitrary precision. `None` for non-integer literals.
- [fn normalize](https://docs.logicaffeine.com/logicaffeine_kernel/fn.normalize): Normalize a term to its normal form.
- [fn normalize_at](https://docs.logicaffeine.com/logicaffeine_kernel/fn.normalize_at): The δ-transparency axis (Lean’s `TransparencyMode`): `normalize_at`/`normalize_checked_at` keep an `@[irreducible]` constant folded with its body intact, while `normalize` stays the kernel’s own always-unfolding setting. `normalize` at a chosen transparency. At `Transparency::Excluding` the named constants keep their bodies and stay FOLDED, which is what `@[irreducible]` means at Lean’s default transparency; `normalize` itself is the kernel’s setting and unfolds everything.
- [fn normalize_checked](https://docs.logicaffeine.com/logicaffeine_kernel/fn.normalize_checked): Normalize a term, reporting honestly when the reduction did not finish.
- [fn normalize_checked_at](https://docs.logicaffeine.com/logicaffeine_kernel/fn.normalize_checked_at): The δ-transparency axis (Lean’s `TransparencyMode`): `normalize_at`/`normalize_checked_at` keep an `@[irreducible]` constant folded with its body intact, while `normalize` stays the kernel’s own always-unfolding setting. `normalize_checked` at a chosen transparency — the honest face of `normalize_at`.
- [fn normalize_checked_elab](https://docs.logicaffeine.com/logicaffeine_kernel/fn.normalize_checked_elab): The elaborator’s reduction face: `@[irreducible]` constants stay folded, body intact, with the opacity predicate built once from `Context::is_irreducible` rather than by each caller. `normalize` remains the kernel’s face and unfolds everything, exactly as Lean’s does. `normalize_elab`’s honest face: the elaborator’s transparency, and a reduction that did not finish reported as such rather than handed back as a normal form.
- [fn normalize_elab](https://docs.logicaffeine.com/logicaffeine_kernel/fn.normalize_elab): The elaborator’s reduction face: `@[irreducible]` constants stay folded, body intact, with the opacity predicate built once from `Context::is_irreducible` rather than by each caller. `normalize` remains the kernel’s face and unfolds everything, exactly as Lean’s does. `normalize` at the ELABORATOR’s transparency, reading the context’s own reducibility registry — the door that makes `@[irreducible]` reachable without every caller inventing its own opacity predicate.
- [fn observe_resource_stops](https://docs.logicaffeine.com/logicaffeine_kernel/fn.observe_resource_stops): Whether a verdict depended on kernel work that stopped for want of a resource: a conversion that says “not equal” decided nothing when one of its reductions ran out of budget. Run `f` and report the first resource stop of any kernel work it did — a reduction that spent its step budget, or a term too deep to descend — on this thread or on any sized-stack thread the kernel started for it.
- [fn reconcile_block_params](https://docs.logicaffeine.com/logicaffeine_kernel/fn.reconcile_block_params): The ONE parameter-count rule for a MUTUAL block, stated where registration can enforce it.
- [fn resolve_const_levels](https://docs.logicaffeine.com/logicaffeine_kernel/fn.resolve_const_levels): Resolve a `Term::Const { name, levels }` against a declaration, producing the universe substitution to apply to its type AND its body (rules 1-3 above). This is the ONE place the decision is made; `instantiate_universes` applies the result.
- [fn substitute](https://docs.logicaffeine.com/logicaffeine_kernel/fn.substitute): Substitute a term for a variable: `body[var := replacement]`.
- [type KernelResult](https://docs.logicaffeine.com/logicaffeine_kernel/type.KernelResult): Result type for kernel operations.

## logicaffeine_kernel::bitvector
Bitvector reflection-symmetry decision procedure.

- [const PROOF_WIDTH](https://docs.logicaffeine.com/logicaffeine_kernel/bitvector/constant.PROOF_WIDTH): Width up to which the per-bit identities are exhaustively machine-checked. The edge-distance-uniformity argument (module docs) needs only n ≳ 6 to exercise every boundary regime plus interior, so 16 — which covers every computationally-feasible N-Queens size with margin and runs in ~50ms once (memoised) — certifies the identities for every `n`.
- [fn reflection_certificate](https://docs.logicaffeine.com/logicaffeine_kernel/bitvector/fn.reflection_certificate): The certificate: `Ok(())` iff the reflection identities are proven (for all `n`), else the counterexample. Memoised.
- [fn reflection_symmetry_proven](https://docs.logicaffeine.com/logicaffeine_kernel/bitvector/fn.reflection_symmetry_proven): `true` iff left-right reflection is a proven symmetry of a bitmask counting search with one column mask and a conjugate `<<1`/`>>1` diagonal pair — the soundness gate for the symmetry-breaking optimization. Proven for all `n`.
- [fn rev_n](https://docs.logicaffeine.com/logicaffeine_kernel/bitvector/fn.rev_n): Reverse the low `n` bits of `x` (bits ≥ n are ignored). The board reflection.

## logicaffeine_kernel::cc
Congruence Closure Tactic

- [struct EGraph](https://docs.logicaffeine.com/logicaffeine_kernel/cc/struct.EGraph): E-graph with congruence closure.
- [struct UnionFind](https://docs.logicaffeine.com/logicaffeine_kernel/cc/struct.UnionFind): The shared Union-Find — one equivalence engine underneath the kernel’s congruence closure and the compiler’s e-graph. Union-Find over `usize` element ids.
- [enum ENode](https://docs.logicaffeine.com/logicaffeine_kernel/cc/enum.ENode): Node in the E-graph representing a term.
- [fn check_goal](https://docs.logicaffeine.com/logicaffeine_kernel/cc/fn.check_goal): Check if a goal is provable by congruence closure.
- [fn decompose_goal](https://docs.logicaffeine.com/logicaffeine_kernel/cc/fn.decompose_goal): Decompose a goal into hypotheses and conclusion.
- [fn reify](https://docs.logicaffeine.com/logicaffeine_kernel/cc/fn.reify): Reify a Syntax term into an E-graph node.

## logicaffeine_kernel::certificate
Independently re-checkable proof certificates — the De Bruijn criterion.

- [struct CaptureRequest](https://docs.logicaffeine.com/logicaffeine_kernel/certificate/struct.CaptureRequest)
- [struct CertDeclaration](https://docs.logicaffeine.com/logicaffeine_kernel/certificate/struct.CertDeclaration): A declaration in a theorem’s disclosed environment: a `name : type` assumption (a premise hypothesis, or a declared predicate/constant) that the proof cites.
- [struct CertDefinition](https://docs.logicaffeine.com/logicaffeine_kernel/certificate/struct.CertDefinition): A transparent definition in a theorem’s disclosed environment: `name : type := body`, δ-unfoldable during re-checking exactly as the prover registered it.
- [struct Certificate](https://docs.logicaffeine.com/logicaffeine_kernel/certificate/struct.Certificate): A self-contained, re-checkable proof certificate.
- [struct ConstructorClaim](https://docs.logicaffeine.com/logicaffeine_kernel/certificate/struct.ConstructorClaim): One constructor of an inductive type: its name and full type (parameters included).
- [struct EnvironmentCertificate](https://docs.logicaffeine.com/logicaffeine_kernel/certificate/struct.EnvironmentCertificate): A proof together with the complete environment it needs, rebuilt and re-checked from nothing but the declared base.
- [struct EnvironmentError](https://docs.logicaffeine.com/logicaffeine_kernel/certificate/struct.EnvironmentError): A refusal: its code and a sentence saying what was refused.
- [struct EnvironmentLimits](https://docs.logicaffeine.com/logicaffeine_kernel/certificate/struct.EnvironmentLimits): Limits enforced on a certificate BEFORE any term is built or checked.
- [struct InductiveType](https://docs.logicaffeine.com/logicaffeine_kernel/certificate/struct.InductiveType): One member of an inductive block.
- [struct RebuiltEnvironment](https://docs.logicaffeine.com/logicaffeine_kernel/certificate/struct.RebuiltEnvironment): A rebuilt environment: the checked context and what the checks found.
- [struct RecheckReport](https://docs.logicaffeine.com/logicaffeine_kernel/certificate/struct.RecheckReport): What `recheck <certificate.json>` reports: its outcome and one line per finding.
- [struct TheoremCertificate](https://docs.logicaffeine.com/logicaffeine_kernel/certificate/struct.TheoremCertificate): A self-contained, re-checkable certificate for a theorem proved FROM premises.
- [struct TheoremRecheck](https://docs.logicaffeine.com/logicaffeine_kernel/certificate/struct.TheoremRecheck): The outcome of independently re-checking a `TheoremCertificate`.
- [enum AnyCertificate](https://docs.logicaffeine.com/logicaffeine_kernel/certificate/enum.AnyCertificate): Every certificate this module defines, read from JSON by one door.
- [enum BinderKind](https://docs.logicaffeine.com/logicaffeine_kernel/certificate/enum.BinderKind): A binder annotation, as Lean’s `BinderInfo` records it.
- [enum ConversionDiscipline](https://docs.logicaffeine.com/logicaffeine_kernel/certificate/enum.ConversionDiscipline): How declared types are compared with inferred ones.
- [enum EnvironmentBase](https://docs.logicaffeine.com/logicaffeine_kernel/certificate/enum.EnvironmentBase): The trusted base an environment is rebuilt on. The checker builds it; the certificate only names it.
- [enum EnvironmentEntry](https://docs.logicaffeine.com/logicaffeine_kernel/certificate/enum.EnvironmentEntry): One declaration of an environment, in dependency order.
- [enum EnvironmentErrorCode](https://docs.logicaffeine.com/logicaffeine_kernel/certificate/enum.EnvironmentErrorCode): Why an environment certificate was refused. Each code is one kind of refusal, so a caller — and a tamper test — can say not only THAT a certificate failed but which check refused it.
- [enum IndependentVerdict](https://docs.logicaffeine.com/logicaffeine_kernel/certificate/enum.IndependentVerdict): How one declaration fared under the second, independent kernel (`crate::recheck`).
- [enum QuotientPrimitive](https://docs.logicaffeine.com/logicaffeine_kernel/certificate/enum.QuotientPrimitive): Lean’s four quotient primitives, as the kernel certifies them.
- [enum RecheckOutcome](https://docs.logicaffeine.com/logicaffeine_kernel/certificate/enum.RecheckOutcome): How an independent re-check of one certificate document ended.
- [enum TermNode](https://docs.logicaffeine.com/logicaffeine_kernel/certificate/enum.TermNode): One row of a certificate’s term table: a `Term` constructor whose children are earlier rows.
- [const ENVIRONMENT_SCHEMA](https://docs.logicaffeine.com/logicaffeine_kernel/certificate/constant.ENVIRONMENT_SCHEMA): The original format, supported unchanged for certificates containing its original entry kinds.
- [const OPAQUE_ENVIRONMENT_SCHEMA](https://docs.logicaffeine.com/logicaffeine_kernel/certificate/constant.OPAQUE_ENVIRONMENT_SCHEMA): The latest environment-certificate format. Version 2 adds checked opaque declarations. Capture writes the oldest supported format that can represent its entries: version 1 for original entry kinds, version 2 when an opaque occurs. Readers never retag existing evidence.
- [const PRELUDE_VERSION](https://docs.logicaffeine.com/logicaffeine_kernel/certificate/constant.PRELUDE_VERSION): The prelude/axiom-set version a certificate was produced against. A re-checker may refuse certificates minted against an axiom set it does not recognise. Bump this whenever the trusted prelude changes.
- [const RETIRED_PRELUDE_VERSIONS](https://docs.logicaffeine.com/logicaffeine_kernel/certificate/constant.RETIRED_PRELUDE_VERSIONS): Prelude tags this checker knows it is NOT. A certificate carrying one of them is refused with an explicit incompatibility — the axiom sets differ and no migration exists — rather than the generic “unknown version” a typo would get. The tag is never rewritten to make it fit.
- [fn check_prelude_version](https://docs.logicaffeine.com/logicaffeine_kernel/certificate/fn.check_prelude_version): Refuse any prelude tag but this checker’s own, explicitly for a retired one.
- [fn read_certificate](https://docs.logicaffeine.com/logicaffeine_kernel/certificate/fn.read_certificate): Read a certificate of any kind from JSON.
- [fn recheck](https://docs.logicaffeine.com/logicaffeine_kernel/certificate/fn.recheck): Independently re-validate a certificate.
- [fn recheck_document](https://docs.logicaffeine.com/logicaffeine_kernel/certificate/fn.recheck_document): Re-check a certificate document of any kind, dispatched by its schema.
- [fn recheck_theorem](https://docs.logicaffeine.com/logicaffeine_kernel/certificate/fn.recheck_theorem): Independently re-validate a `TheoremCertificate`.
- [type NodeRef](https://docs.logicaffeine.com/logicaffeine_kernel/certificate/type.NodeRef): A reference to an earlier row of a certificate’s term table.

## logicaffeine_kernel::dag
The kernel core: a type theory over a hash-consed expression DAG, in two modes (`tc::Theory`): Lean 4’s theory exactly, and LOGOS’s Calculus of Inductive Constructions.

- [mod check](https://docs.logicaffeine.com/logicaffeine_kernel/dag/check/): Admitting declarations: the kernel’s only door into the environment.
- [mod env](https://docs.logicaffeine.com/logicaffeine_kernel/dag/env/): The environment: every declaration the kernel has admitted, indexed by name.
- [mod error](https://docs.logicaffeine.com/logicaffeine_kernel/dag/error/): Typed kernel verdicts.
- [mod export](https://docs.logicaffeine.com/logicaffeine_kernel/dag/export/): Reading a `lean4export` NDJSON stream straight into the kernel core.
- [mod expr](https://docs.logicaffeine.com/logicaffeine_kernel/dag/expr/): The kernel core’s expression store: a maximally shared DAG with de Bruijn indices.
- [mod inductive](https://docs.logicaffeine.com/logicaffeine_kernel/dag/inductive/): Inductive families: Lean’s `add_inductive`, including nested-inductive elimination and recursor generation.
- [mod json](https://docs.logicaffeine.com/logicaffeine_kernel/dag/json/): A small, allocation-free JSON reader for one NDJSON record at a time.
- [mod level](https://docs.logicaffeine.com/logicaffeine_kernel/dag/level/): Universe levels: hash-consed, with a COMPLETE decision procedure for `≤` and `≡`.
- [mod logos](https://docs.logicaffeine.com/logicaffeine_kernel/dag/logos/): LOGOS’s own terms in the core’s store: `lower` takes a `Term` of LOGOS’s Calculus of Inductive Constructions to an `ExprId`, and `lift` takes it back.
- [mod logos_env](https://docs.logicaffeine.com/logicaffeine_kernel/dag/logos_env/): A LOGOS context replayed into the core: every declaration, in dependency order, admitted by `Theory::Logos`’s checks, with the core’s verdict for each.
- [mod logos_tc](https://docs.logicaffeine.com/logicaffeine_kernel/dag/logos_tc/): LOGOS’s Calculus of Inductive Constructions in the core: the rules `Theory::Logos` adds to the substitution checker.
- [mod mirror](https://docs.logicaffeine.com/logicaffeine_kernel/dag/mirror/): The core beside a `Context`: a `Kernel::logos` per thread, kept in step with the context it last mirrored through that context’s admission log.
- [mod name](https://docs.logicaffeine.com/logicaffeine_kernel/dag/name/): Hierarchical names, interned: `Nat.succ` is `Str(Str(Anon, "Nat"), "succ")`, and each distinct name is one `NameId`, so name equality is an integer compare.
- [mod nat](https://docs.logicaffeine.com/logicaffeine_kernel/dag/nat/): Lean’s natural numbers on top of `logicaffeine_base::BigInt`.
- [mod pretty](https://docs.logicaffeine.com/logicaffeine_kernel/dag/pretty/): A bounded, readable rendering of core expressions for diagnostics.
- [mod primitive](https://docs.logicaffeine.com/logicaffeine_kernel/dag/primitive/): Primitive validation: the literal extension is only as sound as the definitions it replaces.
- [mod primitive_wf](https://docs.logicaffeine.com/logicaffeine_kernel/dag/primitive_wf/): Validating the well-founded `Nat` primitives: `Nat.div`, `Nat.mod`, `Nat.gcd`, `Nat.bitwise`.
- [mod relevance](https://docs.logicaffeine.com/logicaffeine_kernel/dag/relevance/): Argument relevance: which arguments of a definition cannot change what it computes.
- [mod sem](https://docs.logicaffeine.com/logicaffeine_kernel/dag/sem/): The value engine: type checking and definitional equality by evaluation into closures.
- [mod tc](https://docs.logicaffeine.com/logicaffeine_kernel/dag/tc/): Type inference, weak-head normalisation and definitional equality over the shared DAG.
- [mod wellknown](https://docs.logicaffeine.com/logicaffeine_kernel/dag/wellknown/): Names the kernel gives meaning to, interned once so every test is an id compare.

## logicaffeine_kernel::dag::check
Admitting declarations: the kernel’s only door into the environment.

- [struct DefnDecl](https://docs.logicaffeine.com/logicaffeine_kernel/dag/check/struct.DefnDecl)
- [struct Header](https://docs.logicaffeine.com/logicaffeine_kernel/dag/check/struct.Header)
- [enum Decl](https://docs.logicaffeine.com/logicaffeine_kernel/dag/check/enum.Decl)

## logicaffeine_kernel::dag::env
The environment: every declaration the kernel has admitted, indexed by name.

- [struct Const](https://docs.logicaffeine.com/logicaffeine_kernel/dag/env/struct.Const)
- [struct CtorInfo](https://docs.logicaffeine.com/logicaffeine_kernel/dag/env/struct.CtorInfo)
- [struct Env](https://docs.logicaffeine.com/logicaffeine_kernel/dag/env/struct.Env): Constants indexed densely by `NameId`.
- [struct InductiveInfo](https://docs.logicaffeine.com/logicaffeine_kernel/dag/env/struct.InductiveInfo)
- [struct RecInfo](https://docs.logicaffeine.com/logicaffeine_kernel/dag/env/struct.RecInfo)
- [struct RecRule](https://docs.logicaffeine.com/logicaffeine_kernel/dag/env/struct.RecRule)
- [enum Hint](https://docs.logicaffeine.com/logicaffeine_kernel/dag/env/enum.Hint)
- [enum Kind](https://docs.logicaffeine.com/logicaffeine_kernel/dag/env/enum.Kind)
- [enum QuotKind](https://docs.logicaffeine.com/logicaffeine_kernel/dag/env/enum.QuotKind)
- [enum Safety](https://docs.logicaffeine.com/logicaffeine_kernel/dag/env/enum.Safety)

## logicaffeine_kernel::dag::error
Typed kernel verdicts.

- [struct Failure](https://docs.logicaffeine.com/logicaffeine_kernel/dag/error/struct.Failure)
- [struct KernelFailure](https://docs.logicaffeine.com/logicaffeine_kernel/dag/error/struct.KernelFailure): A `Failure` behind one pointer. Every step of checking returns a `KResult`, almost always `Ok`; boxed, the failure keeps `KResult<T>` as small as `T` plus a pointer, so results travel in registers instead of through memory on every call.
- [enum FailKind](https://docs.logicaffeine.com/logicaffeine_kernel/dag/error/enum.FailKind)
- [type KResult](https://docs.logicaffeine.com/logicaffeine_kernel/dag/error/type.KResult)

## logicaffeine_kernel::dag::export
Reading a `lean4export` NDJSON stream straight into the kernel core.

- [struct Observe](https://docs.logicaffeine.com/logicaffeine_kernel/dag/export/struct.Observe): How a run is observed, beside the kernel’s own configuration.
- [struct Reader](https://docs.logicaffeine.com/logicaffeine_kernel/dag/export/struct.Reader)
- [struct Stats](https://docs.logicaffeine.com/logicaffeine_kernel/dag/export/struct.Stats)
- [enum Verdict](https://docs.logicaffeine.com/logicaffeine_kernel/dag/export/enum.Verdict): The verdict of checking one export, in the Arena’s exit-code protocol.
- [trait DeclMeter](https://docs.logicaffeine.com/logicaffeine_kernel/dag/export/trait.DeclMeter): Observes each declaration the reader hands to the kernel: `begin` just before the kernel checks it and `end` just after, with its name, its record kind and whether it was admitted. A measurement hook; checking never depends on it.
- [fn check_export](https://docs.logicaffeine.com/logicaffeine_kernel/dag/export/fn.check_export): Checks a whole export stream.
- [fn check_export_in](https://docs.logicaffeine.com/logicaffeine_kernel/dag/export/fn.check_export_in): Checks a whole export into the caller’s kernel, which keeps everything admitted — a command that exits once it has reported need never pay for tearing the kernel down.
- [fn check_export_observed](https://docs.logicaffeine.com/logicaffeine_kernel/dag/export/fn.check_export_observed): `check_export_sized`, observed as `observe` asks.
- [fn check_export_sized](https://docs.logicaffeine.com/logicaffeine_kernel/dag/export/fn.check_export_sized): `check_export_with` for an input whose size is known, so the stores are sized once.
- [fn check_export_with](https://docs.logicaffeine.com/logicaffeine_kernel/dag/export/fn.check_export_with): Checks a whole export with a kernel configured by `configure` first.
- [fn load_refs](https://docs.logicaffeine.com/logicaffeine_kernel/dag/export/fn.load_refs): Loads a file of named reference terms into `k`’s store.

## logicaffeine_kernel::dag::expr
The kernel core’s expression store: a maximally shared DAG with de Bruijn indices.

- [struct ExprId](https://docs.logicaffeine.com/logicaffeine_kernel/dag/expr/struct.ExprId)
- [struct LitId](https://docs.logicaffeine.com/logicaffeine_kernel/dag/expr/struct.LitId)
- [struct NatId](https://docs.logicaffeine.com/logicaffeine_kernel/dag/expr/struct.NatId)
- [struct Store](https://docs.logicaffeine.com/logicaffeine_kernel/dag/expr/struct.Store)
- [struct StrId](https://docs.logicaffeine.com/logicaffeine_kernel/dag/expr/struct.StrId)
- [enum Lit](https://docs.logicaffeine.com/logicaffeine_kernel/dag/expr/enum.Lit): A LOGOS literal with no Lean counterpart. `Nat` and `Text` literals are `Node::NatLit` and `Node::StrLit`. An integer is canonical: one that fits `i64` is `Int`, any other `BigInt`. A float is held by its bits, so equal literals are one id and `0.0`/`-0.0` stay apart.
- [enum Node](https://docs.logicaffeine.com/logicaffeine_kernel/dag/expr/enum.Node)
- [type Args](https://docs.logicaffeine.com/logicaffeine_kernel/dag/expr/type.Args): The arguments of an application spine; most spines fit inline.

## logicaffeine_kernel::dag::inductive
Inductive families: Lean’s `add_inductive`, including nested-inductive elimination and recursor generation.

- [struct IndType](https://docs.logicaffeine.com/logicaffeine_kernel/dag/inductive/struct.IndType)
- [struct InductiveDecl](https://docs.logicaffeine.com/logicaffeine_kernel/dag/inductive/struct.InductiveDecl)

## logicaffeine_kernel::dag::json
A small, allocation-free JSON reader for one NDJSON record at a time.

- [struct JsonError](https://docs.logicaffeine.com/logicaffeine_kernel/dag/json/struct.JsonError)
- [struct Tape](https://docs.logicaffeine.com/logicaffeine_kernel/dag/json/struct.Tape)
- [enum Tok](https://docs.logicaffeine.com/logicaffeine_kernel/dag/json/enum.Tok)

## logicaffeine_kernel::dag::level
Universe levels: hash-consed, with a COMPLETE decision procedure for `≤` and `≡`.

- [struct LevelId](https://docs.logicaffeine.com/logicaffeine_kernel/dag/level/struct.LevelId)
- [struct Levels](https://docs.logicaffeine.com/logicaffeine_kernel/dag/level/struct.Levels)
- [struct LevelsId](https://docs.logicaffeine.com/logicaffeine_kernel/dag/level/struct.LevelsId): An interned list of levels (the universe arguments of a constant).
- [struct SubstId](https://docs.logicaffeine.com/logicaffeine_kernel/dag/level/struct.SubstId): A universe substitution — a constant’s level parameters replaced by the levels of one use of it — interned, so that a value can carry it as one id.
- [enum LevelNode](https://docs.logicaffeine.com/logicaffeine_kernel/dag/level/enum.LevelNode)

## logicaffeine_kernel::dag::logos
LOGOS’s own terms in the core’s store: `lower` takes a `Term` of LOGOS’s Calculus of Inductive Constructions to an `ExprId`, and `lift` takes it back.

- [enum LowerError](https://docs.logicaffeine.com/logicaffeine_kernel/dag/logos/enum.LowerError): Why a term has no image in the core.
- [fn explicit_levels](https://docs.logicaffeine.com/logicaffeine_kernel/dag/logos/fn.explicit_levels): The levels the `Term` kernel’s application rule infers for a bare reference to a universe-polymorphic declaration (`type_checker::implicit_levels_for_head`), written out. The declaration’s level parameters become metavariables; left to right, each argument whose domain mentions one solves it from the argument’s type; a head whose every level is solved becomes `Const` at those levels. A head left with an unsolved level stays a bare reference, which the core refuses rather than guesses at.
- [fn level_telescope](https://docs.logicaffeine.com/logicaffeine_kernel/dag/logos/fn.level_telescope): A global’s universe parameters and type: its explicit level telescope, or else the level variables its type mentions, which the `Term` kernel reads as bound by the declaration.
- [fn lift](https://docs.logicaffeine.com/logicaffeine_kernel/dag/logos/fn.lift): The LOGOS term for a closed core expression.
- [fn lift_level](https://docs.logicaffeine.com/logicaffeine_kernel/dag/logos/fn.lift_level): The LOGOS universe for a core level.
- [fn lower](https://docs.logicaffeine.com/logicaffeine_kernel/dag/logos/fn.lower): The core expression for a closed LOGOS term.
- [fn lower_open](https://docs.logicaffeine.com/logicaffeine_kernel/dag/logos/fn.lower_open): The core expression for a LOGOS term over the kernel’s locals, named as `lift` names them.
- [fn lower_universe](https://docs.logicaffeine.com/logicaffeine_kernel/dag/logos/fn.lower_universe): The core level for a LOGOS universe.

## logicaffeine_kernel::dag::logos_env
A LOGOS context replayed into the core: every declaration, in dependency order, admitted by `Theory::Logos`’s checks, with the core’s verdict for each.

- [struct Replayed](https://docs.logicaffeine.com/logicaffeine_kernel/dag/logos_env/struct.Replayed): One declaration’s verdict in the replay.
- [enum Declaration](https://docs.logicaffeine.com/logicaffeine_kernel/dag/logos_env/enum.Declaration): A declaration as the core admits it, in the `Term` forms a `Context` registers. `params` are its universe parameters, in the order its constants take levels.
- [fn admit](https://docs.logicaffeine.com/logicaffeine_kernel/dag/logos_env/fn.admit): Admits one declaration, or one mutual block of inductive families, into a kernel built by `Kernel::logos` over `ctx`: the core’s verdict on it.
- [fn candidate_axiom](https://docs.logicaffeine.com/logicaffeine_kernel/dag/logos_env/fn.candidate_axiom): The axiom a door of `ctx` puts to the core, its type stored and its levels read as `candidate_definition` reads them.
- [fn candidate_block](https://docs.logicaffeine.com/logicaffeine_kernel/dag/logos_env/fn.candidate_block): The block of inductive families a door of `ctx` puts to the core. Each arity is stored as `ctx` stores it, and each member takes the stated telescope or its stored arity’s level variables. A constructor’s bare reference to a member stands at that member’s telescope, and one to anything else at the level `ctx` gives it.
- [fn candidate_definition](https://docs.logicaffeine.com/logicaffeine_kernel/dag/logos_env/fn.candidate_definition): The definition a door of `ctx` puts to the core: its terms as `ctx` stores them (`Context::stored_term`) and the telescope the door gives it, the stated one or the level variables of the stored type and then of the body (`term`’s rules 1 and 4).
- [fn replay](https://docs.logicaffeine.com/logicaffeine_kernel/dag/logos_env/fn.replay): Replays every declaration of `ctx` into a `Kernel::logos` kernel.

## logicaffeine_kernel::dag::logos_tc
LOGOS’s Calculus of Inductive Constructions in the core: the rules `Theory::Logos` adds to the substitution checker.

- [struct LogosState](https://docs.logicaffeine.com/logicaffeine_kernel/dag/logos_tc/struct.LogosState): What checking LOGOS’s theory needs beyond the store and the environment.

## logicaffeine_kernel::dag::mirror
The core beside a `Context`: a `Kernel::logos` per thread, kept in step with the context it last mirrored through that context’s admission log.

- [struct Synced](https://docs.logicaffeine.com/logicaffeine_kernel/dag/mirror/struct.Synced): What one `sync` did: its route, and the core’s verdict on each declaration it admitted.
- [enum Route](https://docs.logicaffeine.com/logicaffeine_kernel/dag/mirror/enum.Route): How `sync` brought the mirror to a context.
- [fn sync](https://docs.logicaffeine.com/logicaffeine_kernel/dag/mirror/fn.sync): Bring this thread’s mirror to `ctx`.
- [fn with](https://docs.logicaffeine.com/logicaffeine_kernel/dag/mirror/fn.with): Bring this thread’s mirror to `ctx` and run `f` on its kernel. The mirror is out of its slot while `f` runs, so a sync inside `f` builds its own and this one is put back after.

## logicaffeine_kernel::dag::name
Hierarchical names, interned: `Nat.succ` is `Str(Str(Anon, "Nat"), "succ")`, and each distinct name is one `NameId`, so name equality is an integer compare.

- [struct NameId](https://docs.logicaffeine.com/logicaffeine_kernel/dag/name/struct.NameId)
- [struct Names](https://docs.logicaffeine.com/logicaffeine_kernel/dag/name/struct.Names)
- [enum NameNode](https://docs.logicaffeine.com/logicaffeine_kernel/dag/name/enum.NameNode)
- [fn kernel_name_of_components](https://docs.logicaffeine.com/logicaffeine_kernel/dag/name/fn.kernel_name_of_components): The kernel spelling of a Lean name given as its hierarchical components: the name the Lean importer gives a declaration in a kernel context, each component written after `/s:` as a JSON string, with the kernel’s primitive identities applied (`Nat`, `Zero`, `Succ`, the quotient’s four, and every other `Nat` member under `Nat/`).

## logicaffeine_kernel::dag::nat
Lean’s natural numbers on top of `logicaffeine_base::BigInt`.

- [struct Nat](https://docs.logicaffeine.com/logicaffeine_kernel/dag/nat/struct.Nat)

## logicaffeine_kernel::dag::pretty
A bounded, readable rendering of core expressions for diagnostics.

- [fn show](https://docs.logicaffeine.com/logicaffeine_kernel/dag/pretty/fn.show)
- [fn show_level](https://docs.logicaffeine.com/logicaffeine_kernel/dag/pretty/fn.show_level)

## logicaffeine_kernel::dag::primitive
Primitive validation: the literal extension is only as sound as the definitions it replaces.


## logicaffeine_kernel::dag::primitive_wf
Validating the well-founded `Nat` primitives: `Nat.div`, `Nat.mod`, `Nat.gcd`, `Nat.bitwise`.


## logicaffeine_kernel::dag::relevance
Argument relevance: which arguments of a definition cannot change what it computes.

- [struct Cache](https://docs.logicaffeine.com/logicaffeine_kernel/dag/relevance/struct.Cache): Relevance facts, keyed on settled constants only.
- [struct Signature](https://docs.logicaffeine.com/logicaffeine_kernel/dag/relevance/struct.Signature): What a settled constant’s type says about its applications, at one universe instantiation.
- [const MAX_TRACKED](https://docs.logicaffeine.com/logicaffeine_kernel/dag/relevance/constant.MAX_TRACKED): Positions beyond this are always compared.

## logicaffeine_kernel::dag::sem
The value engine: type checking and definitional equality by evaluation into closures.

- [mod conv](https://docs.logicaffeine.com/logicaffeine_kernel/dag/sem/conv/): Definitional equality of values: Lean’s algorithm, in the classic engine’s order of attempts.
- [mod eval](https://docs.logicaffeine.com/logicaffeine_kernel/dag/sem/eval/): Evaluation: terms to values, application, and the values of constants.
- [mod infer](https://docs.logicaffeine.com/logicaffeine_kernel/dag/sem/infer/): Type inference and checking over values.
- [mod table](https://docs.logicaffeine.com/logicaffeine_kernel/dag/sem/table/): The value engine’s hash tables: open addressing with linear probing over small `Copy` keys and `u32` values, one slot per cache line access, Fibonacci-hashed.
- [mod types](https://docs.logicaffeine.com/logicaffeine_kernel/dag/sem/types/): The types of values, for the parts of conversion and reduction that look at types — proof irrelevance, η, struct-η, unit-like types, K — and for projections. Values reaching here are well-typed, so this is inference without checking: a head’s type followed along the spine.
- [mod value](https://docs.logicaffeine.com/logicaffeine_kernel/dag/sem/value/): Semantic values and the arena that interns them.
- [mod whnf](https://docs.logicaffeine.com/logicaffeine_kernel/dag/sem/whnf/): Weak-head reduction of values: ι (recursors, with K and struct-η), quotients, projections, validated `Nat` literal operations, and δ through constant heads.
- [struct Counters](https://docs.logicaffeine.com/logicaffeine_kernel/dag/sem/struct.Counters): How the session’s caches are doing (reported by `logos_kernel --stats`).
- [struct Sem](https://docs.logicaffeine.com/logicaffeine_kernel/dag/sem/struct.Sem): The engine: the kernel (environment, stores, well-known names) and the session state.
- [struct State](https://docs.logicaffeine.com/logicaffeine_kernel/dag/sem/struct.State): One session’s values and caches.

## logicaffeine_kernel::dag::sem::conv
Definitional equality of values: Lean’s algorithm, in the classic engine’s order of attempts.


## logicaffeine_kernel::dag::sem::eval
Evaluation: terms to values, application, and the values of constants.


## logicaffeine_kernel::dag::sem::infer
Type inference and checking over values.


## logicaffeine_kernel::dag::sem::table
The value engine’s hash tables: open addressing with linear probing over small `Copy` keys and `u32` values, one slot per cache line access, Fibonacci-hashed.

- [struct StampedTable](https://docs.logicaffeine.com/logicaffeine_kernel/dag/sem/table/struct.StampedTable): A table emptied often (at every declaration): emptying it is one increment.
- [struct Table](https://docs.logicaffeine.com/logicaffeine_kernel/dag/sem/table/struct.Table): A table that lives for a session: emptied rarely, by filling its slots with the vacant pattern (all bits set — a `memset`).
- [trait Key](https://docs.logicaffeine.com/logicaffeine_kernel/dag/sem/table/trait.Key): A key a table can hold: its hash must be well mixed in the TOP bits.

## logicaffeine_kernel::dag::sem::types
The types of values, for the parts of conversion and reduction that look at types — proof irrelevance, η, struct-η, unit-like types, K — and for projections. Values reaching here are well-typed, so this is inference without checking: a head’s type followed along the spine.


## logicaffeine_kernel::dag::sem::value
Semantic values and the arena that interns them.

- [struct Arena](https://docs.logicaffeine.com/logicaffeine_kernel/dag/sem/value/struct.Arena): All values of a checking session, their memos, and the tables that intern them.
- [struct CtxId](https://docs.logicaffeine.com/logicaffeine_kernel/dag/sem/value/struct.CtxId): The types of the enclosing bound variables, innermost first (for inference under binders).
- [struct CtxNode](https://docs.logicaffeine.com/logicaffeine_kernel/dag/sem/value/struct.CtxNode)
- [struct EnvId](https://docs.logicaffeine.com/logicaffeine_kernel/dag/sem/value/struct.EnvId): An environment: the values of the enclosing bound variables, innermost first.
- [struct EnvNode](https://docs.logicaffeine.com/logicaffeine_kernel/dag/sem/value/struct.EnvNode): An environment node: either one entry consed onto a parent environment, or a frame — a pruned environment of `len` entries holding only the entries an expression can see, stored contiguously from `val` (an index into the frame slots). A narrow frame (every live index below 64) finds an entry by its rank in `live`; a wide frame keeps its live indices as a sorted list (`wide`, an index into the wide-index table) and finds an entry by search.
- [struct HeadId](https://docs.logicaffeine.com/logicaffeine_kernel/dag/sem/value/struct.HeadId)
- [struct Sp](https://docs.logicaffeine.com/logicaffeine_kernel/dag/sem/value/struct.Sp): The arguments applied to a neutral head, as a snoc list.
- [struct SpNode](https://docs.logicaffeine.com/logicaffeine_kernel/dag/sem/value/struct.SpNode)
- [struct V](https://docs.logicaffeine.com/logicaffeine_kernel/dag/sem/value/struct.V)
- [enum Head](https://docs.logicaffeine.com/logicaffeine_kernel/dag/sem/value/enum.Head)
- [enum Kind](https://docs.logicaffeine.com/logicaffeine_kernel/dag/sem/value/enum.Kind): What a neutral’s head does under reduction.
- [enum Val](https://docs.logicaffeine.com/logicaffeine_kernel/dag/sem/value/enum.Val)
- [const DEAD](https://docs.logicaffeine.com/logicaffeine_kernel/dag/sem/value/constant.DEAD): The placeholder for an environment entry an expression cannot see: value 0 of every session, closed and inert (a neutral headed by the anonymous constant, which no declaration can be).
- [const OPEN](https://docs.logicaffeine.com/logicaffeine_kernel/dag/sem/value/constant.OPEN): The value mentions a variable bound by a binder being checked or compared.

## logicaffeine_kernel::dag::sem::whnf
Weak-head reduction of values: ι (recursors, with K and struct-η), quotients, projections, validated `Nat` literal operations, and δ through constant heads.


## logicaffeine_kernel::dag::tc
Type inference, weak-head normalisation and definitional equality over the shared DAG.

- [struct Kernel](https://docs.logicaffeine.com/logicaffeine_kernel/dag/tc/struct.Kernel): A kernel is plain data (its only shared cells are immutable: interned strings and admitted constants), so a clone is an independent kernel; `mirror` keeps one as a snapshot to branch from.
- [struct LocalDecl](https://docs.logicaffeine.com/logicaffeine_kernel/dag/tc/struct.LocalDecl)
- [enum Engine](https://docs.logicaffeine.com/logicaffeine_kernel/dag/tc/enum.Engine): The engine that checks declaration types and values (inductive families, quotients and the primitive validations always use the substitution checker).
- [enum Theory](https://docs.logicaffeine.com/logicaffeine_kernel/dag/tc/enum.Theory): The type theory a kernel checks.

## logicaffeine_kernel::dag::wellknown
Names the kernel gives meaning to, interned once so every test is an id compare.

- [struct QuotNames](https://docs.logicaffeine.com/logicaffeine_kernel/dag/wellknown/struct.QuotNames): One quotient’s four constants: its former, constructor, lift and induction principle.
- [struct WellKnown](https://docs.logicaffeine.com/logicaffeine_kernel/dag/wellknown/struct.WellKnown)

## logicaffeine_kernel::elaborate
R4 — the elaborator: metavariables, unification, and implicit-argument inference.

- [struct InstanceChoice](https://docs.logicaffeine.com/logicaffeine_kernel/elaborate/struct.InstanceChoice): A resolved instance together with WHY it won — the audit trail Lean’s instance resolution does not expose.
- [struct InstanceProbe](https://docs.logicaffeine.com/logicaffeine_kernel/elaborate/struct.InstanceProbe): One candidate examined during instance resolution.
- [struct MetaCtx](https://docs.logicaffeine.com/logicaffeine_kernel/elaborate/struct.MetaCtx): The metavariable context: fresh-name supply + the substitution being solved.
- [enum InstanceTier](https://docs.logicaffeine.com/logicaffeine_kernel/elaborate/enum.InstanceTier): Which TIER an instance was found in, and where inside it.
- [enum ParamKind](https://docs.logicaffeine.com/logicaffeine_kernel/elaborate/enum.ParamKind): How a function parameter is supplied during elaboration.
- [const ANON_CTOR_MARKER](https://docs.logicaffeine.com/logicaffeine_kernel/elaborate/constant.ANON_CTOR_MARKER): Reserved head marking a surface anonymous constructor `⟨e₁, …, eₙ⟩` (E3). The parser emits `⟨anon⟩ e₁ … eₙ`; the elaborator (this module) rewrites it to the sole constructor of the expected inductive and then discards the marker — it NEVER reaches a kernel term. The name contains `⟨`/`⟩`, characters the identifier lexer cannot produce, so it can never collide with a user global. Like the `?`-prefixed metavariables above, this rides on the existing `Term` with no new variant.
- [const DOT_MARKER](https://docs.logicaffeine.com/logicaffeine_kernel/elaborate/constant.DOT_MARKER): Reserved head marking surface dot notation `receiver.field` (E4). The parser emits `⟨proj⟩ receiver field` (the field name carried as a `Global`); the elaborator rewrites it to the projection `H_field params… receiver` and discards the marker. Collision-proof for the same reason as `ANON_CTOR_MARKER`.
- [fn auto_bind_implicits](https://docs.logicaffeine.com/logicaffeine_kernel/elaborate/fn.auto_bind_implicits): Auto-bind free type variables as leading implicit parameters. A definition written `id : A -> A := fun a : A => a` mentions `A` as a FREE, unregistered, single-uppercase global — the type-variable convention. This pass generalizes each such variable: it prepends `Π(A:Type)` to the type and `λ(A:Type)` to the body (converting `Global(A)` to the bound `Var(A)`), and returns the new implicit count, so `A` becomes an inferred implicit argument. Definitions that already bind their parameters reference them as `Var`s, not free `Global`s, so they are untouched — this only rescues what was previously an unbound-variable error.
- [fn bind_self_recursion](https://docs.logicaffeine.com/logicaffeine_kernel/elaborate/fn.bind_self_recursion): Replace every `Global(name)` by `Var(name)` (turning a free type-variable reference into a reference to the binder this pass prepends). Recursive-definition sugar: if `body` refers to the definition’s own `name` as a free `Global`, bind that self-reference with a `fix` so the definition can call itself — `Definition f : T := … f … .` becomes `f := fix f. …`. The kernel’s termination guard (run by `infer_type`) then certifies the recursion decreases structurally; a body with no self-reference (or one that already wrote an explicit `fix`, whose self-references are already bound `Var`s) is returned unchanged. A self-reference SHADOWS any same-named global, so a recursive `Definition add` over `Nat` overrides a built-in `add`.
- [fn elaborate](https://docs.logicaffeine.com/logicaffeine_kernel/elaborate/fn.elaborate): Elaborate `term` (which may contain `Hole`s) against an optional `expected` type, solving the holes by unification. Returns the elaborated term and its type (both still containing metavariables until `instantiate`d).
- [fn elaborate_anon_ctor](https://docs.logicaffeine.com/logicaffeine_kernel/elaborate/fn.elaborate_anon_ctor): Elaborate an ANONYMOUS CONSTRUCTOR `⟨f₀, …, fₙ⟩` (E3) against an EXPECTED inductive/ structure type `H a…`. It applies `H`’s (unique) constructor to the type parameters `a…`, read off the expected type, then the field values — so `⟨Zero, true⟩` expected at `Prod Nat Bool` becomes `Prod_mk Nat Bool Zero true`. Each field is elaborated against its declared type (so coercions/implicits fire), and the whole is kernel-certified.
- [fn elaborate_app](https://docs.logicaffeine.com/logicaffeine_kernel/elaborate/fn.elaborate_app): Elaborate an application of `head` (of type `head_ty`) where leading parameters may be implicit or instance-implicit (`kinds[i]`). A fresh metavariable is inserted for each implicit position; instance positions get a placeholder metavariable whose resolution is DEFERRED until all explicit arguments (which may pin the class’s type variables) have been unified. Returns the fully explicit, metavariable-instantiated term and type.
- [fn elaborate_app_against](https://docs.logicaffeine.com/logicaffeine_kernel/elaborate/fn.elaborate_app_against): Like `elaborate_app` but with an EXPECTED result type. After the explicit arguments are processed, the result type is unified with `expected` — so an implicit that the arguments alone do not pin (e.g. the `A` of `nil : {A} → List A`, which has no value argument) is solved from the surrounding context. The expected-type pass runs BEFORE instance resolution, so a class’s type variable can be fixed by the context too.
- [fn elaborate_dot](https://docs.logicaffeine.com/logicaffeine_kernel/elaborate/fn.elaborate_dot): Elaborate DOT notation `receiver.field` (E4). The receiver’s type head names an inductive/structure `H`; the projection is `H_field` (K4’s convention), applied to `H`’s parameters — read off the receiver’s type — and then the receiver itself. So `p.fst` with `p : Prod A B` becomes `Prod_fst A B p`. Returns an error if no such projection exists or the result does not type-check.
- [fn elaborate_in](https://docs.logicaffeine.com/logicaffeine_kernel/elaborate/fn.elaborate_in): Like `elaborate` but under a LOCAL CONTEXT `lctx` of bound variables. `ctx` is the kernel context already EXTENDED with those same variables (so `infer_type` sees them at the leaves), while `lctx` is the parallel `(name, type)` list the unifier uses for higher-order PATTERN unification. Descending under a `λ` extends both — which is how a metavariable applied to a bound variable (a motive `?P n`) gets solved in a body.
- [fn fill_match_motives](https://docs.logicaffeine.com/logicaffeine_kernel/elaborate/fn.fill_match_motives): Fill in inferred motives for `match` expressions written WITHOUT a `return` clause (the `Hole` motive the parser leaves). The motive is a CONSTANT `λ_:I. T` — covering non-dependent matches — where `T` is the EXPECTED type (a definition’s declared result type, propagated through binders) or, lacking one, the type of a nullary first branch. The pass threads the kernel context through binders so the discriminant’s type resolves; a `match` it cannot give a motive (a dependent case, no expected type) is reported so the user can add an explicit `return`.
- [fn instantiate](https://docs.logicaffeine.com/logicaffeine_kernel/elaborate/fn.instantiate): Substitute every solved metavariable throughout `term` (transitively, since a solution may itself mention other metavariables — the occurs-check keeps this terminating).
- [fn is_meta](https://docs.logicaffeine.com/logicaffeine_kernel/elaborate/fn.is_meta): Whether `name` denotes a metavariable (the `?`-prefix convention).
- [fn resolve_coercion](https://docs.logicaffeine.com/logicaffeine_kernel/elaborate/fn.resolve_coercion): Find a registered coercion carrying `from` to `to` (up to unification), returning the coercion FUNCTION to wrap the argument in — Lean’s `↑`. The elaborator calls this when an argument’s type does not match the expected parameter type; a match commits the unification (a polymorphic coercion’s type variables get solved).
- [fn resolve_instance](https://docs.logicaffeine.com/logicaffeine_kernel/elaborate/fn.resolve_instance): Search the `Context`’s instance database for an instance proving `required`, returning the (metavariable-instantiated) instance term. Handles POLYMORPHIC / RECURSIVE instances (`instance {A} [Inhabited A] : Inhabited (List A)`): the instance’s parameter telescope is freshened to metavariables, its conclusion is unified against `required` (solving the type parameters), and each PREMISE parameter is then resolved RECURSIVELY. The first instance that fully resolves wins; failed trials never pollute `mctx` (each runs on a clone, committed only on success).
- [fn resolve_instance_audited](https://docs.logicaffeine.com/logicaffeine_kernel/elaborate/fn.resolve_instance_audited): `resolve_instance` with the search recorded — the same answer, plus which entry won, at what priority and declaration index, and everything that was tried on the way.
- [fn surface_elaborate](https://docs.logicaffeine.com/logicaffeine_kernel/elaborate/fn.surface_elaborate): Elaborate a whole surface term: walk it, and at every application of a global with declared implicit parameters (`Context::implicit_args`), insert and infer those arguments — so `id 0` becomes `id Int 0`. Terms with no implicits are returned unchanged. The result is fully explicit and metavariable-free; the kernel certifies it as usual. This is the seam that wires the elaborator into the REPL.
- [fn surface_elaborate_against](https://docs.logicaffeine.com/logicaffeine_kernel/elaborate/fn.surface_elaborate_against): Like `surface_elaborate` but with an EXPECTED type (e.g. a definition’s declared type). The expected type is propagated to the top-level application/global so an implicit with no value argument — `nil : {A} → List A` used where a `List Int` is wanted — is inferred from context.
- [fn unify](https://docs.logicaffeine.com/logicaffeine_kernel/elaborate/fn.unify): First-order unification of `a` and `b`, solving metavariables into `mctx`. Returns whether they were made equal. A metavariable unifies with anything (after the occurs-check); everything else decomposes structurally.
- [fn unify_in](https://docs.logicaffeine.com/logicaffeine_kernel/elaborate/fn.unify_in): Unify `a` and `b` under a LOCAL CONTEXT `lctx` (`(name, type)` of the bound variables in scope). The local context enables higher-order PATTERN (Miller) unification: `?M x̄ =?= t`, where `?M` is a metavariable applied to distinct bound variables `x̄`, is solved by `?M := λx̄. t`. The top-level `unify` runs with an empty context, so its behavior — and every existing caller — is the first-order one.

## logicaffeine_kernel::equations
Equation lemmas — Lean’s `f.eq_def`, `f.eq_1 … f.eq_n` — the NAME a proof cites when it appeals to a definition’s behaviour, which is what `rw [f]` / `simp [f]` / `unfold f` all need.

- [const EQUATION_INFIX](https://docs.logicaffeine.com/logicaffeine_kernel/equations/constant.EQUATION_INFIX): Lean’s `eqnThmSuffixBasePrefix` (`Lean/Meta/Eqns.lean:60`), flattened.
- [const UNFOLD_SUFFIX](https://docs.logicaffeine.com/logicaffeine_kernel/equations/constant.UNFOLD_SUFFIX): Lean’s `unfoldThmSuffix` (`Lean/Meta/Eqns.lean:68`), flattened.
- [fn equation_lemmas](https://docs.logicaffeine.com/logicaffeine_kernel/equations/fn.equation_lemmas): The equation lemmas a definition owes, as `(name, statement, proof)` in Lean’s order: the unfold theorem first, then one equation per constructor of the matched argument.
- [fn generate](https://docs.logicaffeine.com/logicaffeine_kernel/equations/fn.generate): Generate and REGISTER the equation lemmas a definition owes.
- [fn generate_missing_for_all](https://docs.logicaffeine.com/logicaffeine_kernel/equations/fn.generate_missing_for_all): Back-fill every definition that was registered before `Eq`/`refl` existed.
- [fn is_equation_name](https://docs.logicaffeine.com/logicaffeine_kernel/equations/fn.is_equation_name): Whether a name is one this module MINTS, rather than one it generates lemmas for.

## logicaffeine_kernel::eval
A call-by-value evaluator for the kernel’s computational fragment — the engine behind `native_decide`.

- [fn eval_bool](https://docs.logicaffeine.com/logicaffeine_kernel/eval/fn.eval_bool): Evaluate a closed Bool term to `true`/`false`, or `None` if it does not reduce to a Bool constructor within the fuel budget (fail-safe).
- [fn eval_bool_tree](https://docs.logicaffeine.com/logicaffeine_kernel/eval/fn.eval_bool_tree): The tree-walking interpreter decision — walks the `Term` each step. The fallback for `eval_bool` and the differential oracle the compiled path is validated against.
- [fn native_compile_bool](https://docs.logicaffeine.com/logicaffeine_kernel/eval/fn.native_compile_bool): Compile a ground Bool decision into native closures and run it — `None` if the term is outside the compilable fragment (the caller falls back to the `eval_bool` interpreter). Semantics are IDENTICAL to `eval_bool`/`normalize` (differential-tested), so the `ofReduceBool` certificate `native_decide` builds is equally sound.
- [fn native_compile_decide](https://docs.logicaffeine.com/logicaffeine_kernel/eval/fn.native_compile_decide): Compile a closed Bool decision to native closures and run it — `None` if it does not reduce to a Bool constructor (fail-safe; the caller falls back to the tree-walking interpreter). Unlike `native_compile_bool`, this handles the FULL computational fragment (recursion, pattern matching, definitions), so recursor-based decisions compile to native code. Its verdict is IDENTICAL to `eval_bool_tree`/`normalize` (differential-tested).
- [fn native_decide](https://docs.logicaffeine.com/logicaffeine_kernel/eval/fn.native_decide): Build a `native_decide` proof of `prop` from a `Decidable prop` instance `inst`: if the decision procedure NATIVELY evaluates to `true`, return the proof term `of_decide_eq_true prop inst (ofReduceBool (decide prop inst) true (refl Bool true))`, which the (main) kernel checks by running this evaluator via the `reduceBool` hook — never by re-normalizing the decision procedure. Returns `None` (fail-safe) when the decision is not `true`, so it can only ever produce proofs of genuinely-true goals.

## logicaffeine_kernel::field_algebra
Kernel algebra for the prime field 𝔽_q of ML-KEM / ML-DSA — the certified arithmetic substrate (F2 seed).

- [const KYBER_Q](https://docs.logicaffeine.com/logicaffeine_kernel/field_algebra/constant.KYBER_Q): Kyber / ML-KEM’s modulus — prime, so ℤ/qℤ is the field 𝔽_q.
- [const MLDSA_MONT_R](https://docs.logicaffeine.com/logicaffeine_kernel/field_algebra/constant.MLDSA_MONT_R): Montgomery radix `R = 2³²` and `qinv = q⁻¹ mod R = 58728449` (the SUBTRACT convention: the reduction is `redc(a) = (a − ((a·qinv) mod R)·q) / R`, matching `mldsa::montgomery_reduce`). The exact integer cofactor `(qinv·q − 1) / R` makes the numerator a clean multiple of `R`.
- [const MLDSA_Q](https://docs.logicaffeine.com/logicaffeine_kernel/field_algebra/constant.MLDSA_Q): Dilithium’s modulus — prime, so ℤ/qℤ is the field 𝔽_q.
- [const MLDSA_QINV](https://docs.logicaffeine.com/logicaffeine_kernel/field_algebra/constant.MLDSA_QINV)
- [const MONT_R](https://docs.logicaffeine.com/logicaffeine_kernel/field_algebra/constant.MONT_R): Montgomery radix `R = 2¹⁶` and `qinv' = −q⁻¹ mod R = 3327`, with the exact integer cofactor `(qinv'·q + 1) / R = 169`. These are the constants of the division-free reduction `redc(x) = (x + ((x·qinv') mod R)·q) / R` used by the (SIMD) ML-KEM NTT.
- [const NEG_QINV_MOD_R](https://docs.logicaffeine.com/logicaffeine_kernel/field_algebra/constant.NEG_QINV_MOD_R)
- [fn conditional_subtract_in_range](https://docs.logicaffeine.com/logicaffeine_kernel/field_algebra/fn.conditional_subtract_in_range): Certify that conditional-subtract reduction keeps a modular-ADD result in range. After an addition in 𝔽_q the value `a` lies in `[0, 2q)`; the reduction is `csub(a) = if a ≥ q { a − q } else { a }`, and the result must lie in `[0, q)`. The two non-trivial bounds (the `a ≥ q` branch) are discharged by Fourier-Motzkin: a goal is valid iff its negation’s constraints are UNSAT.
- [fn gauss_three_multiply_identity](https://docs.logicaffeine.com/logicaffeine_kernel/field_algebra/fn.gauss_three_multiply_identity): Gauss’s three-multiplication identity — the symmetry that turns a 4-multiply bilinear form `ad + bc` into 3 multiplies `(a+b)(c+d) − ac − bd`. It is the archetypal “spend an add to save a multiply” rewrite behind fast complex / polynomial / NTT-butterfly multiplication. Certified as a polynomial identity over any commutative ring by the kernel’s `ring` canonicalizer, so a codegen pass may apply it knowing it is sound.
- [fn mldsa_montgomery_congruence](https://docs.logicaffeine.com/logicaffeine_kernel/field_algebra/fn.mldsa_montgomery_congruence): Certify the ML-DSA Montgomery CONGRUENCE: `(a − lo·q) − a = −q·lo`, so the reduction numerator `redc·R = a − lo·q` differs from `a` by a multiple of `q` ⇒ `redc·R ≡ a (mod q)` ⇒ `redc ≡ a·R⁻¹ (mod q)`. A ring identity in the free variables `a`, `lo`, certified for all values.
- [fn mldsa_montgomery_divisibility](https://docs.logicaffeine.com/logicaffeine_kernel/field_algebra/fn.mldsa_montgomery_divisibility): Certify the ML-DSA Montgomery DIVISIBILITY: `a·qinv·q − a = cofactor·R·a`, i.e. the reduction’s numerator `a − (a·qinv)·q = −cofactor·R·a` is an EXACT multiple of `R` (so `/R` is a shift, never a rounding divide). This holds because `qinv·q ≡ 1 (mod R)`; the `ring` canonicalizer reduces both sides to `a·(qinv·q − 1)`, certifying it for ALL `a`.
- [fn mldsa_montgomery_reduction_certified](https://docs.logicaffeine.com/logicaffeine_kernel/field_algebra/fn.mldsa_montgomery_reduction_certified): The full ML-DSA Montgomery reduction is kernel-certified: the numerator is an exact multiple of `R` (divisibility) and the result is `a·R⁻¹ mod q` (congruence). Together these prove `mldsa::montgomery_reduce` — hence the AVX2 `montmul32` that shares its formula — computes the right field element, with no Z3, for ALL inputs (not a sampled bit-width).
- [fn montgomery_reduction_certified](https://docs.logicaffeine.com/logicaffeine_kernel/field_algebra/fn.montgomery_reduction_certified): The full Montgomery reduction is kernel-certified: the constant divides exactly (so `/R` is a shift), the result is `x·R⁻¹ mod q` (congruence), and the final conditional subtract keeps it in `[0, q)` (range). A single gate over the three procedures.
- [fn montgomery_reduction_congruence](https://docs.logicaffeine.com/logicaffeine_kernel/field_algebra/fn.montgomery_reduction_congruence): Certify the Montgomery CONGRUENCE: `(x + lo·q) − x = q·lo`, so the reduction numerator differs from `x` by a multiple of `q` ⇒ `redc·R ≡ x (mod q)` ⇒ `redc ≡ x·R⁻¹ (mod q)` (`R` is a unit in 𝔽_q). A ring identity in the free variables `x`, `lo`, certified for all values.
- [fn montgomery_reduction_divisibility](https://docs.logicaffeine.com/logicaffeine_kernel/field_algebra/fn.montgomery_reduction_divisibility): Certify the Montgomery DIVISIBILITY: `x + (x·qinv')·q = x·169·R`, i.e. the reduction’s numerator (with the un-reduced `lo = x·qinv'`) is an EXACT multiple of `R` — so `redc`’s `/ R` is an exact shift, never a rounding division. This is what makes `qinv' = 3327` the RIGHT constant (`qinv'·q ≡ −1 mod R`): the kernel `ring` canonicalizer reduces both sides to `x·11075584`, certifying it for ALL `x`, not a sampled width.

## logicaffeine_kernel::inductive_compile
Nested-inductive compiler (K3) — the UNTRUSTED front-end for inductives that recur nested inside a container, `RTree := rnode : TList RTree → RTree`.

- [struct Compiled](https://docs.logicaffeine.com/logicaffeine_kernel/inductive_compile/struct.Compiled): The compiled artifacts of a nested inductive: the mutual block to register, and the iso DEFINITIONS `(name, type, body)` to kernel-check and add. Nothing here is trusted until the caller checks it.
- [struct Elimination](https://docs.logicaffeine.com/logicaffeine_kernel/inductive_compile/struct.Elimination): The auxiliary mutual block Lean’s kernel reduces a nested block to.
- [struct IsoNames](https://docs.logicaffeine.com/logicaffeine_kernel/inductive_compile/struct.IsoNames): One container specialized for this inductive, with the names of its conversion isos.
- [struct NativeRecursor](https://docs.logicaffeine.com/logicaffeine_kernel/inductive_compile/struct.NativeRecursor): A recursor whose motive and constructor terms retain the source container applications.
- [struct NestedBlock](https://docs.logicaffeine.com/logicaffeine_kernel/inductive_compile/struct.NestedBlock): A block of source families, each nesting itself or a sibling inside registered containers: one family, or an ordinary mutual block. The members share `num_params` uniform parameters and the universe parameters `levels`, and may each carry indices of their own.
- [struct NestedDecl](https://docs.logicaffeine.com/logicaffeine_kernel/inductive_compile/struct.NestedDecl): A nested inductive declaration: a name, its sort, and constructors whose argument types may mention the inductive nested inside a registered container (`TList RTree`).
- [struct NestedInfo](https://docs.logicaffeine.com/logicaffeine_kernel/inductive_compile/struct.NestedInfo): What a nested-inductive registration produced: the specialized sibling type names and the conversion isos relating each to its generic container.
- [fn compile_nested](https://docs.logicaffeine.com/logicaffeine_kernel/inductive_compile/fn.compile_nested): Compile a nested inductive into a mutual block plus conversion isos. Untrusted: every artifact is checked by the caller. Handles arbitrary nesting DEPTH (`TList (TList RTree)`) and arbitrary container ARITY (`TPair Nat PTree`) by recursive specialization — each container level becomes its own mutual sibling.
- [fn compile_nested_poly](https://docs.logicaffeine.com/logicaffeine_kernel/inductive_compile/fn.compile_nested_poly): `compile_nested_with_params` for a universe-polymorphic family (`UTree.{u} (α : Type u)`).
- [fn compile_nested_with_params](https://docs.logicaffeine.com/logicaffeine_kernel/inductive_compile/fn.compile_nested_with_params): `compile_nested` for an inductive with `num_params` uniform parameters (`PTree α := node : α → List (PTree α) → PTree α`).
- [fn derive_native_recursors](https://docs.logicaffeine.com/logicaffeine_kernel/inductive_compile/fn.derive_native_recursors): Reconstruct checked generic recursors from the existing mutual generator.
- [fn derive_native_recursors_poly](https://docs.logicaffeine.com/logicaffeine_kernel/inductive_compile/fn.derive_native_recursors_poly): `derive_native_recursors_with_params` for a universe-polymorphic family. Each restored recursor’s levels are its motive universes followed by the family’s own `levels`, in order.
- [fn derive_native_recursors_with_params](https://docs.logicaffeine.com/logicaffeine_kernel/inductive_compile/fn.derive_native_recursors_with_params): `derive_native_recursors` for a nested inductive with `num_params` uniform parameters. The restored recursors abstract the parameters first, exactly as Lean’s generated nested recursors do (`PTree.rec : {α : Type} → {motive_1 …} → {motive_2 …} → …`).
- [fn derive_nested_block_recursors](https://docs.logicaffeine.com/logicaffeine_kernel/inductive_compile/fn.derive_nested_block_recursors): Reconstruct Lean’s recursors for a nested block: the elimination’s mutual recursors, each restored to the source families and container instances and checked again in `ctx`.
- [fn eliminate_nested](https://docs.logicaffeine.com/logicaffeine_kernel/inductive_compile/fn.eliminate_nested): Reduce a nested block to an ordinary mutual block exactly as Lean’s kernel does (`elim_nested_inductive`).

## logicaffeine_kernel::int_inductive
`Int` as a real inductive — Lean’s `ofNat | negSucc` with its arithmetic defined rather than assumed (`Init/Data/Int/Basic.lean:40-45`, `:78-166`). The construction, packaged so the prelude adopts it in one call; the module header carries how Lean keeps it fast anyway. `Int` as a REAL INDUCTIVE — Lean’s `ofNat | negSucc`, with its arithmetic DEFINED.

- [fn canonical_int](https://docs.logicaffeine.com/logicaffeine_kernel/int_inductive/fn.canonical_int): The canonical `Int` term for a machine integer, in Lean’s representation: `ofNat n` for `n ≥ 0`, `negSucc (-n-1)` below. The `Nat` argument is a `Literal::Nat`, not a `Succ` spine, so a large integer costs one node — which is the whole point of the `Nat` literal bridge.
- [fn register_inductive_int](https://docs.logicaffeine.com/logicaffeine_kernel/int_inductive/fn.register_inductive_int): The whole adoption, as one call: `Int` gains Lean’s two constructors and Lean’s arithmetic.
- [fn register_int_arithmetic](https://docs.logicaffeine.com/logicaffeine_kernel/int_inductive/fn.register_int_arithmetic)
- [fn register_int_constructors](https://docs.logicaffeine.com/logicaffeine_kernel/int_inductive/fn.register_int_constructors): `Int`’s two constructors, through the CHECKED door.
- [fn register_nat_arithmetic](https://docs.logicaffeine.com/logicaffeine_kernel/int_inductive/fn.register_nat_arithmetic)
- [fn supports_integer_polynomial_operations](https://docs.logicaffeine.com/logicaffeine_kernel/int_inductive/fn.supports_integer_polynomial_operations): Whether the public add/mul/sub vocabulary has the standard integer meaning.

## logicaffeine_kernel::interface
Vernacular interface for the Kernel.

- [mod lean](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/): Lean 4 kernel export (NDJSON 3.1) as an input surface of the LOGOS kernel.
- [mod literate_parser](https://docs.logicaffeine.com/logicaffeine_kernel/interface/literate_parser/): Literate Specification Parser for the Kernel.
- [mod match_compile](https://docs.logicaffeine.com/logicaffeine_kernel/interface/match_compile/): The equation compiler: surface patterns → the kernel’s positional `Match` tree.
- [mod printer](https://docs.logicaffeine.com/logicaffeine_kernel/interface/printer/): The kernel’s surface, written back: the exact inverse of `term_parser` and `command_parser`.
- [mod surface](https://docs.logicaffeine.com/logicaffeine_kernel/interface/surface/): The SURFACE environment — user-declared notation, fixity and macros.
- [struct BinderSurface](https://docs.logicaffeine.com/logicaffeine_kernel/interface/struct.BinderSurface): Everything the SURFACE says about ONE parameter that the kernel’s three-field `Term::Pi` cannot hold: how it is supplied, and what fills it when the caller does not.
- [struct DeclarationSurface](https://docs.logicaffeine.com/logicaffeine_kernel/interface/struct.DeclarationSurface): A declared type split into the pure kernel type the context is keyed at and the per-parameter surface information that has to be recorded beside it.
- [struct InductiveMember](https://docs.logicaffeine.com/logicaffeine_kernel/interface/struct.InductiveMember): One member of an `Command::InductiveBlock`.
- [struct Repl](https://docs.logicaffeine.com/logicaffeine_kernel/interface/struct.Repl): The Vernacular REPL.
- [struct TermParser](https://docs.logicaffeine.com/logicaffeine_kernel/interface/struct.TermParser): Recursive descent parser for Term syntax.
- [enum BinderKind](https://docs.logicaffeine.com/logicaffeine_kernel/interface/enum.BinderKind): How a parameter is SUPPLIED at a call site – Lean’s four binder kinds.
- [enum Command](https://docs.logicaffeine.com/logicaffeine_kernel/interface/enum.Command): A command in the Vernacular language.
- [enum InterfaceError](https://docs.logicaffeine.com/logicaffeine_kernel/interface/enum.InterfaceError): Errors that can occur in the interface layer.
- [enum ParseError](https://docs.logicaffeine.com/logicaffeine_kernel/interface/enum.ParseError): Parse errors for the Vernacular.
- [fn parse_command](https://docs.logicaffeine.com/logicaffeine_kernel/interface/fn.parse_command): Parse ONE command, and require it to be the WHOLE input.
- [fn parse_command_in_ctx](https://docs.logicaffeine.com/logicaffeine_kernel/interface/fn.parse_command_in_ctx): Parse ONE command with the kernel CONTEXT available, and require it to be the whole input.
- [fn parse_command_prefix_in](https://docs.logicaffeine.com/logicaffeine_kernel/interface/fn.parse_command_prefix_in): Parse ONE command off the FRONT of `input`, returning it with the number of bytes consumed.
- [fn parse_command_prefix_in_ctx](https://docs.logicaffeine.com/logicaffeine_kernel/interface/fn.parse_command_prefix_in_ctx): Parse ONE command off the FRONT of `input` with the kernel CONTEXT available, returning it with the number of bytes consumed.
- [fn standard_context](https://docs.logicaffeine.com/logicaffeine_kernel/interface/fn.standard_context): A context of its own for a REPL or a document to extend: a copy-on-write clone of the process’s one standard library registration, `crate::prelude::StandardLibrary::context`.

## logicaffeine_kernel::interface::lean
Lean 4 kernel export (NDJSON 3.1) as an input surface of the LOGOS kernel.

- [mod emit](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/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.
- [mod intake](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/intake/): Intake: the strict front door of a Lean → LOGOS result.
- [mod native_decide](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/native_decide/): `native_decide`, re-proved by the LOGOS kernel’s own evaluation.
- [mod package](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/package/): The portable proof package (`logos-lean-package/1` and `/2`) and its replay.
- [mod pipeline](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/pipeline/): The Lean → LOGOS pipeline, one named stage at a time, and the benchmark protocol’s dispatch.
- [mod receipt](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/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.
- [mod reference](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/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.
- [mod taint](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/taint/): The taint path of every assumption a refused result rests on: the declarations through which the target reaches it.
- [struct DeclarationAudit](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/struct.DeclarationAudit)
- [struct ImportReport](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/struct.ImportReport)
- [struct ImportRequest](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/struct.ImportRequest): How `import_with` imports.
- [struct ImportedContext](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/struct.ImportedContext): Owned imported artifacts keep the importer’s stack discipline when released.
- [struct InternalHelper](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/struct.InternalHelper): Checked conservative definitions introduced to preserve source DAG sharing.
- [struct MetadataLoss](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/struct.MetadataLoss)
- [struct Reason](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/struct.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.
- [struct RuntimeDeclaration](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/struct.RuntimeDeclaration): Source-only runtime metadata. No corresponding axiom or body enters Context.
- [enum DiagnosticCode](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/enum.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.
- [enum Outcome](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/enum.Outcome): The outcome of a `logos-lean-result/1` document, with the contract’s exit code.
- [enum RetainSource](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/enum.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.
- [enum Verdict](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/enum.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).
- [fn check_str](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/fn.check_str)
- [fn check_str_with_declaration_audit](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/fn.check_str_with_declaration_audit)
- [fn check_str_with_report](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/fn.check_str_with_report)
- [fn import](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/fn.import): Import the export and return its checked context: no audit, nothing retained, Lean’s binder names carried.
- [fn import_audited](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/fn.import_audited)
- [fn import_audited_retaining](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/fn.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.
- [fn import_audited_retaining_source](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/fn.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.
- [fn import_retaining_closure](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/fn.import_retaining_closure): The pipeline’s import of `target`: audited, retaining `target`’s dependency closure, with `target` as the `retained_source`.
- [fn import_with](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/fn.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.
- [fn lean_binder_name](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/fn.lean_binder_name): The Lean binder name an imported binder carries, when the import kept one.
- [fn lean_type](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/fn.lean_type)

## logicaffeine_kernel::interface::lean::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.

- [struct Correspondence](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/emit/struct.Correspondence): One Lean declaration and the LOGOS declaration that carries it.
- [struct EmittedDocument](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/emit/struct.EmittedDocument): An emitted document.
- [enum DeclarationKind](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/emit/enum.DeclarationKind): What a declaration is, as the kernel holds it.
- [enum EmissionFault](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/emit/enum.EmissionFault): Why an emitted document does not reparse to the imported declarations. Every variant names the LOGOS declaration it concerns.
- [enum Form](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/emit/enum.Form): Which surface carries a declaration in the document.
- [enum LeanPart](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/emit/enum.LeanPart): One component of a Lean name.
- [enum Origin](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/emit/enum.Origin): Where a LOGOS declaration came from.
- [enum Published](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/emit/enum.Published): What a publication left in place.
- [const DOCUMENT_EXTENSION](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/emit/constant.DOCUMENT_EXTENSION): The published document’s extension.
- [const FAILURE_EXTENSION](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/emit/constant.FAILURE_EXTENSION): The extension of a failed run’s diagnostic record.
- [const MAX_SOURCE_BYTES](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/emit/constant.MAX_SOURCE_BYTES): The largest document the emitter writes.
- [fn check_statement](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/emit/fn.check_statement): Rule R8: the target’s REPARSED statement against `reference`, an independent translation of the Lean declaration (`reference::reference_declaration`) in the importer’s names. The reference is carried into LOGOS names through the correspondence alone — the emitter’s own terms play no part — and must name the target, bind the same universe parameters in the same order, and state the same type up to α.
- [fn emit_context](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/emit/fn.emit_context): `emit_document` over any checked context whose constants carry the importer’s key scheme. `proofs` hands back the checked proof of an opaque theorem, which a context does not keep.
- [fn emit_document](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/emit/fn.emit_document): The dependency closure of `target`, as a LOGOS document.
- [fn publish](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/emit/fn.publish): Publish `outcome` under `dir/<stem>.lg`, or its failure under `dir/<stem>.failure.txt`.
- [fn publish_through](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/emit/fn.publish_through): `publish`, writing every file’s bytes through `write` — the seam a test uses to make a write fail half way.
- [fn verify](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/emit/fn.verify): Reparse `document.source` in a fresh context and compare every declaration with what it must be. Returns the checked context.

## logicaffeine_kernel::interface::lean::intake
Intake: the strict front door of a Lean → LOGOS result.

- [struct Declaration](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/intake/struct.Declaration): One declared constant.
- [struct Header](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/intake/struct.Header): The export’s first record.
- [struct Intake](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/intake/struct.Intake): An export that passed intake.
- [struct Profile](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/intake/struct.Profile): The toolchain and assumption profile a result is produced under.
- [enum Component](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/intake/enum.Component): One component of a Lean name.
- [enum DeclarationKind](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/intake/enum.DeclarationKind): What a declaration record declares.
- [const EXPORTER_FLAGS](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/intake/constant.EXPORTER_FLAGS): The exporter flags every result is produced with: metadata and unsafe declarations are exported so that the reader, not the exporter, decides what they mean.
- [const EXPORTER_REVISION](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/intake/constant.EXPORTER_REVISION): The pinned lean4export revision.
- [const EXPORTER_SOURCES](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/intake/constant.EXPORTER_SOURCES): SHA-256 of the pinned exporter’s sources at `EXPORTER_REVISION`. The exporter is identified by its content, never by the name of the directory holding it.
- [const STAGE_A](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/intake/constant.STAGE_A): Stage A: Lean 4.14.0, lean4export 3.1.0 (revision `EXPORTER_REVISION`), export format 3.1.0, Lean core only, and Lean’s three standard axioms.
- [const TOOLCHAIN](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/intake/constant.TOOLCHAIN): The elan toolchain name of the pinned Lean.
- [fn components](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/intake/fn.components): The components of a kernel identity, when it is the encoding of a Lean name.
- [fn encode](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/intake/fn.encode): The structural encoding of a Lean name, before the reader’s reserved identities apply.
- [fn kernel_name](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/intake/fn.kernel_name): The kernel identity the reader registers the dotted Lean name `lean` under.
- [fn lean_name](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/intake/fn.lean_name): The dotted Lean name a kernel identity encodes, as Lean prints it; a kernel name that encodes no Lean name is returned unchanged.
- [fn parse_lean_name](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/intake/fn.parse_lean_name): Parse a dotted Lean name as Lean prints it: components separated by `.`, a component that is not an identifier written `«…»`, a component of digits numeric.
- [fn print_lean_name](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/intake/fn.print_lean_name): Print components as Lean prints a name.
- [fn read](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/intake/fn.read): Read and validate an export under `profile`.
- [fn read_header](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/intake/fn.read_header): The header, held to the profile: the format version first (a newer format may legitimately add fields), then the header’s own fields, then the producing toolchain.

## logicaffeine_kernel::interface::lean::native_decide
`native_decide`, re-proved by the LOGOS kernel’s own evaluation.

- [struct Elimination](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/native_decide/struct.Elimination): What a target’s closure rests on once its leaves are re-derived.
- [struct NativeDecision](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/native_decide/struct.NativeDecision): One recognized leaf: Lean’s appeal to its compiler, and the pieces its re-derivation keeps.
- [struct NativeDecisions](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/native_decide/struct.NativeDecisions): The native decisions of one export.
- [struct Rederivation](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/native_decide/struct.Rederivation): One declaration whose type or value holds re-derived leaves.
- [const ELIMINATED_AXIOM](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/native_decide/constant.ELIMINATED_AXIOM): The trust escape a re-derived leaf no longer rests on, as Lean’s `#print axioms` names it.
- [const INFORMATION_CATEGORY](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/native_decide/constant.INFORMATION_CATEGORY): The information-change category a re-derivation is disclosed under.
- [const METHOD](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/native_decide/constant.METHOD): How a disclosed step was re-derived.

## logicaffeine_kernel::interface::lean::package
The portable proof package (`logos-lean-package/1` and `/2`) and its replay.

- [struct AssumptionRecord](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/package/struct.AssumptionRecord)
- [struct Build](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/package/struct.Build): A built package and the producing run’s receipt. A build never claims more than its receipt: `assemble` is the door that refuses to hand out a package whose receipt is not clean.
- [struct BuildOptions](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/package/struct.BuildOptions): What the producing run knows that the export does not say.
- [struct CorrespondenceFile](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/package/struct.CorrespondenceFile)
- [struct CorrespondenceRow](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/package/struct.CorrespondenceRow)
- [struct EmissionRecord](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/package/struct.EmissionRecord)
- [struct InformationLoss](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/package/struct.InformationLoss)
- [struct LeanRun](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/package/struct.LeanRun): A pinned Lean toolchain’s run over the original source.
- [struct Manifest](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/package/struct.Manifest)
- [struct PackageLimits](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/package/struct.PackageLimits): Limits enforced on a package before any work.
- [struct SourceIdentity](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/package/struct.SourceIdentity)
- [struct StageRecord](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/package/struct.StageRecord)
- [struct TargetIdentity](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/package/struct.TargetIdentity)
- [struct Toolchain](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/package/struct.Toolchain)
- [const ALLOWED_AXIOMS](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/package/constant.ALLOWED_AXIOMS): Lean’s three standard axioms, in the kernel’s spelling of their Lean names — the only assumptions a verified result may rest on.
- [const CERTIFICATE](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/package/constant.CERTIFICATE)
- [const CORRESPONDENCE](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/package/constant.CORRESPONDENCE)
- [const CORRESPONDENCE_SCHEMA](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/package/constant.CORRESPONDENCE_SCHEMA)
- [const EXPORT](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/package/constant.EXPORT)
- [const MANIFEST](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/package/constant.MANIFEST)
- [const NATIVE_REDERIVED_SCHEMA](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/package/constant.NATIVE_REDERIVED_SCHEMA): The schema of a package whose proof is the export’s with the native decisions of the target’s closure re-derived by kernel evaluation.
- [const PACKAGE_SCHEMA](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/package/constant.PACKAGE_SCHEMA): The schema of a package whose proof is the export’s own, checked as exported.
- [const PACKAGE_SCHEMAS](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/package/constant.PACKAGE_SCHEMAS): Every package schema this crate writes and replays.
- [const REPLAY_SCHEMA](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/package/constant.REPLAY_SCHEMA)
- [const TRUSTED_BASE](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/package/constant.TRUSTED_BASE): The trusted computing base shared by the checks a package’s receipt names. Two checkers that share this much are two implementations of typing, not two independent theorem provers, and the manifest says so in every package.
- [fn assemble](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/package/fn.assemble): Build the package for `target` from a Lean export, and require that every stage the producing run can establish passed. A package is returned only when it would replay clean.
- [fn assemble_observed](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/package/fn.assemble_observed): `assemble_with`, holding the result’s assumptions against what the pinned Lean’s own `#print axioms` reported for the target (Lean names), as the package’s contract says: any difference in either direction, and a native-rederived proof without Lean’s report, is an `assumption_disagreement`, and no package is handed out.
- [fn assemble_with](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/package/fn.assemble_with): `assemble` with the producing run’s own evidence.
- [fn build](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/package/fn.build): Build a package and its producing receipt. Refuses only when no package can be formed at all (an export the importer does not accept, a target it does not declare); a package whose checks fail is returned with the failure on its receipt, so a refusal can be inspected and replayed.
- [fn build_observed](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/package/fn.build_observed): `build`, with the pinned Lean’s `#print axioms` for the target when the producing run has it.
- [fn canonical_certificate](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/package/fn.canonical_certificate): The certificate’s canonical encoding: compact, newline-terminated.
- [fn canonical_json](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/package/fn.canonical_json): The one canonical encoding of a package JSON file: pretty-printed, newline-terminated.
- [fn document_path](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/package/fn.document_path): The document’s file name for a Lean target: its name with anything outside letters, digits, `_`, `-` and `.` written as `_`, then `.lg`.
- [fn publish](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/package/fn.publish): Write a package to `dir` atomically: every file is written and synced in a staging directory beside it, which is then renamed into place. An existing `dir` is never replaced — a published result is immutable — and a failure leaves nothing behind.
- [fn publishable](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/package/fn.publishable): The package of `build`, when every stage the producing run can establish passed and the package replays clean in this process; otherwise the first stage that did not pass, as a refusal.
- [fn read_directory](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/package/fn.read_directory): Read a package directory, enforcing the file-count, size and path limits before reading any content. Symbolic links and special files are refused.
- [fn receipt_document](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/package/fn.receipt_document): The replay receipt as a `logos-lean-replay/1` document.
- [fn replay](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/package/fn.replay): Replay a package from its bytes alone, under the default limits.
- [fn replay_with](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/package/fn.replay_with): Replay a package from its bytes alone, under `limits`.
- [fn result_id](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/package/fn.result_id): The result identity of a `logos-lean-package/1` package: the target and every non-manifest file’s path and digest.
- [fn result_id_in](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/package/fn.result_id_in): The result identity under `schema`, which is the preimage’s domain: the same files under two contracts have two identities.
- [fn sha256_hex](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/package/fn.sha256_hex): The lowercase hexadecimal SHA-256 of `bytes`.
- [type PackageFiles](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/package/type.PackageFiles): A package’s files, keyed by published relative path.

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

- [struct Checked](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/pipeline/struct.Checked): A result and, when every stage up to packaging passed, the package to publish and replay.
- [struct Diagnostic](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/pipeline/struct.Diagnostic): One typed, located diagnostic of a result.
- [struct LeanResult](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/pipeline/struct.LeanResult): A `logos-lean-result/1` document under construction.
- [struct Limits](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/pipeline/struct.Limits): Budgets declared before any work.
- [struct Loss](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/pipeline/struct.Loss): Information the result does not carry from the Lean input.
- [struct PackageRef](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/pipeline/struct.PackageRef): A published package, as the result names it.
- [enum LeanEvidence](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/pipeline/enum.LeanEvidence): What the run observed of Lean itself.
- [const RESULT_SCHEMA](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/pipeline/constant.RESULT_SCHEMA)
- [fn check_export](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/pipeline/fn.check_export): Run every in-process stage over a Lean export for the dotted Lean name `target`: intake, import and check, independent recheck, assumption policy, emission and package assembly. `fresh_replay` is left to the caller, which must replay the published package in a new process.
- [fn run_cli](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/pipeline/fn.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.
- [fn self_verification_failure](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/pipeline/fn.self_verification_failure): A refusal of LOGOS’s own artifact — emission, packaging, replay — once every check of the user’s input passed. Unsupported capabilities, budgets and environment failures keep their codes; any other refusal (a rejection, a malformed or ill-typed artifact of our own making) is an `InternalInconsistency`: the fault is ours, and it is never reported as the user’s mathematics being wrong.

## logicaffeine_kernel::interface::lean::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.

- [struct Receipt](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/receipt/struct.Receipt): A receipt: one entry per stage in `STAGES`, in order. Verified only when every stage passed.
- [struct Stage](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/receipt/struct.Stage)
- [enum StageStatus](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/receipt/enum.StageStatus): What happened in one stage. `NotRun` and `Unsupported` are never a pass.
- [const REPLAY_STAGES](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/receipt/constant.REPLAY_STAGES): The stages a replay establishes from a package’s bytes alone. `lean_accepted` is not among them: a replay never runs Lean, and says so rather than inheriting the producing run’s word.
- [const STAGES](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/receipt/constant.STAGES): Every stage, in the order a result passes through them.

## logicaffeine_kernel::interface::lean::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.

- [struct Reference](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/reference/struct.Reference): An export read once, for reading many declarations from it.
- [struct ReferenceDeclaration](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/reference/struct.ReferenceDeclaration): One declaration as the reference translator reads it.
- [enum ReferenceKind](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/reference/enum.ReferenceKind): What a Lean declaration record is, as far as the statement binding needs to know.
- [const REFERENCE_NODE_BUDGET](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/reference/constant.REFERENCE_NODE_BUDGET): The largest term (in tree nodes) the reference translation will build. Exports share subexpressions as a DAG; a tree unfolding is bounded so a hostile export cannot make the oracle allocate without limit.
- [fn kernel_name_of_components](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/reference/fn.kernel_name_of_components): The kernel spelling of a Lean name given as its hierarchical components.
- [fn reference_declaration](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/reference/fn.reference_declaration): The whole reference reading of one declaration: kernel name, kind, universe parameters and type.
- [fn reference_type](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/reference/fn.reference_type): The type of `declaration` as the reference translator reads it from `export`.

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

- [struct TaintPath](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/taint/struct.TaintPath): One assumption and the Lean declarations through which the target reaches it, target first and the assumption last, in Lean’s spelling.
- [const STAGE](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/taint/constant.STAGE): The receipt stage whose refusal a taint path explains.
- [fn diagnostics](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/taint/fn.diagnostics): One `disallowed_assumption` diagnostic of the assumption-policy stage per assumption outside Lean’s three standard axioms that `target` (a kernel name, printed as `target_lean`) rests on, naming its taint path. `assumptions` are the result’s (Lean names).
- [fn taint_paths](https://docs.logicaffeine.com/logicaffeine_kernel/interface/lean/taint/fn.taint_paths): The taint path of each of `assumptions` (Lean names) from `target` (a kernel name), in the order `assumptions` lists them. An assumption the target does not reach through the environment has no path and is left out.

## logicaffeine_kernel::interface::literate_parser
Literate Specification Parser for the Kernel.

- [const ONE_SHOT_TACTICS](https://docs.logicaffeine.com/logicaffeine_kernel/interface/literate_parser/constant.ONE_SHOT_TACTICS): The closed one-shot tactic vocabulary of the literate `Proof:` surface: the keyword a mathematician writes, and the reflected tactic it applies to the reified goal. Adding a tactic is a row here — `parse_proof_tactic` and `parse_single_tactic` both read this table, so the two doors can never drift apart again.
- [fn measure_definition](https://docs.logicaffeine.com/logicaffeine_kernel/interface/literate_parser/fn.measure_definition): The EXTENT of the `## To` block at the front of `input` — where it ends — read from its syntax alone. See `measure_theorem`.
- [fn measure_theorem](https://docs.logicaffeine.com/logicaffeine_kernel/interface/literate_parser/fn.measure_theorem): The EXTENT of the `## Theorem:` block at the front of `input`, read from its syntax alone.
- [fn parse_definition](https://docs.logicaffeine.com/logicaffeine_kernel/interface/literate_parser/fn.parse_definition): Parse “## To [name] (params) -> RetType:” into Command::Definition
- [fn parse_definition_in](https://docs.logicaffeine.com/logicaffeine_kernel/interface/literate_parser/fn.parse_definition_in): `parse_definition`, with the kernel context the equation compiler needs.
- [fn parse_definition_scoped](https://docs.logicaffeine.com/logicaffeine_kernel/interface/literate_parser/fn.parse_definition_scoped): `parse_definition_in`, reading every name in the namespace scope `scope` — the door the REPL reads through, so a literate definition’s names mean exactly what they mean to every other door.
- [fn parse_inductive](https://docs.logicaffeine.com/logicaffeine_kernel/interface/literate_parser/fn.parse_inductive): Parse “A [Name] is either…” into Command::Inductive
- [fn parse_let_definition](https://docs.logicaffeine.com/logicaffeine_kernel/interface/literate_parser/fn.parse_let_definition): Parse “Let [name] be [term].” into Command::Definition (constant, not function)
- [fn parse_theorem](https://docs.logicaffeine.com/logicaffeine_kernel/interface/literate_parser/fn.parse_theorem): Parse “## Theorem: [name] Statement: [proposition].” into Command::Definition
- [fn parse_theorem_in](https://docs.logicaffeine.com/logicaffeine_kernel/interface/literate_parser/fn.parse_theorem_in): `parse_theorem`, with the kernel context.
- [fn parse_theorem_scoped](https://docs.logicaffeine.com/logicaffeine_kernel/interface/literate_parser/fn.parse_theorem_scoped): `parse_theorem_in`, reading every name in the namespace scope `scope`. The statement is reflected into syntax only after its names are resolved, so a theorem about `add` in a session that shadows `add` is a theorem about the session’s `add`.

## logicaffeine_kernel::interface::match_compile
The equation compiler: surface patterns → the kernel’s positional `Match` tree.

- [struct Clause](https://docs.logicaffeine.com/logicaffeine_kernel/interface/match_compile/struct.Clause): One equation: one pattern per column, and the body those patterns’ variables are free in.
- [struct CompileReport](https://docs.logicaffeine.com/logicaffeine_kernel/interface/match_compile/struct.CompileReport): What the compiler noticed on the way through, beyond the term itself.
- [enum Pattern](https://docs.logicaffeine.com/logicaffeine_kernel/interface/match_compile/enum.Pattern): A surface pattern, exactly as a `When` clause spells it.
- [fn compile_clauses](https://docs.logicaffeine.com/logicaffeine_kernel/interface/match_compile/fn.compile_clauses): Compile a clause matrix against a list of scrutinees.
- [fn compile_clauses_reporting](https://docs.logicaffeine.com/logicaffeine_kernel/interface/match_compile/fn.compile_clauses_reporting): `compile_clauses`, plus what the compiler noticed.
- [fn pattern_binder_types](https://docs.logicaffeine.com/logicaffeine_kernel/interface/match_compile/fn.pattern_binder_types): The types a pattern’s binders take when it is matched against a value of `disc_ty`.

## logicaffeine_kernel::interface::printer
The kernel’s surface, written back: the exact inverse of `term_parser` and `command_parser`.

- [enum PrintError](https://docs.logicaffeine.com/logicaffeine_kernel/interface/printer/enum.PrintError): A term or command the LOGOS surface cannot spell (yet).
- [fn inductive_command](https://docs.logicaffeine.com/logicaffeine_kernel/interface/printer/fn.inductive_command): The vernacular command that registers the inductive block `name` belongs to, EXACTLY as `ctx` holds it — its universe telescope, each member’s written parameters (the context’s declared parameter count), its arity past them, and each constructor’s type past them.
- [fn print_command](https://docs.logicaffeine.com/logicaffeine_kernel/interface/printer/fn.print_command): Spell `command` as one vernacular command, terminated by its period.
- [fn print_term](https://docs.logicaffeine.com/logicaffeine_kernel/interface/printer/fn.print_term): Spell `term` in the kernel term surface.
- [fn print_term_in](https://docs.logicaffeine.com/logicaffeine_kernel/interface/printer/fn.print_term_in): Spell `term` read in a context whose locals are `locals`: each prints as its own name. A goal and its hypotheses are spelled this way for a reader; a closed term’s round trip is `print_term`’s, which refuses a free name because the surface would read it as a global.
- [fn structure_commands](https://docs.logicaffeine.com/logicaffeine_kernel/interface/printer/fn.structure_commands): The commands that make `name` a STRUCTURE exactly as `ctx` holds it: each projection’s definition (under the inductive’s universe telescope), then `Structure name := proj₀ … projₙ.` Empty when `ctx` holds no structure information for `name`. Emit them right after the block from `inductive_command`, before anything — a recursor whose body is written through the projections, say — relies on structure η.

## logicaffeine_kernel::interface::surface
The SURFACE environment — user-declared notation, fixity and macros.

- [struct Env](https://docs.logicaffeine.com/logicaffeine_kernel/interface/surface/struct.Env): The environment a written name is resolved against — the two questions resolution asks of it, as closures, which is what keeps the kernel out of the surface.
- [struct Name](https://docs.logicaffeine.com/logicaffeine_kernel/interface/surface/struct.Name): A hierarchical name — Lean’s `Name`, which is a LIST of components and not a string with dots.
- [struct Namespaces](https://docs.logicaffeine.com/logicaffeine_kernel/interface/surface/struct.Namespaces): The namespace scope: what is CURRENT, and what is OPEN.
- [struct OpenClause](https://docs.logicaffeine.com/logicaffeine_kernel/interface/surface/struct.OpenClause): One `open` clause: a namespace, and WHICH of its names it brings in, under WHICH spelling.
- [struct ScopeMark](https://docs.logicaffeine.com/logicaffeine_kernel/interface/surface/struct.ScopeMark): Where a scope stood, so a scoped `Open … in …` (or a declaration’s own implicit namespace) can be wound back EXACTLY, without knowing what it pushed.
- [struct Surface](https://docs.logicaffeine.com/logicaffeine_kernel/interface/surface/struct.Surface): The surface environment: a stack of scopes, innermost last.
- [enum Assoc](https://docs.logicaffeine.com/logicaffeine_kernel/interface/surface/enum.Assoc): Which way a chain of one operator nests.
- [enum OperatorForm](https://docs.logicaffeine.com/logicaffeine_kernel/interface/surface/enum.OperatorForm): The shape a fixity command implies for its operator.
- [enum Resolution](https://docs.logicaffeine.com/logicaffeine_kernel/interface/surface/enum.Resolution): What a written name denotes, once the scope has had its say.
- [enum SurfaceDecl](https://docs.logicaffeine.com/logicaffeine_kernel/interface/surface/enum.SurfaceDecl): A declaration that extends the SURFACE rather than the context. Emitted by the command parser, applied by the REPL — so the one place a parser extension can land is the surface environment.
- [const ANONYMOUS_SECTION](https://docs.logicaffeine.com/logicaffeine_kernel/interface/surface/constant.ANONYMOUS_SECTION): How an ANONYMOUS section is named in a report. Lean’s `section` may be written with no name at all, and a scope with no name still has to be reportable — as an unclosed scope at the end of a document, and as the scope a mismatched `End` failed to close.
- [const ROOT_ESCAPE](https://docs.logicaffeine.com/logicaffeine_kernel/interface/surface/constant.ROOT_ESCAPE): The one name that is never relative: `_root_.x` is the absolute `x`, whatever is open.
- [fn fill_defaults](https://docs.logicaffeine.com/logicaffeine_kernel/interface/surface/fn.fill_defaults): Fill every OMITTED DEFAULT ARGUMENT in `term`, at every application spine in it.
- [fn resolve_names](https://docs.logicaffeine.com/logicaffeine_kernel/interface/surface/fn.resolve_names): `resolve_names_in` against an environment that is only its declared keys — `known` — and shadows nothing.
- [fn resolve_names_in](https://docs.logicaffeine.com/logicaffeine_kernel/interface/surface/fn.resolve_names_in): Resolve every global name written in `term` against the scope, BEFORE any elaboration sees it — Lean’s staging, and the whole content of “name resolution completes before translation begins”.
- [fn respell_names](https://docs.logicaffeine.com/logicaffeine_kernel/interface/surface/fn.respell_names): The inverse of `resolve_names_in`, for a term already in KEY space: every global is re-spelled so that resolving the result in this same scope reaches exactly the key it holds now.

## logicaffeine_kernel::lia
Linear Integer Arithmetic via Fourier-Motzkin Elimination

- [struct Constraint](https://docs.logicaffeine.com/logicaffeine_kernel/lia/struct.Constraint): A linear constraint representing either `expr <= 0` or `expr < 0`.
- [struct LinearExpr](https://docs.logicaffeine.com/logicaffeine_kernel/lia/struct.LinearExpr): A linear expression of the form c₀ + c₁x₁ + c₂x₂ + … + cₙxₙ.
- [struct Rational](https://docs.logicaffeine.com/logicaffeine_kernel/lia/struct.Rational): An exact rational number: a fraction kept in lowest terms with a strictly positive denominator. Built on `BigInt`, so it never rounds the way a JSON / `f64` “number” does — `1/3` stays exactly `1/3`, not `0.3333…`, and a numerator past 2^53 survives instead of collapsing onto a double.
- [enum LiaError](https://docs.logicaffeine.com/logicaffeine_kernel/lia/enum.LiaError): Error during reification to linear expression
- [fn extract_comparison](https://docs.logicaffeine.com/logicaffeine_kernel/lia/fn.extract_comparison): Extract comparison from goal: (SApp (SApp (SName “Lt”|“Le”|“Gt”|“Ge”) lhs) rhs)
- [fn fourier_motzkin_unsat](https://docs.logicaffeine.com/logicaffeine_kernel/lia/fn.fourier_motzkin_unsat): Check if a constraint set is unsatisfiable using Fourier-Motzkin elimination.
- [fn goal_to_negated_constraint](https://docs.logicaffeine.com/logicaffeine_kernel/lia/fn.goal_to_negated_constraint): Convert a goal to constraints for validity checking.
- [fn reify_linear](https://docs.logicaffeine.com/logicaffeine_kernel/lia/fn.reify_linear): Reify a Syntax term to a linear expression.

## logicaffeine_kernel::observational
Certified universe-polymorphic quotient primitives. Observational equality: `Obs.{u} A a b : SProp`, an equality over every type that computes on the weak-head normal form of `A`, with `Obs_refl`, `Obs_transp` (its elimination, into `SProp` only) and `Obs_cast` (a value carried along an equality of types), after Pujet and Tabareau’s CC^obs.

- [fn register](https://docs.logicaffeine.com/logicaffeine_kernel/observational/fn.register): The `SProp` connectives and the four constants, certified.

## logicaffeine_kernel::omega
Omega Test: True Integer Arithmetic Decision Procedure

- [struct IntConstraint](https://docs.logicaffeine.com/logicaffeine_kernel/omega/struct.IntConstraint): Integer constraint representing `expr <= 0` or `expr < 0`.
- [struct IntExpr](https://docs.logicaffeine.com/logicaffeine_kernel/omega/struct.IntExpr): Integer linear expression of the form c + a₁x₁ + a₂x₂ + … + aₙxₙ.
- [fn extract_comparison](https://docs.logicaffeine.com/logicaffeine_kernel/omega/fn.extract_comparison): Extract comparison from goal: (SApp (SApp (SName “Lt”|“Le”|“Gt”|“Ge”) lhs) rhs)
- [fn goal_to_negated_constraint](https://docs.logicaffeine.com/logicaffeine_kernel/omega/fn.goal_to_negated_constraint): Convert a goal to constraints for validity checking using integer semantics.
- [fn omega_unsat](https://docs.logicaffeine.com/logicaffeine_kernel/omega/fn.omega_unsat): Check if integer constraints are unsatisfiable using the Omega test.
- [fn reify_int_linear](https://docs.logicaffeine.com/logicaffeine_kernel/omega/fn.reify_int_linear): Reify a Syntax term to an integer linear expression.

## logicaffeine_kernel::positivity
Strict positivity checking for inductive types.

- [fn check_positivity](https://docs.logicaffeine.com/logicaffeine_kernel/positivity/fn.check_positivity): Check strict positivity in a constructor type without unfolding definitions.
- [fn check_positivity_mutual](https://docs.logicaffeine.com/logicaffeine_kernel/positivity/fn.check_positivity_mutual): Check strict positivity of a MUTUAL BLOCK of inductives in a constructor type.
- [fn check_positivity_mutual_resolved](https://docs.logicaffeine.com/logicaffeine_kernel/positivity/fn.check_positivity_mutual_resolved): `check_positivity_resolved` for a MUTUAL block — the same δ resolution, and a member hidden behind an alias is a member of the block for every question asked here.
- [fn check_positivity_resolved](https://docs.logicaffeine.com/logicaffeine_kernel/positivity/fn.check_positivity_resolved): Strict positivity with every REFERENCE resolved — the paradox fence that a definitional alias cannot walk around.

## logicaffeine_kernel::prelude
Standard Library for the Kernel.

- [struct AxiomUsage](https://docs.logicaffeine.com/logicaffeine_kernel/prelude/struct.AxiomUsage): What a proof rests on: the axioms it cites transitively, and the names that resolve to nothing.
- [struct StandardLibrary](https://docs.logicaffeine.com/logicaffeine_kernel/prelude/struct.StandardLibrary): Standard library definitions.
- [const ADMITTED_AXIOMS](https://docs.logicaffeine.com/logicaffeine_kernel/prelude/constant.ADMITTED_AXIOMS): Names that mark a proof as ADMITTED rather than proved.
- [const FOREIGN_AXIOMS](https://docs.logicaffeine.com/logicaffeine_kernel/prelude/constant.FOREIGN_AXIOMS): Axioms and constants LOGOS deliberately does NOT have, each with the sentence a diagnostic should say instead of “unbound variable”.
- [fn axiom_dependencies](https://docs.logicaffeine.com/logicaffeine_kernel/prelude/fn.axiom_dependencies): Every AXIOM a term actually depends on — Lean’s `#print axioms`, as a function.
- [fn axiom_dependencies_given](https://docs.logicaffeine.com/logicaffeine_kernel/prelude/fn.axiom_dependencies_given): The axiom closure of `term`, as `axiom_dependencies`, where `known` answers the axioms of a constant whose closure was already taken: the walk takes that answer at the constant instead of walking below it. Reachability is transitive, so the answer is what the walk would have found there, and a constant whose closure was taken had every name below it resolved. An importer that audits each declaration in order passes the sets it recorded, so a declaration’s walk covers its own terms and what is not yet audited rather than the whole closure again.
- [fn axiom_dependencies_of](https://docs.logicaffeine.com/logicaffeine_kernel/prelude/fn.axiom_dependencies_of): The axiom closure of a NAMED constant in a context — what `Print Axioms <name>.` reports.
- [fn foreign_axiom_note](https://docs.logicaffeine.com/logicaffeine_kernel/prelude/fn.foreign_axiom_note): The diagnostic sentence for a constant the trusted base deliberately lacks, or `None` when the name is simply not registered (a typo, a missing import, an out-of-scope local).
- [fn is_admitted_axiom](https://docs.logicaffeine.com/logicaffeine_kernel/prelude/fn.is_admitted_axiom): Whether a name marks an admitted (not proved) step.

## logicaffeine_kernel::quotient
Certified universe-polymorphic quotient primitives for kernel importers.

- [enum Kind](https://docs.logicaffeine.com/logicaffeine_kernel/quotient/enum.Kind)
- [fn install](https://docs.logicaffeine.com/logicaffeine_kernel/quotient/fn.install): Install only a canonical primitive, never an arbitrary trusted input type. The importer separately compares its serialized signature with this one.
- [fn signature](https://docs.logicaffeine.com/logicaffeine_kernel/quotient/fn.signature): The canonical Lean signature, with explicit universe instances throughout.

## logicaffeine_kernel::recheck
An independent proof-term re-checker (the de Bruijn criterion taken seriously).

- [struct Incomplete](https://docs.logicaffeine.com/logicaffeine_kernel/recheck/struct.Incomplete): Why the independent kernel reached no verdict, and its account of the stop.
- [enum DoubleCheck](https://docs.logicaffeine.com/logicaffeine_kernel/recheck/enum.DoubleCheck): The verdict of cross-checking a term with BOTH kernels.
- [enum IncompleteKind](https://docs.logicaffeine.com/logicaffeine_kernel/recheck/enum.IncompleteKind): What stopped the independent kernel.
- [enum ReCheckError](https://docs.logicaffeine.com/logicaffeine_kernel/recheck/enum.ReCheckError): Why the re-checker could not produce a verdict, split by soundness meaning.
- [fn double_check](https://docs.logicaffeine.com/logicaffeine_kernel/recheck/fn.double_check): Cross-check `term` against both `infer_type` and `recheck`.
- [fn primitive_rule_names](https://docs.logicaffeine.com/logicaffeine_kernel/recheck/fn.primitive_rule_names): The names in `PRIMITIVE_RULES` — the reading surface the cross-kernel ratchet needs, so the table can be compared against the first kernel’s dispatcher from a test rather than by eye.
- [fn recheck](https://docs.logicaffeine.com/logicaffeine_kernel/recheck/fn.recheck): Independently re-check `term` in `ctx`, returning its inferred type on success.

## logicaffeine_kernel::recursor
R2 — auto-derived recursors (dependent eliminators) for inductive types.

- [struct DerivedAux](https://docs.logicaffeine.com/logicaffeine_kernel/recursor/struct.DerivedAux): One derived auxiliary: the name Lean gives it, the type the kernel certified for it, and the term it certified.
- [fn derive_auxiliaries](https://docs.logicaffeine.com/logicaffeine_kernel/recursor/fn.derive_auxiliaries): Everything the declaration of `ind` should bring with it, in DEPENDENCY ORDER, for a caller to register verbatim:
- [fn derive_below](https://docs.logicaffeine.com/logicaffeine_kernel/recursor/fn.derive_below): `I_below : Π(A…). Π(motive : I A… → Type 0). I A… → Type 0`
- [fn derive_brec_on](https://docs.logicaffeine.com/logicaffeine_kernel/recursor/fn.derive_brec_on): `I_brecOn : Π(A…). Π(motive : I A… → Type 0). Π(t : I A…). Π(F : Π(s). I_below A… motive s → motive s). motive t`
- [fn derive_cases_on](https://docs.logicaffeine.com/logicaffeine_kernel/recursor/fn.derive_cases_on): `I_casesOn` — `recOn` with the INDUCTION HYPOTHESES dropped from every minor premise.
- [fn derive_ctor_inj](https://docs.logicaffeine.com/logicaffeine_kernel/recursor/fn.derive_ctor_inj): `C_inj : Π(A…). Π(x⃗). Π(y⃗). Eq (I A…) (C A… x⃗) (C A… y⃗) → (x₀ = y₀ ∧ … ∧ x_{m-1} = y_{m-1})`
- [fn derive_dec_eq](https://docs.logicaffeine.com/logicaffeine_kernel/recursor/fn.derive_dec_eq): `decEqI : Π(A…). Π(dA_i : Π(u v : A_i). Decidable (Eq A_i u v))…. Π(a b : I A…). Decidable (Eq (I A…) a b)`
- [fn derive_no_confusion](https://docs.logicaffeine.com/logicaffeine_kernel/recursor/fn.derive_no_confusion): `I_noConfusion : Π(A…). Π(P : Type 0). Π(a b : I A…). Eq (I A…) a b → I_noConfusionType A… P a b`
- [fn derive_no_confusion_type](https://docs.logicaffeine.com/logicaffeine_kernel/recursor/fn.derive_no_confusion_type): `I_noConfusionType : Π(A…). Π(P : Type 0). I A… → I A… → Type 0`
- [fn derive_quot_rec](https://docs.logicaffeine.com/logicaffeine_kernel/recursor/fn.derive_quot_rec): `Quot_rec` — the DEPENDENT quotient eliminator, built from the four quotient primitives rather than taken as a fifth one. The prelude registers exactly this body as `Quot_rec`.
- [fn derive_rec_on](https://docs.logicaffeine.com/logicaffeine_kernel/recursor/fn.derive_rec_on): `I_recOn` — the eliminator with the MAJOR PREMISE moved in front of the minors, which is the argument order `induction`/`match` elaboration wants and the one every Lean development writes by hand.
- [fn derive_recursor](https://docs.logicaffeine.com/logicaffeine_kernel/recursor/fn.derive_recursor): Build `I_rec`’s term and type for the inductive `ind`. Returns `(recursor_type, recursor_term)` where `recursor_type` is exactly `infer_type(recursor_term)` — so the type is, by construction, the one the kernel certifies the term against.
- [fn derive_recursor_universe_poly](https://docs.logicaffeine.com/logicaffeine_kernel/recursor/fn.derive_recursor_universe_poly): Build `I_rec.{u}` — the UNIVERSE-POLYMORPHIC eliminator, `Π(P : I → Sort u). … → Π(x). P x` with `u` an explicit level PARAMETER. Returns `(level_params, recursor_type, recursor_term)`.

## logicaffeine_kernel::reify
Shared reification substrate for the arithmetic decision procedures.

- [struct VarInterner](https://docs.logicaffeine.com/logicaffeine_kernel/reify/struct.VarInterner): Per-goal map from global names to variable indices.

## logicaffeine_kernel::ring
Ring Tactic: Polynomial Equality by Normalization

- [struct Monomial](https://docs.logicaffeine.com/logicaffeine_kernel/ring/struct.Monomial): A monomial is a product of variables with their powers.
- [struct Polynomial](https://docs.logicaffeine.com/logicaffeine_kernel/ring/struct.Polynomial): A polynomial is a sum of monomials with integer coefficients.
- [enum ReifyError](https://docs.logicaffeine.com/logicaffeine_kernel/ring/enum.ReifyError): Error during reification of a term to polynomial form.
- [fn reify](https://docs.logicaffeine.com/logicaffeine_kernel/ring/fn.reify): Reify a Syntax term into a polynomial representation.

## logicaffeine_kernel::simp
Simplifier Tactic

- [enum STerm](https://docs.logicaffeine.com/logicaffeine_kernel/simp/enum.STerm): Simplified representation of Syntax terms for rewriting.
- [fn check_goal](https://docs.logicaffeine.com/logicaffeine_kernel/simp/fn.check_goal): Check if a goal is provable by simplification.
- [type Substitution](https://docs.logicaffeine.com/logicaffeine_kernel/simp/type.Substitution): Substitution mapping variable indices to replacement terms.

## logicaffeine_kernel::tactic_cert
Independent verification of reflected ring, linear-arithmetic, and congruence goals.

- [struct CcCert](https://docs.logicaffeine.com/logicaffeine_kernel/tactic_cert/struct.CcCert): A checkable proof that a goal’s conclusion follows from its hypotheses by congruence.
- [struct LiaCert](https://docs.logicaffeine.com/logicaffeine_kernel/tactic_cert/struct.LiaCert): A refutation of a constraint system, as the multipliers that refute it.
- [enum CcStep](https://docs.logicaffeine.com/logicaffeine_kernel/tactic_cert/enum.CcStep): One step of an equality proof.
- [enum CertifiablePrimitive](https://docs.logicaffeine.com/logicaffeine_kernel/tactic_cert/enum.CertifiablePrimitive): A tactic reduction primitive a second kernel can now corroborate.
- [enum Syn](https://docs.logicaffeine.com/logicaffeine_kernel/tactic_cert/enum.Syn): The object language’s four shapes, as this module reads them.
- [fn check_cc](https://docs.logicaffeine.com/logicaffeine_kernel/tactic_cert/fn.check_cc): Check a congruence proof against a goal.
- [fn check_lia](https://docs.logicaffeine.com/logicaffeine_kernel/tactic_cert/fn.check_lia): Check a Farkas certificate against a `try_lia` goal.
- [fn emit_cc](https://docs.logicaffeine.com/logicaffeine_kernel/tactic_cert/fn.emit_cc): Search for a congruence proof of `goal` — UNTRUSTED.
- [fn emit_lia](https://docs.logicaffeine.com/logicaffeine_kernel/tactic_cert/fn.emit_lia): Emit a Farkas certificate for a `try_lia` goal, or `None` when the search finds none.
- [fn syn_apply](https://docs.logicaffeine.com/logicaffeine_kernel/tactic_cert/fn.syn_apply): `SApp f x`.
- [fn syn_binary](https://docs.logicaffeine.com/logicaffeine_kernel/tactic_cert/fn.syn_binary): `SApp (SApp (SName op) a) b`.
- [fn syn_of_term](https://docs.logicaffeine.com/logicaffeine_kernel/tactic_cert/fn.syn_of_term): Read a kernel `Term` as reflected object syntax, or `None` if it is not one.
- [fn syn_typed_eq](https://docs.logicaffeine.com/logicaffeine_kernel/tactic_cert/fn.syn_typed_eq): `SApp (SApp (SApp (SName "Eq") (SName ty)) a) b` — the typed equation `try_ring` reads.
- [fn term_of_syn](https://docs.logicaffeine.com/logicaffeine_kernel/tactic_cert/fn.term_of_syn): The same reflected syntax as a kernel `Term`, so a caller can hand the FIRST kernel exactly the goal it handed this module — which is what makes a differential between the two a differential and not two different questions.
- [fn verify_cc](https://docs.logicaffeine.com/logicaffeine_kernel/tactic_cert/fn.verify_cc): `try_cc goal` reduces to `DccSolve goal`, verified from a certificate this module both produced and then checked without reference to how it was produced.
- [fn verify_lia](https://docs.logicaffeine.com/logicaffeine_kernel/tactic_cert/fn.verify_lia): `try_lia goal` reduces to `DLiaSolve goal`, verified from a certificate this module both produced and then checked without reference to how it was produced.
- [fn verify_ring](https://docs.logicaffeine.com/logicaffeine_kernel/tactic_cert/fn.verify_ring): `try_ring goal` reduces to `DRingSolve goal`, verified here.

## logicaffeine_kernel::tactics
Tactics over the kernel’s own goals: a goal state of metavariables, outside the trusted base.

- [struct Goal](https://docs.logicaffeine.com/logicaffeine_kernel/tactics/struct.Goal): One open goal as a reader sees it: the hypotheses in scope, outermost first, and the target, every solved metavariable substituted.
- [struct GoalState](https://docs.logicaffeine.com/logicaffeine_kernel/tactics/struct.GoalState): A proof under construction: the statement, the metavariables standing for its unproved parts, and the goals still open.
- [struct ScriptError](https://docs.logicaffeine.com/logicaffeine_kernel/tactics/struct.ScriptError): A script’s failure: the step, by position and as written, and why; no step when the script ran to its end and the proof is not done.
- [enum TacticError](https://docs.logicaffeine.com/logicaffeine_kernel/tactics/enum.TacticError): Why a tactic did nothing, or why there is no proof yet.
- [enum TacticStep](https://docs.logicaffeine.com/logicaffeine_kernel/tactics/enum.TacticStep): One step of a tactic script (`by intro A x; exact (refl A x)`).
- [const SIMP_STEPS](https://docs.logicaffeine.com/logicaffeine_kernel/tactics/constant.SIMP_STEPS): How many rewrites one `simp` makes before it is refused as not terminating.

## logicaffeine_kernel::term_store
Hash-consed term storage — the representation a kernel needs to be as fast as Lean’s.

- [struct DefEqCache](https://docs.logicaffeine.com/logicaffeine_kernel/term_store/struct.DefEqCache): A cache of decided conversions, keyed on a PAIR of node identities.
- [struct EnvId](https://docs.logicaffeine.com/logicaffeine_kernel/term_store/struct.EnvId): Identity of a hash-consed LOCAL TYPING ENVIRONMENT — the fragment of a `Context` that decides a term’s type, and therefore half of the key an `inferType` cache must have.
- [struct IdCache](https://docs.logicaffeine.com/logicaffeine_kernel/term_store/struct.IdCache): A cache keyed on node identity, dense: `Vec<Option<V>>` indexed by the id, so a lookup is a bounds check and NOT a hash.
- [struct KernelCall](https://docs.logicaffeine.com/logicaffeine_kernel/term_store/struct.KernelCall): A token that lives exactly as long as ONE outermost kernel call, and that a cache BORROWS.
- [struct LevelId](https://docs.logicaffeine.com/logicaffeine_kernel/term_store/struct.LevelId): Identity of an interned universe level.
- [struct LitId](https://docs.logicaffeine.com/logicaffeine_kernel/term_store/struct.LitId): Identity of an interned literal.
- [struct NameSetId](https://docs.logicaffeine.com/logicaffeine_kernel/term_store/struct.NameSetId): Identity of a hash-consed, sorted set of names.
- [struct ScopedDefEqCache](https://docs.logicaffeine.com/logicaffeine_kernel/term_store/struct.ScopedDefEqCache): `DefEqCache` branded with the lifetime of ONE outermost kernel call. See `DefEqCache::scoped`.
- [struct ShapeMask](https://docs.logicaffeine.com/logicaffeine_kernel/term_store/struct.ShapeMask): The set of `NodeShape`s occurring anywhere in a subterm — one `u16`, computed once at interning time and answered in O(1) thereafter.
- [struct SubstId](https://docs.logicaffeine.com/logicaffeine_kernel/term_store/struct.SubstId): Identity of a hash-consed simultaneous substitution.
- [struct TermId](https://docs.logicaffeine.com/logicaffeine_kernel/term_store/struct.TermId): Identity of an interned term — a `Copy` handle whose equality IS structural equality.
- [struct TermStore](https://docs.logicaffeine.com/logicaffeine_kernel/term_store/struct.TermStore): A hash-consed term store: maximal structural sharing, O(1) equality, O(1) annotations.
- [struct TooLarge](https://docs.logicaffeine.com/logicaffeine_kernel/term_store/struct.TooLarge): A DAG whose unfolding is too large to materialise as a `Term`.
- [struct TypeCache](https://docs.logicaffeine.com/logicaffeine_kernel/term_store/struct.TypeCache): `inferType`, memoised on `(environment, term)` — the cache Lean has and we do not, with the half Lean does not need because its `Expr` is de Bruijn.
- [enum LevelView](https://docs.logicaffeine.com/logicaffeine_kernel/term_store/enum.LevelView): A borrowed view of one interned universe level.
- [enum Node](https://docs.logicaffeine.com/logicaffeine_kernel/term_store/enum.Node): One term node with its children replaced by handles — the flat shape that makes the store a DAG rather than a tree.
- [enum NodeShape](https://docs.logicaffeine.com/logicaffeine_kernel/term_store/enum.NodeShape): Which `Node` kind a subterm is — one per `Node` variant, and wildcard-free everywhere it is matched for the same reason `Node` is.
- [enum Occurrences](https://docs.logicaffeine.com/logicaffeine_kernel/term_store/enum.Occurrences): How often a name occurs — the only distinction an occurrence-gated ζ rule needs.
- [enum StoreNormalForm](https://docs.logicaffeine.com/logicaffeine_kernel/term_store/enum.StoreNormalForm): The result of `TermStore::beta_zeta_normalize` — honest about a budget it did not finish inside, the way `reduction::normalize_checked` is.
- [const BASE_STACK_BYTES](https://docs.logicaffeine.com/logicaffeine_kernel/term_store/constant.BASE_STACK_BYTES): The floor under any stack the kernel sizes for itself, whatever the term’s depth — room for the non-recursive part of a kernel call, and for a panic to unwind and format its message.
- [const BYTES_PER_RUNG](https://docs.logicaffeine.com/logicaffeine_kernel/term_store/constant.BYTES_PER_RUNG): Stack reserved per rung of nesting past `INLINE_DEPTH`.
- [const INLINE_DEPTH](https://docs.logicaffeine.com/logicaffeine_kernel/term_store/constant.INLINE_DEPTH): The deepest term the kernel will walk on a stack it did not size.
- [fn beta_zeta_normal_form](https://docs.logicaffeine.com/logicaffeine_kernel/term_store/fn.beta_zeta_normal_form): THE PURE β/ζ DOOR. The `Term`-level entry point a tree reducer wires in so a β-heavy reduction stops being quadratic — and the only one it needs, because it answers `None` for every term it is not certain about.
- [fn beta_zeta_normal_form_in_context](https://docs.logicaffeine.com/logicaffeine_kernel/term_store/fn.beta_zeta_normal_form_in_context): `beta_zeta_normal_form` with every policy question answered from the `Context` — the form a reducer wires in, with nothing left for the caller to get wrong.
- [fn deepen_stack](https://docs.logicaffeine.com/logicaffeine_kernel/term_store/fn.deepen_stack): Run `f` on a stack sized for `term` — or report that this call is already on one.
- [fn deepen_stack_all](https://docs.logicaffeine.com/logicaffeine_kernel/term_store/fn.deepen_stack_all): `deepen_stack` for an entry point that takes more than one term — `is_subtype` and `def_eq` compare two, and the stack has to hold the DEEPER of them.
- [fn deepen_stack_all_with_depth](https://docs.logicaffeine.com/logicaffeine_kernel/term_store/fn.deepen_stack_all_with_depth): `deepen_stack_all` told about depth the TERMS DO NOT SHOW — and it is not a refinement, it is a hole in the door that this is the only way to close.
- [fn deepen_stack_with_depth](https://docs.logicaffeine.com/logicaffeine_kernel/term_store/fn.deepen_stack_with_depth): `deepen_stack` told about depth the term does not show — see `deepen_stack_all_with_depth` for the defect this closes.
- [fn kernel_stack_bytes](https://docs.logicaffeine.com/logicaffeine_kernel/term_store/fn.kernel_stack_bytes): How much stack the kernel call on this thread is entitled to use.
- [fn kernel_stack_rungs](https://docs.logicaffeine.com/logicaffeine_kernel/term_store/fn.kernel_stack_rungs): The rungs (`BYTES_PER_RUNG` each) of the stack this thread runs on, by the kernel’s own sizing rule: at least `INLINE_DEPTH`, at most the kernel’s term-depth door.
- [fn literal_identity_eq](https://docs.logicaffeine.com/logicaffeine_kernel/term_store/fn.literal_identity_eq): THE ONE RULE. Total, reflexive literal equality — bit-exact on floats — offered as a FUNCTION so `term.rs` and this store cannot hold two different opinions about it.
- [fn occurrence_count_in_term](https://docs.logicaffeine.com/logicaffeine_kernel/term_store/fn.occurrence_count_in_term): How many FREE occurrences of `name` a `Term` has, saturating at `u32::MAX`.
- [fn occurrences_in_term](https://docs.logicaffeine.com/logicaffeine_kernel/term_store/fn.occurrences_in_term): `occurrence_count_in_term`, classified — everything an occurrence-gated ζ rule needs, and strictly CHEAPER than the count, because it stops at the second occurrence.
- [fn occurs_free_in_term](https://docs.logicaffeine.com/logicaffeine_kernel/term_store/fn.occurs_free_in_term): Whether `name` occurs free in `body` at all — stops at the first occurrence.
- [fn stack_bytes_for_depth](https://docs.logicaffeine.com/logicaffeine_kernel/term_store/fn.stack_bytes_for_depth): How many bytes of stack a term of this depth is given.
- [fn term_depth](https://docs.logicaffeine.com/logicaffeine_kernel/term_store/fn.term_depth): The nesting depth of a `Term`, counted in EDGES: a leaf is 0.
- [fn within_kernel_depth](https://docs.logicaffeine.com/logicaffeine_kernel/term_store/fn.within_kernel_depth): Whether syntax is within the kernel’s existing term-depth limit.
- [fn zeta_expand_head_term](https://docs.logicaffeine.com/logicaffeine_kernel/term_store/fn.zeta_expand_head_term): ζ-expand a `Let` at the head, whatever its occurrence count — the step a conversion check must be able to take on demand once `zeta_or_share` lets a `Let` survive into a normal form. `None` for anything that is not `Let`-headed.
- [fn zeta_or_share](https://docs.logicaffeine.com/logicaffeine_kernel/term_store/fn.zeta_or_share): ONE ζ step, OCCURRENCE-GATED, against a reducer that always returns a `Term`.
- [fn zeta_or_share_in_place](https://docs.logicaffeine.com/logicaffeine_kernel/term_store/fn.zeta_or_share_in_place): `zeta_or_share_opt` on a `Let` the caller owns, stepping its parts where they lie: the same rule, in the same order, with the same answer, but a part that a step leaves alone is never copied and nothing is rebuilt around the one that moved. `step_in_place` must be the in-place twin of `step` (`reduce_step_in_place` of `reduce_step_opt`), which `reduction::owned_normalize_controls` pins shape by shape. `false` for anything not `Let`.
- [fn zeta_or_share_opt](https://docs.logicaffeine.com/logicaffeine_kernel/term_store/fn.zeta_or_share_opt): `zeta_or_share` against a reducer that reports PROGRESS: `step` answers `None` when there is no redex. `reduction.rs`’s `reduce_step_opt` calls it for every `Term::Let`.

## logicaffeine_kernel::termination
Termination checking for fixpoints.

- [fn check_termination](https://docs.logicaffeine.com/logicaffeine_kernel/termination/fn.check_termination): Check that a Fix term satisfies the syntactic guard condition.
- [fn check_termination_mutual](https://docs.logicaffeine.com/logicaffeine_kernel/termination/fn.check_termination_mutual): Check that a MUTUAL block of fixpoints terminates — the mutual Giménez guard.
- [fn structural_columns](https://docs.logicaffeine.com/logicaffeine_kernel/termination/fn.structural_columns): THE ι-SPECIFICATION — which argument makes a `Fix` unroll.
- [fn structural_position](https://docs.logicaffeine.com/logicaffeine_kernel/termination/fn.structural_position): The single argument POSITION a reducer needs: the Giménez structural column, or `None` when the guard admits no column at all and therefore no ι rule applies to this fixpoint.

## logicaffeine_kernel::word_ring
Kernel ring proofs for the word ring ℤ/2ⁿ (`Word8`/`Word16`/`Word32`/`Word64`).

- [fn add_associative](https://docs.logicaffeine.com/logicaffeine_kernel/word_ring/fn.add_associative): `(a + b) + c = a + (b + c)` — additive associativity in ℤ/2ⁿ.
- [fn add_commutative](https://docs.logicaffeine.com/logicaffeine_kernel/word_ring/fn.add_commutative): `a + b = b + a` — additive commutativity in ℤ/2ⁿ.
- [fn additive_identity](https://docs.logicaffeine.com/logicaffeine_kernel/word_ring/fn.additive_identity): `a + 0 = a` — additive identity in ℤ/2ⁿ.
- [fn all_word_ring_laws_certified](https://docs.logicaffeine.com/logicaffeine_kernel/word_ring/fn.all_word_ring_laws_certified): Every word-ring law the optimizer leans on, kernel-certified — a single gate.
- [fn karatsuba_expand](https://docs.logicaffeine.com/logicaffeine_kernel/word_ring/fn.karatsuba_expand): `(a + b)(c + d) = ac + ad + bc + bd` — the Karatsuba/gauss product expansion, the identity the 3-multiply NTT butterfly and complex-multiply reshaping rely on, certified at full word width.
- [fn left_distributive](https://docs.logicaffeine.com/logicaffeine_kernel/word_ring/fn.left_distributive): `a · (b + c) = a · b + a · c` — left distributivity in ℤ/2ⁿ.
- [fn mul_associative](https://docs.logicaffeine.com/logicaffeine_kernel/word_ring/fn.mul_associative): `(a · b) · c = a · (b · c)` — multiplicative associativity in ℤ/2ⁿ.
- [fn mul_commutative](https://docs.logicaffeine.com/logicaffeine_kernel/word_ring/fn.mul_commutative): `a · b = b · a` — multiplicative commutativity in ℤ/2ⁿ.
- [fn multiplicative_identity](https://docs.logicaffeine.com/logicaffeine_kernel/word_ring/fn.multiplicative_identity): `a · 1 = a` — multiplicative identity in ℤ/2ⁿ.