Add self-contained kernel verification and relative consistency for environment checking

[johnchandlerburnham]

This PR establishes model-backed relative consistency for Ix's certified
acceptance path and makes its verification dependencies local to Ix. Successful
certified source and store checks produce models of the admitted declarations;
logical claim receipts preserve the original statements and declared frontier,
with no-False theorems for closed logical acceptance. These are proved
acceptance-to-model results for the supported certified profile.

The mathematical foundation has a concrete construction on Mathlib's ZFSet,
under a countable increasing sequence of strongly inaccessible cardinals.
This supplies the set-theory interface used by the consistency proofs.
The foundational hypothesis, and a model of any arbitrary source axioms in the
direct production theorem, are explicit premises of relative consistency.

The PR also connects the ordinary Lean production checker in Ix.Kernel to
this semantics for a supported checkEnvAnon fragment: every model of the
source axioms extends to a model of the checked environment, preserving the
original axiom interpretations. This direct implementation theorem covers
aliases, universe terms, instances of polymorphic constants, and closed
dependent function bodies, including definitions with their own universe parameters, under explicit
execution and representation witnesses. The remaining implementation work is full
production-checker refinement: extending that connection to the other inference,
conversion, cache, and declaration-admission paths. The Rust checker in
crates/kernel and the Aiur IxVM checker in Ix/IxVM/Kernel need their own
correctness connections; this PR does not establish those transfers.

Full-mode lets now compose inside the original recursive synthesis datatype
and enter the direct declaration theorem through their
original declared-type, value, and opened-body synthesis checks. The proof
follows actual fresh-local opening, type abstraction, value substitution,
selected cheap beta, scope cleanup, and cache publication. Substitution retains
the original checking derivations for later beta reductions. The scoped reader
and its walker proofs include nested lets. The three children and surrounding
binders, applications, and cache hits can contain further lets. Complete
derivations retain both function-type children when substitution exposes their
constructor. Typed cache histories now retain let roots and their descendants;
later full-cache selection reconstructs the same checks and beta origins.
Automatic execution/resource construction and the seven full-refinement
obligations below remain unfinished.

Recursive forall, lambda, and let checks now also expose sorts through the
supported public beta WHNF path or its recorded outer-cache hit. Successful
production inference supplies all raw child-call observations, including the
sort-exposure states. SynthesisSortCheck retains inference at the actual
returned type and derives its conversion from earlier checked type origins.
The exposed level forms the next binder context; the original source derivation
continues through substitution and later beta steps. Both inference-cache maps
retain the original child publication, even when its type reduces to a sort.
General construction of the finite reading, collision, reduction, and checking
resources remains open, as do other reduction and cache paths.

Returned syntax readings are now derived before the synthesis semantic
induction, without a context-formation premise. The source derivation producer
uses those readings to identify compared types and retains the original
checking origins. The semantic induction separately derives an invariant
closed under dependent substitution, then recovers the existing typing,
formation, and lambda-spine results. Source support and reconstruction do not
assume this invariant; explicit dependency guards enforce that boundary.

Structural local-state preservation now follows the entire production recursive
method table on both success and failure. The actual loader and lazy initial
state establish coherent local lookup and the allocation-counter bound. Every
inference, reduction, conversion, and projection branch preserves that
invariant; scope cleanup restores all incoming declarations and lookups.
The model reader transports through observable restoration. The let proof now
derives its intermediate context frames, fresh identifier, and final scope
restoration from its actual child runs and one initial invariant. It no longer
assumes exact local-context equality or a separate freshness fact. General
semantic typing, reduction, cache validity, and declaration admission remain
unfinished.

Forall, lambda, and application traces now also retain the initial structural
local invariant and derive their context frames from the actual recursive
calls. Binder and synthesis nodes derive freshness instead of storing it.
The application exposure frame follows the real reduction call without a
beta-path premise. Retained codomain and lambda-body checking origins,
subsequent beta typing, and whole-cache histories consume the derived reader
transport. The sort-aware binder traces now extract their raw observations
from successful calls; complete checking-resource construction remains unfinished.

The ordinary Lean and Rust checkers now reject circular safe definitions.
Before the fix, a content-addressed source with only P : Prop as an axiom
accepted theorem loop : P := loop, including as a one-member mutual block.
Safe declaration validation now traverses definition references in both types
and values, including binders, lets, shared syntax, and projection heads. It
rejects cycles and exhaustion of a shared one-million-step bound. Acyclic mutual
blocks and the separate partial/unsafe safety policies remain supported.
The Lean proof derives a dependency certificate from the actual traversal,
proves a strictly decreasing rank on its edges, and proves that address
memoization omits no syntax reference under finite-run collision freedom.
Successful safe validation exposes the order to the model-reference proof.
This closes an actual admission defect; it does not by itself supply general
body typing or model construction for every block member.
The rejection includes axiom-free definitions of ∀ P : Prop, P whose body
is a relative self-reference. Termination-checked source recursion remains
supported: Lean elaborates it into recursor applications, with recursive calls
supplied as local arguments. Positive structural, well-founded, and mutual
fixtures now require both host kernels to accept their complete exported
dependency closures, including every requested declaration.

The direct inference proofs also cover polymorphic constant references with
arbitrary readable declaration types. They connect the actual universe
instantiation walker, lazy lookup, and runtime arity check to model typing,
under explicit lookup and finite-support resources. Scope and reference
preservation for the actual substituted type compose this result into
declaration admission and environment model extension at the definition's
declared universe arity. Parameters may be forwarded, reordered, or combined
when instantiating an earlier declaration. The remaining general inference,
conversion, cache, loader, and block-admission paths still need further proofs.

The binder fragment covers real identity bodies such as
def idProp (P : Prop) (p : P) : P := p, calls to earlier definitions and
polymorphic constants, and applications of local functions. It connects production locals,
fresh-variable opening, abstraction, dependent function universes, argument
checking, codomain substitution, and finite recursive inference trees to the
model. The declared type's separate inference
establishes hereditary validity before the value's checking result becomes
typing. DefinitionBodyTrace.binderSupport takes these inference calls from
the same production execution and derives source scope from its actual
validation. Finite validation coverage and collision freedom are retained;
only the auxiliary binder-condition bounds require a separate syntax check.
SynthesisInference.closed_sound additionally derives a uniform universe bound
for the generated type, covering direct lambda applications, returned functions,
and dependent lambda bodies. Bounds come from actual domain checks and earlier
declaration type checks. The key set-model lemma proves that an inhabited
dependent product in a Grothendieck universe bounds each fibre: an existing
function supplies the other values while one fibre element is varied. This
avoids the invalid inversion of an empty product. The resulting application
bound preserves the exact Prop condition and may enlarge a positive universe;
it does not postulate another inference call on a generated codomain.
DefinitionBodyTrace.synthesisSupport connects these rules to model admission.
Earlier type checks retain their raw source, states, successful execution, and
finite inference tree, and remain usable after interface growth and universe
instantiation. Successful environment rows supply the axiom type-check traces;
public declaration success supplies the definition traces. Their inference
trees may themselves contain direct lambda applications.
Source beta redexes now derive equality and result typing from those actual
inference trees. Lambda-shape inversion retains the checked domain, which
denotational typing alone cannot recover after proof values are identified.
The multi-argument structural-WHNF step is connected to model substitution
through its actual lambda peel, simultaneous walker, and interned application
suffix, preserving intern coherence under finite construction, size, and
collision resources. Bounds concern the original body and argument trees.
The model judgments also have proved substitution rules for typing, checking,
and equality. Selected cheap-beta plans have the same typed meaning when an
actual source check is available.
DefinitionCheckSupport.betaDeclaredSpine reuses the declaration's executed
type check to justify conversion through a lambda prefix and a remaining
argument suffix. This case reaches the existing environment model-extension
and no-False roots. The previous hash interface remains available through
AtomicDefinitionRun.ofHash. Recursive lambda inference now handles changed
cheap beta when its generated body type retains an actual checking origin.
The same inference recursion preserves checked lambda domains. Pure syntax
transport carries the original type and beta result together through interface
growth, local weakening, universe instantiation, and level congruence. Earlier
local contexts come from actual domain checks, so origins can precede several
binders. The reader derives the actual spine and selected reduction from the
body type returned by inference; abstraction uses the reduced type and final
intern table. Retained codomain checks now cross dependent term substitution
inside that same inference recursion. The earlier function-type tree supplies
the actual codomain check; the executed function and argument calls and their
hash comparison supply the argument's membership in the expected domain.
ContextSubstitution updates every remaining dependent parameter at the same
cutoff, and the proved syntax laws carry both the original lambda prefix and
its result. The model's typing, checking, and conversion judgments are all
preserved. Variable-headed codomains now retain their exact local head type
and the actual checks of their arguments. Nested function-type calls supply
these origins with their executed domain checks. Earlier arguments update
the retained head's dependent type; substituting a lambda for the head uses
that argument's own checked prefix to justify the new beta steps. Later
arguments continue transporting the resulting reduction. A supplied lambda
application also contributes its already checked arguments. Their dependent
types are lifted beneath retained parameters, then joined to the original
codomain's substituted argument checks in order. The selected beta prefix can
consume arguments from both origins. The mutual origin
proof supplies conversion and reduced-type formation to lamBeta. No new
inference call on a generated type or semantic argument premise is required.
The body of a lambda that applies its parameter now retains its actual
argument checks even when cheap beta changes that body's inferred type.
The first beta result supplies typing at the current type, and the supplied
lambda's original check supplies the next reduction prefix. These origins
compose two successive prefixes, connect to the actual intermediate WHNF
step, and justify declaration admission through both reductions. Finite
SynthesisBetaTrace values now compose any number of retained prefixes.
Earlier results can supply later function or argument origins; application
suffixes, dependent substitutions, and changes in the retained type preserve
the original source typing. Source inference extracts the head and every
argument check. SynthesisBetaWhnfTrace computes each raw result and intern
table through production substitution and suffix interning, then proves the
actual uncached WHNF loop with its terminal iteration and fuel bound. These
traces also justify declaration admission. The original inference now
constructs a complete beta typing derivation retaining each lambda body and
both application children. Substitution rebuilds it under dependent binders,
so generated results automatically supply every later lambda and argument
origin. Forward beta conversion retains the exact Pi domains when cheap beta
changes a body's inferred type. Thus every finite head-beta path of the
currently supported inference fragment derives its semantic origins from the
original check. A raw operational path supplies only execution, reading, and
finite representation resources; its computed semantic annotation also
justifies declaration admission. Initial inference and operational resource
construction for arbitrary accepted programs, other WHNF branches, and general
conversion remain open.
Public WHNF now connects those beta paths to its instrumentation, shared-fuel
charge, exact context keys, and three physical cache insertions when the result
is a sort, Pi, or lambda. Application inference can expose a Pi through that
public call or reuse the exact result of an earlier supported path from the
outer cache. The retained check of the function type supplies the conversion;
the argument check starts in the actual post-exposure state. Conversions can
occur between successive dependent arguments, and all later substitutions and
beta derivations retain those checks. This application case reaches the
existing synthesis, declaration, and environment model-extension theorems.
Cold paths currently require misses in all three WHNF caches and an inactive
native-reduction guard. Warm outer-cache hits retain their originating path
and need no fuel. General cache agreement, intermediate cache hits, and the
other exposure and conversion branches remain open.
Local-variable cache hits must match the current declaration's concrete
type. Constant hits must equal pure universe substitution of a loaded,
admitted declaration. Sort hits use the canonical successor sort. Cache
agreement is preserved by sort and already-loaded constant inference, and
structural frames carry closed constant witnesses through scope changes and
unrelated writes. A finite recursive trace computes the keys written by an
entire application or binder inference and preserves entries outside those
writes, together with loaded declarations and checking policy.
Frames allow declaration growth. Verified standalone and mutual-block lazy
loading preserve old declarations and inference caches on success and failure,
and the recursive trace composes loads inside application and binder inference.
Block publication requires each prepared entry to agree with any old declaration
at its key; this admits fresh entries and exact repeats in partially loaded
blocks. Preparation's mutable state is restricted to intern tables and conversion
caches; public ingress interfaces and partial-state error behavior are retained.
Intern-table key coherence is derived through all production conversion forms
and lazy loading on both outcomes. Conversion uses finite bounds computed from
source syntax, with worklists for counting and execution; cyclic sharing returns
an error with coherent partial progress. Constant inference carries initial
coherence through lookup, universe substitution, and cache publication.
A finite source-header check now establishes disjoint projection ownership.
Conversion emits only the enumerated keys, and atomic publication records their
owning block. The invariant that loaded projections have recorded blocks starts
empty and survives actual lookup on both outcomes and successful constant calls.
Unrecorded blocks consequently have fresh entries, removing per-block overlap
comparisons for this path. The general compatibility resource remains available
for externally partially populated states.
Source-only conversion now predicts complete standalone declarations and the
finite expression/universe candidates used to construct them. Under explicit
finite collision data, actual conversion follows this prediction on both
outcomes. Loaded-standalone agreement starts empty and survives verified
lookup and supported recursive inference, including intervening block loads.
A static source/model binding reads the predicted type once; actual constant
lookup then derives its type reading, arity, and intern coherence. These bindings
still select already admitted model entries, and the standalone catalog does
not interpret mutual members or establish general declaration admission.
Finite catalogs of closed sorts and standalone constant instances now establish
both inference partitions' agreement from empty caches. The invariant also
retains the loaded declaration behind every cached constant. Recursive calls
preserve catalog entries at their written keys, and histories include policy
changes, binder scopes, block loads, lookup failures, and clearing. Actual
selection derives the existing constant and sort hit/miss interfaces; constant
typing follows from the source binding and history without fresh cache witnesses.
Composite synthesis cache hits now retain an earlier successful inference
tree and its raw execution. Lambda domains, dependent codomain checks, and
body checks remain available to every later beta origin. A successful full
call establishes the exact stored type, and cache frames derive subsequent
selection under either policy without recursion fuel. The frames include
beta Pi exposure and changed cheap-beta lambda bodies. The original checks now
survive interface growth and insertion of locals, including captured variables
beneath dependent binders. Pi checks retain both domain and codomain checks;
lambda bodies and variable-headed codomains retain their argument checks.
A successful full call constructs a concrete cache resource, whose proved
frames and syntax transport supply the new hit in the original synthesis
recursion. Successive and hereditary beta, declaration admission, and environment
model extension include these transported checks. Every initially populated
full key now survives supported recursive inference by cache priority, without
a write-exclusion premise. An exact event fold reconstructs both complete maps
from actual child and parent calls. Histories begin empty and retain the producing
call at every present key through inference, policy changes, scopes, verified
loading on both outcomes, and clearing. The original rich synthesis tree supplies
all full-publication checks; older checking-only wrappers need supplementary
annotations for omitted child calls. Finite query/history collision data recovers
the source and materializes its retained synthesis check. The check keeps its
original context and supports later interface transport. Arbitrary execution
construction, compatibility with later contexts after scope exit, and other
inference and conversion/cache paths remain open. Cold composite nodes
retain eligible misses; full mode leaves the inference-only partition unconstrained.
The raw event history additionally covers full-mode lets, with the domain,
value, and opened-body calls preceding the parent publication. Their original
let check and child cache data derive both exact maps and the history. Typed
history retains the same recursive let root and all its children. Sort-exposure
nodes preserve this fold and retain the child's original inferred type.

Main changes

Local verification dependencies and checker naming

• Moves the production Lean checker and its implementation proofs from Ix.Tc
  to Ix.Kernel, updating imports, namespaces, callers, tests, build targets,
  and CI commands.
• Retains the required name-indexed specification and reference implementation
  lemmas under Ix.Theory.Named, with 104 source modules and an exact inventory
  of their original source hashes and attribution.
• Retargets the existing Ix.Compile.Verify proofs to the local specification.
  This preserves the existing compiler proof boundary; it does not add the
  separate compiler or wire-format development.
• Removes the external lean4lean Lake dependency and its benchmark/test
  targets. Building the maintained proof libraries no longer requires an
  external formalization checkout.
• Shares Ix.Theory.VLevel between the named specification and the consistency
  model. Their expression calculi remain separate: the named checker proofs use
  their existing syntax, while the set model uses explicit store references and
  annotated semantic expressions.

Most changes to the existing checker tree are relocation, namespace updates,
and proof/documentation maintenance. The production fixes also reject circular
safe definitions in both the Lean and Rust kernels, with source-level verdict
parity and regression coverage.

Set-theoretic foundation and certified acceptance

Ix.Theory contains the selected consistency foundation, certified acceptance
interface, and required certificate construction modules. The import preserves
120 selected source modules plus the certified umbrella, with source manifests,
licenses, and per-file attribution. Its mathematical import boundary excludes
the named checker development, production checker/compiler code, and test
harnesses.

The main foundation results are:

• Ix.Theory.Certified.accepted_has_model: accepted declarations have a model
  under the stated set-theory and frontier hypotheses.
• accepted_proof_sound: accepted proofs satisfy the corresponding semantic
  interpretation.
• no_proof_of_False: the certified interface cannot admit a proof of its false
  proposition under those hypotheses.

The required Ix.Theory.Model.SetTheory V structure remains an explicit
assumption. A separate Lake package, Models/SetTheory, constructs it on
Mathlib's ZFSet from a strictly increasing countable sequence of strongly
inaccessible cardinals. Its public implication is:

OmegaInaccessibles.{u} →
  Nonempty (Σ V : Type (u + 1), Ix.Theory.Model.SetTheory V)

The construction includes the required replacement scheme and passes an axiom
guard allowing only propext, Classical.choice, and Quot.sound. The
large-cardinal hypothesis is not discharged or hidden as a new Lean axiom.
Mathlib is confined to this package; ordinary Ix builds do not acquire a
Mathlib dependency.

Direct refinement of production checking

Ix.Kernel.Verify.Consistency connects production operations directly to
Ix.Theory, with a separate strict build and exact dependency audit.

The supporting results establish:

• Agreement of production universe equality and ordering with model evaluation,
  subject to the existing finite address-faithfulness and arithmetic bounds.
• A structural reading of kernel expressions into model syntax. It resolves
  addresses through an explicit interface, preserves projections and natural
  literals, and substitutes let values. The closed reader excludes free
  variables, unresolved addresses, and strings. A separate scoped reader
  handles registered locals, syntactic binders, and let substitution, excluding
  loose legacy variables, unknown locals, and strings. Its opening, abstraction,
  substitution, scope, and reference proofs include nested lets.
• Preservation of this reading through hash equality and interning under the
  stated collision/coherence assumptions. Metadata does not change the reading.
• inferUncached_sort_sound, which derives model typing from a successful
  execution of the actual production sort-inference branch, including the
  intern-table reuse case. infer_sort_cached_sound supplies the same typing
  when the selected cached result is the canonical successor sort.
• instantiateUnivParams_readAnnotated, which connects the memoized and
  interned production walker to model universe substitution for every readable
  expression form. The returned syntax may simplify max or imax; an exact
  structural congruence preserves every reference, index, and binder annotation
  while proving preservation of interpretation and hereditary validity.
  Let substitution commutes with the universe operation. Universe scope
  justifies the production empty-argument fast path, which skips range checks.
• instantiateUnivParams_readAnnotated_scoped, which also derives scope and
  reference preservation for the actual returned type. The successful walker
  and scoped arguments establish these syntactic facts; semantic level
  equivalence alone does not imply scope.
• inferUncached_const_sound and infer_const_sound, which prove model typing
  for polymorphic references with arbitrary readable declaration types.
  Runtime success establishes arity. The remaining premises are model-interface
  well-formedness, agreement with the actual lazy-loaded type and universe
  count, finite expression/level support and arithmetic bounds, and inference
  misses in eligible inference-cache partitions for the ordinary entry point.
  Full mode permits a populated, ignored inference-only partition.
  The shared support definitions
  are also used by the existing named-translation proof.
• CachedConstantInferenceSupport.sound, which derives typing for monomorphic
  and polymorphic constant cache hits inside binder trees. The cached value
  equals pure substitution of a loaded declaration whose type reads as the
  admitted entry, with explicit universe arity and finite level resources.
  InferenceCacheHit.run proves full-cache priority and inference-only policy
  eligibility, including the exact returned state. infer_const_cache_write
  proves that a successful miss inserts its pure substituted type in the
  correct partition.
• SynthesisInference.closed_sound, which derives both full term typing and
  formation of the returned type. It follows the actual lambda-domain check
  and bounds the body's generated type, so lambdas can occur directly in
  function position. Application recovers a fibre bound from its inhabited
  product. The Prop bound stays zero, while positive upper bounds need not
  equal an independently inferred sort. TypeFormation and SynthesisTypeCheck
  retain executed type checks through interface extension, local weakening,
  and universe instantiation. AxiomObservation.synthesisTypeCheck and
  StandalonePrefix.definitionTypeCheck recover those executions from the
  actual public checker, and DefinitionBodyTrace.synthesisSupport composes
  full synthesis with source scope and dependency references for admission.
• SynthesisInference.reuseFull, which derives a composite cache node from
  the earlier actual check, its successful full call, and a preserved entry.
  The stored result's reading follows from the original tree, whose lambda
  domains, dependent codomain checks, and beta derivations remain available.
  reuseFullClosed computes the key for a source without loose variables;
  reuseFullAcross derives the frame from intervening recursive inference.
  CachedSynthesisCheck additionally retains those checks through interface
  growth and fresh-local insertion, deriving reading transport and selection
  from actual full calls and operational frames. Its support constructs
  SynthesisInference.cachedFrom in the original recursion. The full entry
  has priority under both later checking policies and needs no fuel.
• InferenceCacheAgreement, which records concrete agreement in both
  partitions at one key, independent of checking policy. Actual sort inference
  and already-loaded constant inference preserve agreement at their own key
  and leave other entries and loaded declarations unchanged. Their miss proofs
  follow the real interning or universe-substitution operation and cache write.
  PreservesInferenceCache composes frames through interning, key computation,
  binder opening, unrelated writes, and scope/policy cleanup on success or
  failure. Clearing reduction caches establishes empty-cache agreement.
  CachedConstantInferenceSupport.transport carries a closed witness across
  those frames, and BinderInference.sortOfAgreement constructs sort leaves.
  Initial agreement and finite execution resources remain premises. Frames allow
  new declarations while retaining each previously loaded declaration.
• InferenceCacheTrace.frame, which derives cache preservation through finite
  application, forall, and full-mode lambda trees. Its computed write footprint
  includes each recursive miss and final outer insertion; hits contribute no
  writes. A key outside that footprint retains both cache entries, loaded
  declarations, and the checking policy through the whole successful call.
  The proof includes lambda domain validation, scope cleanup, and the optional
  statistics update on hash conversion. The existing application and binder
  output lemmas now also identify their exact final states.
  CachedConstantInferenceSupport.afterInference transports an earlier closed
  constant witness, with later typing given by sound_after_inference.
  BinderInference.sortAfterInference constructs a later sort leaf from
  preserved agreement. These operations derive the later cache observation.
  Callers still supply the finite operational trace, lookup and walker
  resources. populated_outside derives the exclusion for every initially
  populated full key from production cache priority; populated_frame then
  preserves both slots at that key. Full synthesis reuse consumes this stronger
  interface without a write-exclusion premise.
• InferenceCacheTrace.cache_maps, which reconstructs both complete inference
  maps by folding the actual successful miss events in publication order.
  InferenceCacheHistory begins empty and derives an actual producing call at
  every selected value, including new keys, through supported inference, scopes,
  policy changes, verified loading on both outcomes, and clearing. This operational
  statement needs no collision premise or fixed catalog.
  SynthesisInference.cacheExecution extracts full-publication annotations from
  the original rich synthesis tree and derives child readings and contexts from
  its actual domain calls. Older checking-only wrappers supply operational
  resources and annotations for omitted children; primitive leaves need no
  additional checking tree. SynthesisCacheHistory retains these origins through
  interface growth. Finite query/history collision data recovers the same source
  at selection, constructing its complete CachedSynthesisCheck without fresh
  cached-typing, result-reading, or earlier-run premises. Selected checks retain
  their original local contexts; arbitrary scope-exit transport remains open.
• SynthesisInference.letE, which derives returned-type reading, term typing,
  and type formation from a full production let check. Its three original
  synthesis children check the declaration, value, and opened body. The actual
  hash comparison identifies the value's inferred type with the declaration;
  fresh opening, abstraction, value substitution, and selected cheap beta
  determine the returned type. Substituting the original checking derivations
  retains every later beta origin, including a lambda exposed by the value.
  The same recursive datatype permits lets inside each child and every other
  supported synthesis constructor. LetInferenceCheck.asSynthesis connects
  the original let interface to this case; DefinitionBodyTrace.letSupport
  uses the same declaration's validation calls for model extension.
  LetInferenceCheck.cache_maps and
  cacheHistory derive both maps and the raw history from those same checks
  and their child cache data. SynthesisInference.cacheExecution and
  LetInferenceCheck.synthesisCacheHistory also retain the root and its
  descendants in the typed history, with complete checks for later selection.
  General automatic execution and representation resources remain open.
• SortInferenceTrace and the forall/lambda/let ofInference constructors,
  which extract actual child inference, sort exposure, opening, comparison,
  and body observations from successful production branches.
  SynthesisInference.forallSort, lamSort, and letSort consume the original
  recursive child checks. SynthesisSortCheck.ofRetainedType obtains conversion
  from an earlier check of the returned type, with no semantic typing premise.
  Binder contexts use the exposed level; complete beta derivations and typed
  cache histories preserve the source check. Direct sorts, supported cold beta
  WHNF, and outer-cache replay share this interface. Exposure preserves both
  inference-cache maps, including the original unreduced child type. Other
  reducers and general construction of finite resources remain open.
• MethodsLocalState.methodsN, which closes structural local-state preservation
  through all six recursive method-table fields. Public inference, WHNF,
  conversion, and sort/forall exposure entries retain coherent lookup,
  monotone allocation, and the installed loader on both outcomes. The proof
  follows actual production branches, including speculative rollback and
  scope cleanup. IngressM.FramesState.ingressAnonAddrShallow proves the loader
  effect from the intern-only conversion boundary and declaration publication;
  LocalStateInvariant.newLazyAnon establishes the initial invariant without a
  callback premise. LocalContextReading.congr and freshReading connect these
  structural facts to model locals. LetInferenceTrace retains only actual
  runs; its context frames and restoration are derived. LetInferenceCheck
  uses those frames to derive freshness for the same body and cache proofs.
• getConst_standalone_cache, which proves a declaration-extension frame for
  the actual verified standalone loader on both outcomes. Conversion can update
  only intern tables and conversion caches; an initial lookup miss makes the
  single-entry registration fresh. Missing sources, integrity/parse errors,
  conversion errors with partial progress, reserved markers, and deduplicated
  faults retain both inference maps and the old declarations.
• getConst_verified_cache, which extends preservation to mutual-block loading.
  Block preparation, including inductives, constructors, and recursor rules,
  changes only intern tables. The actual publication fold preserves each old
  declaration when all prepared entries agree with any old declaration at their
  key. Fresh entries and exact repeats satisfy this condition; duplicate fresh
  keys need no uniqueness premise. Parent failures, block deduplication,
  partial preparation failures, and errors after completed publication all
  retain the earlier cache witness.
  InferenceCacheTrace.lazyConst composes loading with substitution at the
  returned state, and CachedConstantInferenceSupport.afterVerifiedInference
  reuses an earlier witness after inference may load another dependency.
  Successful and failed lookups also transport the old witness. This general
  interface retains explicit overlap checks for arbitrary starting states.
• getConst_coherent, which derives intern-table key coherence through the
  actual loader without collision or declaration-overlap premises. The bounded
  universe and expression machines preserve coherence frame by frame, including
  errors, recursor rules, inductives, constructors, and block publication.
  UniverseInstantiationSupport.afterVerifiedGetConst obtains the post-lookup
  coherence field from the pre-load invariant. InferenceCacheTrace.coherentConstOfKey
  builds a leaf without a post-lookup coherence premise, and
  infer_coherentConst_cache_frame returns coherence after the full constant
  call alongside cache preservation. CachedConstantInferenceSupport.afterCoherentInference
  carries the earlier witness through that call. Finite collision and level
  resources and source interpretation remain explicit.
• getConst_owned, which derives block compatibility from a reusable invariant:
  every loaded source projection has a recorded owning block. The invariant
  starts empty, actual conversion emits only the finite source projection
  inventory, and atomic publication records the correct owner. An unrecorded
  block's prepared keys are therefore fresh. All lookup outcomes preserve the
  invariant, including errors after publication and conversion failures.
  sourceOwnershipCheck verifies separation using only verified source headers
  and deterministic member/constructor addresses. SourceOwnership.ofCheck
  proves its result; different block owners and standalone/projection conflicts
  reject, while duplicate keys within one block are permitted. Corrupt headers
  are excluded because the actual verified loader rejects them. This optional
  preflight changes no loader acceptance behavior and establishes no expression
  interpretation or declaration admission claim.
  OwnedLazySupport.ofCheckedSource initializes the reusable loader resource;
  afterGetConst and afterFailedGetConst carry it across lookups.
  afterConstInference retains it through successful key computation,
  substitution, and cache publication. InferenceCacheTrace.ownedConstOfKey
  and CachedConstantInferenceSupport.afterOwnedInference use it without a
  per-block overlap premise. Finite substitution resources, general source
  agreement, and preservation through other checker paths remain explicit.
• OwnedInferenceTrace.preserves, which carries ownership and intern coherence
  through successful recursive application, forall, and full-mode lambda calls.
  InferenceStateInvariant.ofCheckedSource initializes the combined resource
  from one source check. Tree nodes supply only operational traces and finite
  walker data: collision freedom, constructed expression annotations, size
  bounds, and universe-substitution data as needed. The proof derives initial
  coherence for application substitution, binder opening, and lambda abstraction
  from their preceding child calls. Constant leaves derive block compatibility
  and post-lookup coherence from the root invariant. toCacheTrace reconstructs
  the earlier cache-frame tree with exactly the same write footprint.
  CachedConstantInferenceSupport.afterOwnedRecursiveInference transports a
  previous witness; BinderInference.sortAfterOwnedInference supplies a later
  sort leaf without a post-inference coherence premise. The returned invariant
  supports another constant call, including a new lazy block load. No semantic
  source agreement, arbitrary trace construction, or global checker-state
  preservation is inferred from this resource.
• ConversionRecipe.run_predict and the converter correspondence proofs,
  which connect source-only prediction to every bounded production expression
  conversion form and all four standalone declaration converters. Recipes
  retain source resolution, sharing and universe caches, normalization, hints,
  and errors. Their finite candidate lists, together with the initial table,
  define the collision domain. Successful and failed executions agree with
  prediction and retain coherent tables covered by that domain. The optional
  predictStandalone? API verifies the source and selects standalone entries;
  production loader behavior is unchanged.
• SourceStateInvariant, which combines standalone source agreement with the
  earlier ownership and coherence invariant. It starts empty after the finite
  source check and survives actual lookup on both outcomes. Source ownership
  prevents block publication from overwriting a selected standalone.
  OwnedInferenceTrace.preservesSource threads this resource through supported
  recursive calls using finite conversion data at constant misses, and
  frameSource returns it together with the existing cache frame.
  StandaloneModelBinding.getConst derives actual lookup arity, type reading,
  and coherence from the immutable source prediction. The scoped/closed
  ofSource support builders and infer_const_source_sound use those facts
  without post-load reading premises. Source/model bindings, finite collision
  and level data, operational traces, and model admission remain explicit.
• SourceCacheHistory.invariant, which establishes agreement for a finite
  source catalog from the actual empty lazy state. SourceCacheEntry records
  both the predicted result in each populated partition and the loaded
  declaration that produced it. OwnedInferenceTrace.preservesCache follows
  every recursive write at a catalog key, including repeated constant and sort
  writes. Finite domains containing the catalog inputs and executed input
  prevent another syntax form from overwriting those keys. Lookup on both
  outcomes, policy changes, binder opening and cleanup, and cache clearing
  preserve the combined invariant.
  CachedConstantInferenceSupport.ofSourceCache derives the loaded declaration
  and substituted cached result. BinderInference.constFromSourceCache and
  sortFromSourceCache construct leaves from actual cache selection.
  infer_const_history_sound derives typing from a history beginning empty,
  with no initial cache agreement or new post-load reading premise. Catalog
  membership, static source/model bindings, finite data, and operational traces
  remain explicit. Composite/local semantic cache typing and the full checker
  state invariant remain obligations.
• ModelTyping.no_false, which excludes a closed model-typed expression at
  primitive False in a certified environment under the set-theory hypothesis.

The production declaration and environment proofs then derive typing for their
supported executions. They do not assume a generic checker-soundness interface
or treat a separate certificate validator as evidence that the production
checker is sound.

Production environment theorem

checkEnvAnon_atomic_preserves_model handles standalone definitions,
theorems, and opaque definitions with their declared universe parameters,
whose bodies are universe terms, references to earlier interface entries, instances of
polymorphic constants, or closed function bodies in the binder fragment.
Referenced types may contain dependent functions.
For example, the fragment includes declarations with these shapes:

axiom P : Prop
axiom p : P
def q : P := p
theorem r : P := q
def typeAlias : Type := Prop
axiom ident.{u} : (α : Sort u) → α → α
def propIdent : (α : Prop) → α → α := ident.{0}
def idProp (P : Prop) (p : P) : P := p
def useId (P : Prop) (p : P) : P := idProp P p
def applyProp (P Q : Prop) (f : P → Q) (p : P) : Q := f p
def usePoly (P : Prop) (p : P) : P := ident.{0} P p
axiom T.{u} : Sort u
axiom f.{u} : T.{u} → T.{u}
def useF (x : T.{1}) : T.{1} := f.{1} x
def idSort.{u} (A : Sort u) (a : A) : A := a
def aliasSort.{u,v} : (A : Sort (max u v)) → A → A := idSort.{max u v}
def useSort.{u} (A : Sort u) (a : A) : A := idSort.{u} A a

This example illustrates the supported shapes; the theorem also requires the
operational witnesses below. It does not automatically construct a certificate
for every serialized environment containing such declarations.

Axiom policy

The initial interface contains exactly the source axioms and retains their
declared universe arities. Their types have no free term variables, use only
their declared universe parameters, and refer only to that interface.
A Realizes witness supplies a model of these axioms, and every admitted
definition extends that model while retaining all previous interpretations.

The assumption is model existence. A converse theorem turning arbitrary
syntactic consistency into model existence is outside this result. There is no
axiom-name allowlist: the no-False corollary requires the designated false type
to be interpreted as empty in the initial model, and model extension preserves
that interpretation.

Execution boundary

AtomicEnvironmentFragment makes the following conditions explicit:

1. Every source key appears in the actual buildAnonWork result. Each work item
   represents an axiom or definition, and lookup/routing/reset witnesses identify
   the exact KConst reached by the production checker.
2. Definition observations refer to the states reached in the original serial
   work order, including cache clearing. Definitions are admitted in semantic
   dependency order with fresh interface references.
3. Application, forall, and lambda nodes execute supported misses or reuse
   earlier actual synthesis checks. Composite hits retain the original tree,
   source reading, and successful execution through interface growth and
   insertion of locals. Successful full inference and a cache frame derive
   the later selected entry; fresh-local reading transport shifts captured
   source and result annotations. A complete supported cache history can now
   supply that earlier check from actual publication events at every full key.
   Its rich synthesis nodes derive the event annotations; older checking-only
   wrappers still supply omitted child checks. Selection needs finite
   query/history collision data, and use after a scope exit still needs an
   appropriate context relation. Cold nodes miss every eligible
   partition; full mode leaves the ignored inference-only partition
   unconstrained. Sort nodes use a miss or a hit equal
   to the canonical successor sort; maintained agreement constructs that leaf.
   Local-variable hits must match the current
   production declaration type. Constant nodes use the existing miss rule or
   a selected hit. Hits check the loaded declaration, finite level resources,
   and equality of the cached value with pure substitution of its type. They
   supply arity agreement because the runtime guard is skipped. A miss's lookup
   agrees with an already admitted type and universe count. Specializations supply
   closed arguments and finite substitution resources at the actual post-lookup
   state. The declared type's occurrence annotations agree with those of the
   substituted entry. Ordinary aliases retain their simpler empty-substitution
   path. Sort misses retain their finite interning-coherence and
   address-faithfulness premises.
4. Conversion uses either the initial hash-equality path, with faithfulness
   of the compared expressions, or a beta-reducible declared type. The latter
   reuses the declaration's actual type-inference tree to derive equality with
   its model substitution; the value's inference returns that substituted
   type. No additional generated-type check is assumed. General reduction and
   conversion-cache paths require additional proofs.
5. checkEnvAnon returns .ok results, and every result row has no error.
   The outer .ok alone can contain failed declarations and is insufficient.

The proof extracts successful validation, type inference, the theorem guard,
body inference, and conversion from the public checker execution. It derives
body typing and uses extend_atomic_definition to extend the previous model.
The operational and representation inputs contain no body-typing or
checker-soundness premise.

Additional results make the boundary reviewable:

• WorkPosition.check_success recovers a successful declaration check at the
  precise serial work position from all-success result rows.
• AtomicDefinitionRun.no_self_alias rules out using a fresh definition to
  justify its own type through a reference to itself at any universe arguments.
• checkEnvAnon_atomic_represents_source relates every source address to the
  interface entry carrying the type and body reached by production lookup.
• checkEnvAnon_atomic_no_false excludes a resulting declaration at an axiom
  type interpreted as empty, including the designated False type.

Binder definitions additionally supply finite inference trees for the actual
value and its separately checked declared type, exact scoped readings, closed
annotated syntax, and references to the preceding interface. The trees follow the
smaller production method table, require syntactic sort exposure, and retain
an initial structural local invariant, interning coherence, finite
collision freedom, and bounds excluding index overflow. Lambda nodes use full
mode and the unchanged cheap-beta path. BinderInference.sound derives
CheckingClaim; declared-type formation converts it to typing, without an
assumed codomain-typing judgment. Local cache hits are tied to the exact type
returned by the current production declaration.
Domain-context restoration and fresh identifiers now follow from actual
recursive execution. The same context transport is used by retained codomain
checks, lambda-body argument origins, and cache publication proofs.
Constant hits require concrete agreement with a loaded declaration and its
pure universe-substituted type. This admits repeated carrier references in
the domain, codomain, and body of declarations such as useF, even when caches
are cleared before every item. The resulting type stays closed under active locals.
Sort hits also admit repeated domains such as
def chooseLeft (P Q : Prop) (p : P) (q : Q) : P := p.
Closed constant witnesses can be reused after a composed frame preserving
their cache entries, checking policy, and loaded declarations. Binder opening
derives such a frame directly; sort and already-loaded constant inference
frame other keys. This reduces repeated observations without assuming semantic
typing of cache data. Frames retain every old declaration while allowing
fresh declarations to be added. getConst_verified_cache derives this
extension for the installed production loader with verification enabled,
including source misses, integrity/parse errors, conversion failures,
reserved-address rejection, and deduplicated faults. Conversion accesses only
intern tables; the initial lookup miss supplies freshness for single-entry
registration. Mutual-block publication follows the actual left-to-right insertion
fold. BlockEntriesCompatible requires each entry returned by actual preparation
to agree with any previously loaded declaration at its key. Its constructors
accept fresh entries or a mixture of fresh entries and exact repeats. They
assume neither a cache frame nor a final environment invariant, and uniqueness
among fresh entries is unnecessary. The verified path also handles parent lookup
failure, block deduplication, and lookup failure after successful publication.
Other checker fields and the fresh-id counter remain unchanged.
For an entire recursive call, InferenceCacheTrace computes the writes from
its operational tree and derives the cache frame and policy equality for any
unwritten key. It shares application and binder traces and includes the
lambda-domain call used by production validation. Repeated protected references
can appear as hits, which contribute no writes. Constant leaves can load a
verified standalone or mutual block and then use universe-walker resources at
the actual post-lookup state. CachedConstantInferenceSupport.afterVerifiedInference reuses
an earlier witness after such a constant call; recursive transport covers
loads inside applications and binders. The general interface retains declaration
agreement as a premise; bound standalones derive the actual lookup's arity,
reading, and coherence from source prediction. Finite collision/level data
remain explicit resources. Block overlap follows
from the source ownership check and the preserved loaded-block invariant for
states initialized empty and advanced by supported calls. OwnedInferenceTrace
threads this invariant and intern coherence through recursive applications and
binders, deriving each constant leaf's loader resource and preserving the same
cache-write footprint. Arbitrary partial states retain the general pointwise
compatibility interface.
SourceStateInvariant also maintains agreement with the standalone catalog.
It starts empty and survives successful supported recursive inference, both
lookup outcomes, and block publication. Its static bindings read the predicted
type in an admitted model entry; this does not admit a source declaration or
interpret a mutual block.
SourceCacheHistory starts at empty caches and derives predicted result
agreement and loaded-declaration coverage for a finite catalog. Recursive
preservation includes the catalog's written keys, guarded by finite input
collision data. The resulting invariant constructs constant and sort leaves
through actual hit/miss selection and retains the state resource across
lookup errors, scopes, policy changes, and clearing.
Actual loading derives key coherence from its pre-state on both outcomes;
the production lazy state starts with coherent empty intern tables. Constant
inference also returns coherence after substitution and the cache write, so it
can be reused by the next operation. General preservation through all checker
operations remains open. This tree proves state effects;
semantic typing of application, forall, and lambda cache hits remains open.

The BinderInference application spines start with a local or an admitted constant.
BinderInference.synthesis derives the function type's hereditary validity
from the current context or dependency model. Its domain then supplies the
validity needed to check the argument, including lambda arguments.
Faithful hash conversion and matching occurrence annotations connect the
argument's inferred type to that domain. The actual memoized codomain
substitution agrees with model substitution beneath nested binders and in
the presence of active locals.

Its applications require full mode, syntactic Pi exposure, an argument without
an eager-reduction marker, and concrete context/substitution resources at the
actual recursive-call states. The synthesis rules additionally admit direct
lambda applications, returned functions, and supported beta Pi exposure.
Polymorphic constants supply a closed scoped
reading of the selected entry type and finite substitution resources. On
misses, instantiateUnivParams_readScopedAnnotated connects the actual
universe walker to a reading of the returned type in the active local context, retaining term scope and
occurrence annotations even when universe levels simplify. A pure
readInstantiatedType? check fixes the finite inference tree's chosen result
syntax; this check contains no semantic typing premise. Cache hits instead use
instantiateUnivParamsSpec_readScopedAnnotated and exact cached syntax agreement,
requiring no mutable interning resources. Arity follows from the runtime guard
on misses and a concrete equality check on hits. The admitted dependency model
establishes the polymorphic typing rule in both cases.
Monomorphic references retain the simpler empty-substitution path. General Pi
exposure through other reductions and cache paths still needs further proofs.

Automatic construction of these witnesses, broader application paths,
broader lambda paths, inductives, coordinated blocks,
and general conversion remain outside this
production fragment.
Polymorphic constant inference is composed into declaration admission and
environment model extension at the exact declared universe count. Definitions
can use their own parameters in sorts, binder conditions, and references to
earlier constants. The model interprets each checked body at every universe
instance while preserving all existing interpretations. For binders,
DefinitionBodyTrace.scopes uses the actual type/value validator calls and
finite collision coverage to recover source bounds; the scoped reader
establishes term closure without interpreting a wrapped kernel binder depth.
Only bounds on the auxiliary occurrence conditions are checked independently.
Refinement of the independent serialized-Ixon reader is also a separate boundary.

What full production-checker refinement requires

The set model and the relative axiom premise already have their intended roles.
carneiro_implies_ix constructs the required set-theory interface on ZFSet
under OmegaInaccessibles. Certified acceptance then gives its proved
acceptance-to-model and no-False results. For arbitrary source axioms, supplying
a model of those axioms is the premise whose preservation the production
theorem establishes.

Full refinement would extend the direct result to the complete ordinary
Lean implementation in Ix.Kernel, in its full-validation configuration.
The intended statement is: given faithful source decoding and the documented
representation, hashing, and arithmetic assumptions, if checkEnvAnon succeeds
with no error in any result row, every admitted declaration has its stated
meaning in an extension of the source-axiom model. In particular, a declaration
whose type denotes the empty set cannot be accepted. The theorem must derive
the semantic typing facts from the actual production execution.

The following obligations describe the remaining connection. Existing
implementation lemmas provide substantial support; they must be connected to
the set-model judgments with the required assumptions discharged or stated.

1. Expression representation and source loading. Extend the current closed
   and scoped readings of KExpr to every expression form admitted by the full
   checker configuration. The scoped reading now follows registered locals,
   fresh-variable opening, and abstraction through the supported binder paths.
   Prove that production Ixon loading, block/member
   lookup, substitution, and generated auxiliaries
   preserve the intended declarations and expressions. The current structural
   reader handles projections, natural literals, and let substitution; the
   scoped reader now also substitutes lets beneath registered free variables
   and binders. Its opening, closing, substitution, scope, and reference proofs
   include nested lets. SynthesisInference.outputReading now derives the
   returned syntax reading for every supported recursive constructor without
   a context-formation premise. Loose legacy variables, unknown locals, and strings
   still fail that reading. The atomic environment theorem
   consumes lookup and representation witnesses; the full result needs the
   production loader and state invariants to establish them.
   Universe instantiation now has a direct model refinement for every readable
   type, including its memoization, interning, simplifying level constructors,
   and empty-argument shortcut. Loader agreement and the finite-support
   resources consumed by that theorem still need to follow from the general
   state invariant.

2. All inference branches. Connect successful runs of infer and
   inferUncached in Ix/Kernel/Infer.lean to semantic typing for variables,
   lambdas, applications, dependent function types, lets, polymorphic constants,
   projections, and supported literals. This includes the inferred result type
   and the updated checker state. Direct consistency currently covers sort
   inference, polymorphic constant inference for arbitrary readable entry
   types, and finite binder/application inference trees. Constants are proved at both the
   uncached dispatcher and the ordinary inference entry point on cache misses;
   closed scoped constant types and sorts also support concrete cache-hit witnesses.
   Binder trees cover dependent function types and full-mode lambdas with
   syntactic or supported beta sort exposure and unchanged or supported changed cheap beta. Local-variable
   hits require concrete cache/declaration agreement. The original synthesis
   datatype now includes a full-mode let case with three recursive children,
   the value-type hash
   comparison, fresh let opening, and actual type abstraction/substitution and
   cheap beta. It derives term typing, returned-type reading, type formation,
   and the substituted derivation's later beta origins. Declaration admission
   includes lets in bodies and declared types. The children and surrounding
   binders, applications, and retained cache hits may themselves contain lets;
   typed histories retain these original recursive checks. Forall, lambda, and
   let sort-aware traces recover all raw child observations from successful
   inference; both forall children may need sort exposure. SynthesisSortCheck
   converts the original inferred type through retained checked beta origins,
   including a supported outer-cache hit, and supplies the binder's actual
   exposed level. Finite execution, walker, collision, and
   selected beta-origin resources remain explicit. These results do not yet
   construct the general semantic loader/state invariants. Structural local
   coherence, the allocation-counter bound, and scope restoration are now
   proved through the complete recursive checker, including the concrete lazy
   loader and initial state. Let inference consumes these results to derive
   its intermediate contexts and freshness from actual execution. Composite synthesis hits
   reuse an earlier successful check and preserve its full inference tree;
   a successful full call and cache frame derive the later selected result.
   The check now crosses interface growth and local insertion while retaining
   the original Pi domains, codomains, and lambda-body argument checks.
   The environment theorem
   composes this inference result for definitions with their own parameters using the
   derived scope/reference facts and structural annotation agreement.
   Closed bodies such as idProp, useId, and usePoly above are included, as are local
   function applications with dependent results and checked lambda arguments.
   Applications use full mode, syntactic or supported beta Pi exposure,
   ordinary arguments, and hash comparison with the exposed domain.
   Polymorphic references preserve their closed substituted
   types beneath active locals, with a pure syntax/annotation check selecting
   the tree's result. Constant hits use the same pure substitution semantics
   with concrete cache/declaration agreement and explicit arity. Beta Pi
   exposure follows the public WHNF call, including cold cache writes or a
   supported outer-cache hit. Its conversion comes from an actual retained
   check of the function type. The next argument starts in the computed
   post-exposure state. The argument spine preserves conversions between
   successive dependent applications and through all later beta derivations.
   General Pi exposure through other reductions or cache paths, eager arguments, and
   automatic checking origins for arbitrary generated types remain open.
   Recursive lambda inference now includes changed cheap beta when a retained
   actual type-check tree supplies the original checked lambda domains. Its
   context comes from actual domain checks, and a pure transport follows
   interface growth, weakening, universe instantiation, and dependent term
   substitution. Codomain origins are extracted from actual earlier
   function-type checks, and function/argument calls derive domain membership
   through their recorded hash comparison. Substitution updates the types of
   retained dependent parameters. Checked variable applications now retain
   the exact local head type and their argument calls. Nested codomain checks
   are extracted through their actual scopes. Earlier parameter substitutions
   update these origins, and a lambda substituted for the head contributes its
   own checked prefix; later arguments preserve the resulting reduction.
   A supplied lambda application retains its initial argument checks, which
   join the original codomain's checks after lifting beneath retained
   parameters. Both lists contribute to the selected beta prefix.
   Lambda-body extraction also retains the actual argument spine separately
   from the inferred codomain when cheap beta changes the original body type.
   The first beta result retains typing at the current codomain, allowing a
   supplied lambda to contribute a second prefix without fresh inference of
   the intermediate term.
   Finite beta traces now retain generated function and argument origins,
   type conversion, and application suffixes. Original source inference
   extracts the head and every argument check, including binder-backed spines.
   SynthesisInference.betaTyping now retains every lambda body, both
   application children, and both function-type checks, including a body's
   changed cheap-beta type and lets inside any supported constructor.
   Hereditary substitution rebuilds that derivation beneath dependent binders.
   Each result therefore supplies the exact syntactic lambda domains and
   argument origins for every later head-beta step automatically. This covers
   all current source-inference constructors; deriving the initial inference
   and generated-type resources for every production branch remains open.
   Returned syntax readings let this reconstruction precede the synthesis
   semantic induction without a context-formation premise. The induction
   derives its own semantic invariant closed under substitution; no source
   constructor or derivation producer assumes it, as enforced by the audit.
   The raw reader
   derives the selected prefix, reduced type, and final intern coherence.
   Direct lambda applications are now supported
   by synthesis trees that derive formation from actual domain and earlier
   declaration type checks. These include returned functions, dependent
   codomains, and earlier types that themselves contain lambda applications.

3. Reduction and conversion. Prove that the actual successful reduction and
   equality paths in Ix/Kernel/Whnf.lean and Ix/Kernel/DefEq.lean preserve
   denotation and justify the conversion used to check a declaration's body
   against its declared type. This includes unfolding, substitution, recursor
   and projection reduction, extensionality/proof-irrelevance rules, primitive
   shortcuts, and recursive comparisons. The production theorem now includes
   hash equality and beta reduction of a declared type, justified by that
   declaration's actual type check. Source beta inference yields both semantic
   equality and typing of the substituted result for the original lambda
   prefix, dependent arguments, and a remaining application suffix. The
   production multi-argument structural-WHNF step reads that result through
   the actual lambda peel, simultaneous walker, and interned suffix, preserving
   intern coherence. Selected cheap-beta plans have the same meaning from an
   actual source check. Model typing, checking, and equality are preserved by
   substitution, including beneath remaining dependent parameters. An earlier
   checked beta prefix can now be transported through those substitutions
   inside lambda inference. A checked variable-headed codomain now gains a
   new reduction origin from the actual lambda argument substituted for its
   head, including through earlier and later dependent substitutions. Supplied
   lambda applications also retain their existing arguments, and a selected
   reduction can consume both those arguments and the codomain's arguments.
   When an outer lambda applies its parameter, its retained body and actual
   argument checks now compose the first beta step with a prefix of the
   supplied lambda. This includes changed body-type inference, initial
   arguments on the supplied lambda, and a remaining application suffix.
   A representation theorem connects retained origins to the actual
   multi-argument WHNF step, and declaration admission now includes these
   two successive prefixes. Finite beta traces now compose arbitrarily many
   retained prefixes, preserving the initial type even when adjacent steps
   retain different types. The corresponding structural-WHNF trace computes
   each intermediate expression and intern table, proves the actual uncached
   loop with its final unchanged iteration and fuel bound, and supplies
   declaration conversion. BetaWhnfTrace now needs only raw operational,
   reading, and finite representation resources: annotate derives all
   semantic step origins from the original inference's complete beta typing
   derivation. beta_whnf_sound preserves the original type, conversion,
   reading, and intern coherence through the actual uncached loop, and the
   declaration helper supplies the existing model-extension boundary.
   Public beta WHNF now computes instrumentation, context-key memoization,
   the shared-fuel charge, and all three cache insertions. Its proved reducer
   tails terminate on sorts, Pis, and lambdas without extra recursive-call
   premises. BetaPiExposure derives the actual ensureForallDirect call
   and the exposed domain/codomain readings, either from a cold public path
   or its exact result in the outer cache. SynthesisInference.appBeta
   consumes that call in the original inference recursion. A retained actual
   type check constructs the conversion trace, so generated Pi typing is
   derived rather than assumed. Existing source-beta and declaration roots
   include this case. Initial coherence, finite walker resources, and the operational path
   remain explicit. Constructing the initial inference and operational traces
   for arbitrary accepted programs and proving the remaining WHNF/conversion
   paths are open.

4. Mutable state and recursive calls. Establish semantic invariants for
   inference, WHNF, conversion, equivalence, and block-result caches across
   insertion, reuse, scope changes, and environment extension. Cache keys must
   identify the relevant expression, context, and checking policy. Connect the
   bounded recursive method table in Ix/Kernel/Knot.lean to those invariants
   for every mutually recursive call. Finite binder trees already follow the
   decreasing table. The structural local component is now proved for the
   complete recursive table: coherent lookup, the allocation-counter bound,
   and observable scope restoration hold on success and partial failure.
   The actual ingress loader preserves the counter and establishes the initial
   invariant. Let, forall, lambda, and application inference derive their
   intermediate contexts and freshness from these general effects. Their
   traces retain initial structural state rather than exact context-equality
   facts; separate freshness fields have been removed from binder and synthesis
   nodes. Application exposure derives its context from the actual call.
   Finite binder trees also
   justify local-variable, constant, and sort cache hits
   from concrete declaration, substitution, or canonical-sort agreement.
   Exact selection preserves full-result priority and policy separation.
   Sort and already-loaded constant inference preserve agreement at their key
   and frame other entries. Structural frames compose through actual key
   computation, interning, binder opening, unrelated writes, and scope/policy
   cleanup, including errors; cache clearing establishes empty agreement.
   A finite InferenceCacheTrace now composes preservation through applications,
   foralls, and full-mode lambdas at keys outside its computed write footprint.
   It includes lambda-domain validation, actual scope cleanup, and hash
   conversion's statistics update; it preserves loaded declarations and policy.
   Later closed constant witnesses and sort leaves follow without repeated
   cache-hit observations. Verified standalone and mutual-block lazy loading
   now supply a declaration-extension frame on every outcome, including partial
   intern progress, fault and block deduplication, and errors after publication.
   Block publication requires each prepared entry to agree with any old
   declaration at its key. The trace composes constant misses through this loader
   using resources at the returned lookup state. For a fixed source, an optional
   finite header check establishes disjoint projection ownership. The invariant
   that loaded projections have recorded blocks starts empty and is preserved
   by lookup on both outcomes and supported successful recursive inference.
   It derives fresh entries for unrecorded blocks, discharging overlap checks on that path;
   arbitrary partial states retain the general compatibility premise.
   General semantic cache agreement, general state/source invariants, operational trace
   construction, finite post-lookup collision/level
   data, and the remaining recursive paths still
   need proofs. Block-check verdicts form a separate cache: a warm success skips
   body validation, while low-level declaration replacement leaves that verdict
   intact. A reproduced internal-state probe accepts a replaced invalid body
   until the verdict is cleared. That probe bypasses fresh, hash-verified ingress;
   the public theorem must derive verdict provenance from completed checks,
   preservation of the checked declarations and block membership, and failure
   isolation. Hash integrity alone does not establish dependency acyclicity or
   cached semantic validity. Composite synthesis hits now retain the original actual check,
   with its lambda domains, dependent codomain checks, and beta derivations.
   A successful full inference supplies the stored result, and frames derive
   its later selection at the same key under either policy. The retained source
   checks survive interface growth and insertion under dependent binders.
   Fresh-local reading transport and the actual opening frame preserve captured
   cache entries. These resources construct the cache case of the original
   synthesis recursion and remain usable by later beta origins. The existing
   named-specification and recursion proofs provide further supporting lemmas.
   Key coherence is now derived through bounded universe/expression conversion,
   every declaration conversion form, and the actual lazy lookup on success and
   error. Successful constant inference carries coherence through key computation,
   lookup, universe substitution, and cache publication. OwnedInferenceTrace
   carries both ownership and coherence through application substitution, binder
   opening, and lambda abstraction using finite walker data and one initial
   state resource. It derives the existing cache-frame tree, so later constant
   witnesses and sort leaves reuse these invariants without per-leaf loader or
   post-lookup coherence premises. Extending preservation to all checker
   operations remains part of the general state proof.
   Standalone source agreement is now derived from immutable conversion
   predictions and finite candidate collision data. It starts empty and
   survives lookup on both outcomes and supported recursive calls. Static
   source/model bindings replace mutable post-lookup reading and arity
   witnesses for these declarations. Mutual-member interpretations, automatic
   model admission, and general semantic cache agreement remain open.
   For a finite catalog of closed sort and standalone constant instances,
   SourceCacheHistory now establishes both partitions' agreement and loaded
   dependency coverage from the empty state. It preserves entries at written
   catalog keys through supported recursive calls, using finite collision
   domains to separate other input forms. Actual cache selection builds the
   existing inference interfaces, and constant typing follows from the history
   and static source/model binding. This discharges initial and repeated cache
   witnesses on that path. Composite reuse additionally follows an actual
   successful synthesis check through preserved entries, interface growth,
   and insertion beneath dependent binders. Complete event histories now record
   every actual miss and reconstruct both entire maps for the supported trace,
   so every present value has a producing call, including at written keys.
   Full-cache priority also preserves every initially occupied full key without
   a write-exclusion premise. The rich synthesis recursion derives each new
   full publication's original checking tree and context from its actual children
   and domain calls. Older checking-only wrappers need supplementary omitted-child
   annotations and operational resources. Finite query/history collision data
   recovers the same source at selection and constructs its full retained cache
   check. The raw trace and exact map fold now include full lets and all three
   children. The same recursive let check and child cache data now construct
   the typed history as well, retaining the root and all descendants for later
   full-cache selection. Initial occupied full keys remain protected by cache
   priority. Sort-aware forall, lambda, and let nodes use the same original
   child trees and typed history. Exposure preserves both inference-cache maps,
   so each child retains its actual inferred type before sort reduction.
   Each retained
   synthesis check keeps its original local context. Arbitrary later-context
   compatibility after scope exit, general execution/resource construction,
   remaining omitted-child annotations, and other inference paths remain open.
   Supported public beta paths additionally compute all three WHNF cache
   writes and preserve the local context and intern coherence. Outer-cache
   reuse retains the earlier raw path's exact result and works with zero
   fuel, including while native reduction is active. Cold paths require
   all three cache misses and an inactive native guard. General semantic
   WHNF cache histories, mixed cache states, and preservation through other
   reducers remain open.
   Public beta WHNF and Pi exposure now derive inference-cache frames at every
   key from their computed state updates. InferenceCacheTrace includes those
   exposures between function and argument inference, and changed cheap-beta
   lambda bodies. Thus the same write-footprint proof supplies later reuse of
   full composite checks. Clearing removes the entry and requires another
   full check before reuse; no cache-presence premise is inferred from empty
   agreement.

5. General declaration admission. Lift body typing and conversion to model
   extension for the full declaration forms handled by Ix/Kernel/Check.lean
   and Ix/Kernel/Inductive.lean. The supported standalone definitions now
   retain their own universe parameters through admission and model extension;
   their body and conversion paths remain restricted as described above.
   Safe definition validation now enforces an acyclic dependency graph, and the
   production traversal has proved root coverage, declaration order, and
   well-foundedness. The memoized collector is complete under finite syntax
   collision freedom. Successful validation supplies the order used to bound
   references in the model reading. General member admission and construction
   of interpretations for that order remain to be composed.
   Coordinated inductive, constructor, and recursor blocks need their universe, parameter,
   positivity, elimination, and reduction conditions connected to the
   mathematical interpretations. The certified validator already checks its
   supported inductive/model schemas; proving that the ordinary production
   checker enforces the corresponding conditions is a distinct obligation.

6. The complete public environment run. Compose the declaration results
   through actual work enumeration, dependency ordering, block coordination,
   cache resets, and error propagation. Derive the source coverage, freshness,
   and execution facts currently packaged in AtomicEnvironmentFragment for
   every admitted work item. The final theorem must still require every result
   row to be successful: outer .ok can contain declaration errors. Other
   entry points or execution configurations need equivalent composition
   results before inheriting this contract.

7. Close the dependencies used by the final theorem. The broader named
   implementation library retains audited unfinished results. For example,
   its public declaration-checking roots currently reach
   Ix.Theory.Named.VEnv.IsDefEqU.forallE_inv_stratified and
   Ix.Theory.Named.VEnv.IsDefEqU.sort_inv, tracked in
   Ix/Kernel/Verify/Audit/Statements.lean. A full result that reuses those
   roots must discharge those dependencies or use a proved alternative.
   Existing direct consistency roots already exclude proof holes and
   implementation/metatheory bridge axioms. The expanded theorem needs an
   equally explicit audit of its actual dependency closure.

These obligations concern acceptance soundness. They do not require the
fuel-bounded checker to accept every valid declaration or succeed with every
fuel budget. The finished connection would let a full successful production
run inherit the established model-based consistency result without a separate
atomic-fragment witness.

The other implementations have additional transfer obligations:

Implementation	Connection needed to inherit the result
Rust checker in crates/kernel	Relate Rust execution and any accelerated operations used by a checked path to the proved semantics, including representation, arithmetic, and state behavior. Differential tests provide regression evidence, not that refinement theorem.
Aiur checker in Ix/IxVM/Kernel	Relate the checker program's accepted executions to the model, then establish the compiler/trace/AIR and proof-verification connections with the actual program identity, public inputs, and permitted keys bound to the claim.

The Lean implementation proofs, Rust transfer, and Aiur/proof-system transfer
are separate claims. The completed certified host consistency results and the
direct atomic Lean theorem do not depend on completing those later transfers.

Certified source and claim commands

Ix.Certified adds maintained host adapters and explicit checker entry points.
Requests and envelopes have typed Lean APIs and binary or readable text Ixon
representations. Binary input is the default:

certified-check proof SOURCE.ixe REQUEST.ix
certified-check store SOURCE.ixe REQUEST.ix
certified-claim-check SOURCE.ixe ENVELOPE.ix REQUEST.ix

certified-check --request-format text proof SOURCE.ixe REQUEST.ixon
certified-claim-check --request-format text --envelope-format text \
  SOURCE.ixe ENVELOPE.ixon REQUEST.ixon

The request and envelope format flags are independent and accept binary or
text; mixed inputs are supported. Command.Request, ClaimCommand.Request,
and Envelope expose toIxon/ofIxon, toText/ofText, and
Ixon.Serialize instances. Text uses the existing .ixon grammar with one
typed constructor value. Binary requests have a versioned header and distinct
source/claim tags, with exact canonical decoding and bounded input sizes.
Existing JSON requests are an explicit --request-format json compatibility
mode, including the frozen command regressions.

Successful source validation connects authenticated Ixon to model admission.
Claim validation additionally checks the exact envelope bytes, expected content
address, canonical re-encoding, and protocol versions. The checker version is
2; format, codec, policy, and aggregation versions are 1. Older checker
envelopes and trailing bytes reject. Binary envelope bytes retain their original
representation. Text envelopes authenticate their canonical Ixon encoding, so
formatting does not affect the expected claim address. All formats reach the
same proved command acceptance functions.

ClaimCommand.run_meaning proves that successful pure execution yields a receipt
for the exact envelope and its SemanticClaimMeaning. A logical receipt with a
closed structural frontier constructs its model; LogicalReceipt.no_False
excludes a checked subject at the profile's false proposition under [SetTheory V].
Source axioms retain the logical policy's model hypotheses. A closed structural
frontier does not imply an empty logical-axiom manifest.

Witness search proposes certificates and the validator checks them. Unsupported
forms, unavailable models, or exhausted search decline. The current commands
use fuel 6,400, so acceptance soundness does not imply completeness. Membership
and revelation have their own structural meanings; evaluation claims are
outside this semantic profile.

The maintained native tests and actual CLI executions are compared against
frozen source/claim evidence:

Corpus	Fixtures	Accepted executions	Rejected executions
Source proof/store	42 source fixtures	84	562
Versioned claims	1,578 claim fixtures	584	5,454
Modeled source and claims	44 source and 74 claim fixtures	30	540

The modeled native tests also cover 29 source mutations with accepted controls,
42 forged witnesses, and nine malformed mutual inputs. Further regressions
exercise lazy loading, cold/warm caches, rollback, claim cycles, shared
dependencies, source fidelity, membership, and revelation.

Native Lean execution, transport parsing, filesystem loading, and the BLAKE3 foreign interface
remain execution boundaries. Certified execution inside an authenticated Aiur
proof is a separate obligation. The VM pilot and its evidence are preserved in
the frozen archive and excluded from the maintained host gate.

Trust audits and provenance

The axiom visitor traverses checked declaration types, bodies, and inductive
constructor fields, following direct dependencies in the current Lean
environment. It records proof-hole origins and checks exact axiom sets rather
than relying on cached imported axiom summaries. Direct dependency lookups are
cached within an environment; each root's reachable declarations and assumptions
are still computed separately.

Boundary	Audit coverage	Contract
Named specification	441 assertions	Exact dependency/axiom manifests, including retained unfinished metatheory
Kernel implementation proofs	2,037 manifest roots	Per-root assumptions and proof-hole origins; completed roots cannot depend on Ix.Kernel.Frontier.Pending
Consistency foundation	145 roots	Exact root types, premise structure, recursion workers, and mathematical import boundary; no proof holes or unapproved axioms
Direct production consistency	1,336 theorem boundaries	No proof holes or metatheory/implementation bridge axioms; production roots also forbid generic soundness interfaces and the independent certificate validator
Certified host adapters	86 distinct roots	Standard Lean axioms only in the mathematical closure, with a separate runtime inventory

The direct production environment roots retain four existing generated
output-length proofs reached through the full production method table and
expression/universe construction. This change introduces no new native proof
axioms for those roots. The pure model-extension theorem and
ModelTyping.no_false use only propext, Classical.choice, and Quot.sound,
with set theory as a hypothesis.

The universe-congruence, substitution, polymorphic-inference, and specialization
boundaries preserve that audit policy. The production substitution/inference
roots reach only the two existing expression/universe native output-length
proofs; their model-side congruence uses standard Lean axioms only.

The certified adapter audit additionally fixes 74 premise definitions or
constructor types, 9,682 logical declarations, and 10,957 declarations including
runtime dependencies. Its runtime inventory accounts for five BLAKE3 foreign
operations and 130 recursion workers with safe source definitions.

Address.blake3 and context hashing now use kernel-checked proofs of the
32-byte output bound on both supported platform sizes. The hash operation is
definitionally equal to the former wrapper; this removes an unnecessary native
proof dependency without changing the hash bytes. Frozen byte-level fixtures
guard source and envelope compatibility.

Source inventories, hashes, licenses, and notices are retained for the named
development, selected consistency model, 20 con-leche foundation files, separate
set-theory package, and frozen host adapters. Provenance checks distinguish the
original sources from maintained namespace/import adaptations.
The new level-congruence, semantic-checking, and universe-bound modules have
separate Ix-authored source inventory entries; the imported-source hashes and
notices are preserved.

Documentation and build integration

• Rewrites verification documentation and comments around the actual algorithms,
  invariants, theorem premises, and local modules. Removes branch-history and
  development-plan labels while preserving public identifiers, fixture data,
  source attribution, and unresolved proof obligations.
• Renames the recursion guide to docs/kernel-recursion.md and links it with the
  context-digest boundary from docs/kernel-verification.md.
• Adds the aggregate lake run check-kernel --with-model command. It builds
  implementation proofs, checks strict consistency roots, runs foundation and
  certified-host audits/regressions, runs kernel unit tests, and builds the
  separate Mathlib model.
• Adds a regular CI theory job and the certified-host gate. The all-target Lean
  lint driver checks production, consistency, and certified targets with
  warnings as errors. The named specification and its implementation proof
  libraries retain a separate trust gate for their audited frontier.
• Adds a separate workflow for the Mathlib model and updates the merge-queue
  kernel verification/parity job to the local namespaces and libraries.

Validation

The current sort-exposure integration increment (pending) has passed:

• lake build --wfail IxKernelConsistency: all 1,336 exact theorem boundaries
  and 296 build jobs. The preceding 1,281 exact axiom profiles pass unchanged.
  The 55 added roots cover production trace extraction, sort exposure,
  recursive checking origins, semantic conversion, and typed cache history.
  Source and cache construction explicitly forbid the hereditary invariant
  derived by the semantic induction. Existing production-interface and
  certificate exclusions remain in force. No axioms or native proofs are added.
• lake build IxKernelVerify IxCompileVerify: all 863 build jobs, including
  the 2,037 main kernel roots, 143 compiler roots, and 1,336 consistency roots,
  with the existing conditional/statement and source-frontier checks.
• lake test --wfail -- tc-unit: all 731 checks. Five additions cover forall,
  lambda, and let sort exposure in Prop, Type, and parameterized universes;
  persistent and cleared caches; exact child and parent inference maps;
  cold and warm WHNF, zero-method exposure, instrumentation and acceleration
  flags; changed lambda-body beta; and reduced-Pi rejection with scope cleanup.
• git diff --check, including the new proof module.

The original synthesis recursion now carries sort checks at domains and both
forall children. Its trace constructors extract all raw child observations
from successful production branches. The source check retains its actual
returned type; an earlier retained type check supplies the conversion to the
sort returned by the real exposure call. Binder contexts use that exposed
level. Complete beta derivations and typed cache histories preserve the
original source check, and sort exposure leaves both inference-cache maps
unchanged. This connects the existing supported public beta WHNF path and its
outer-cache hit to recursive binder checking.

Production checker code, the model foundation, named kernel/compiler proof
implementations, and certified host adapters are unchanged. The broader proof
builds and unit suite were rerun; the separate theory, certified, Mathlib, and
Lean/Rust parity gates retain their preceding results below. All seven full
refinement obligations remain incomplete. General reading, representation,
reduction, and source-checking resource construction; non-hash comparisons;
other reduction and cache paths; and full declaration/model admission remain open.

The preceding recursive-let integration increment (c67db1fb9ea3) has passed:

• lake build --wfail IxKernelConsistency: all 1,281 exact theorem boundaries
  and 295 build jobs. The preceding 1,250 exact axiom profiles pass unchanged.
  The 31 new roots cover recursive let support, retained function-type children,
  returned readings, the derived hereditary semantic invariant, and typed
  let-cache history. Source reconstruction explicitly forbids dependence on
  that semantic invariant; the existing production-interface and certificate
  exclusions remain in force. No axioms or native proofs are added.
• lake build IxKernelVerify IxCompileVerify: all 862 build jobs, including
  the 2,037 main kernel roots, 143 compiler roots, 1,281 consistency roots,
  and existing conditional/statement and source-frontier checks.
• lake test --wfail -- tc-unit: all 726 checks. Three additions cover lets
  in binder domains and bodies, function positions, nested values, composite
  declaration types and bodies under both cache-clearing settings, and failed
  nested checks with scope cleanup and no parent publication. Successful
  inference also checks full-cache storage and zero-fuel replay under both
  policies.
• git diff --check, including the newly tracked proof modules.

The original SynthesisInference.letE carries the same three actual child
checks, hash comparison, opening, substitution, and selected cheap-beta
resources as the preceding standalone let interface. Its children and all
surrounding synthesis constructors can contain further lets. Complete beta
derivations retain both checked children of a function type through dependent
substitution, so shape extraction works even when the substituted value exposes
a Pi or lambda. Returned readings precede the synthesis semantic induction;
source reconstruction no longer requires context formation. The induction
derives its own hereditary invariant and preserves the existing public typing
and formation contracts. The original typed cache history now retains let
roots and descendants and reconstructs their complete checks at later hits.

Production checker code, the set-model foundation, named kernel/compiler proof
implementations, and the certified host adapters are unchanged. The broader
verification builds and unit suite were rerun; the separate theory, certified,
Mathlib, and Lean/Rust parity gates retain the preceding results below.
All seven full-refinement obligations remain incomplete. General execution
and representation-resource construction, non-hash comparisons, other inference
and reduction branches, semantic cache invariants, and full declaration/model
admission remain open.

The preceding derived-context inference increment (f1e71c5013f2) has passed:

• lake build --wfail IxKernelConsistency: all 1,250 exact theorem boundaries
  and 286 build jobs. Twenty additional roots derive function, argument,
  comparison, domain, and exposure frames and binder freshness. Existing
  semantic, beta-origin, admission, and cache-history roots pass with their
  unchanged exact axiom policy and forbidden-dependency checks.
• lake build --wfail Ix.Kernel.Verify.Consistency.SynthesisCacheExecution Ix.Kernel.Verify.Consistency.LetCache: all 268 jobs, including the updated
  retained checking origins, beta derivations, and both cache-history consumers.
• git diff --check.

The four application/forall/lambda trace families replace their exact
local-context-equality field with the maintained structural invariant at the
trace's start. Actual recursive calls derive observable restoration. The
five separate freshness fields in binder and synthesis constructors are
removed; the same calls and model-reader agreement prove freshness.
ApplicationWhnfInferenceTrace.exposure_context now follows the actual
exposure call without a separate beta-path premise. Its semantic beta reading
and finite walker resources remain separate requirements.
General construction of these traces and their initial state resources,
arbitrary recursive let composition, and the seven full-refinement obligations
remain incomplete. Production, named kernel/compiler proofs, and runtime tests
are unchanged; their preceding validation below remains the baseline.

The preceding structural local-state increment (10c038b68667) has passed:

• lake build --wfail IxKernelConsistency: all 1,230 exact theorem boundaries,
  including 431 additional structural state, loader, recursive method, and
  model-reader boundaries. The existing forbidden dependencies and exact axiom
  policy are unchanged; the new freshness lemma uses no choice axiom.
• lake build IxKernelVerify IxCompileVerify: all 853 build jobs, the 2,037
  main kernel roots, 143 compiler roots, 1,230 direct consistency roots, existing
  conditional/statement audits, and the source-frontier check. Shared context
  extraction and the stronger universe-instantiation frame preserve the
  existing named proof contracts and exact trust boundaries.
• git diff --check, including the newly tracked proof modules.

Production code and runtime tests are unchanged in this increment. The 723
unit checks and 17 Lean/Rust parity checks passed on the preceding regression
commit below and were not rerun for these proof and documentation changes.

The complete recursive structural proof was adapted from the other checkout's
76112e2bfec6 work, preserving this branch's production code and stronger global
definition-dependency guard. Shared local-context and universe-instantiation
effect lemmas avoid duplicating the named proof development. The loader proof
uses this branch's intern-only conversion boundary on both outcomes.
The model integration removes two exact context-equality fields from
LetInferenceTrace and the separate freshness field from LetInferenceCheck.
The let typing, retained beta-origin, and cache-history proofs now derive these
facts from the actual recursive calls and one initial structural invariant.
All seven full-refinement obligations remain incomplete; semantic preservation
for general reduction, conversion, caches, and declaration admission remains open.

The preceding recursion regression and admission-boundary review (e1a03ee5a7f9)
has passed:

• lake test --wfail -- tc-unit: all 723 checks. Seven additions include the
  three positive source-recursion families, axiom-free self-reference under
  all three safe definition kinds, and a cycle spanning separate internal
  blocks. The positive exports cover 33, 1,350, and 26 checked targets in both
  hosts, with no omitted requested declarations or accepted matching failures.
• lake test --wfail -- --ignored tc-anon-diff: all 17 differential checks,
  including eleven serialized dependency-policy fixtures and the six existing
  source closures. Both hosts reject the three new axiom-free counterexamples
  with the expected target sets and cycle diagnostics.
• git diff --check.

The positive fixtures are taken from e596f0b15d29 on jcb/ixvm-consistency.
That branch's stored-definition guard rejects self-reference and cycles within
a block. This branch's existing traversal additionally rejects the separate-block
cycle from its admission-boundary probe. Both branches replay a stale cached
success after a deliberately constructed internal state replaces the previously
checked declaration. The invalid replacement fails after clearing that verdict.
The probe does not pass through fresh hash-verified source ingress and does not
establish a public-input acceptance failure. It identifies the need to derive
block-verdict validity from completed checks and preserved declarations.

The same branch's 76112e2bfec6 proves local-state preservation for all six
production method fields by induction on the actual finite method tables,
including success, failure, loader preservation, and monotone fresh allocation.
Those structural proofs are a candidate for integration into this branch's
general state invariant; they do not establish semantic inference or cache
validity. No production algorithm or consistency theorem changed in this review.
The preceding 799-root consistency audit was the proof baseline for that review.
All seven full-refinement obligations remain incomplete.

The preceding let inference increment (913a96b07047) has passed:

• lake build --wfail IxKernelConsistency: all 799 exact theorem boundaries,
  across 271 jobs. Thirty-three additions cover let reading and substitution,
  actual opening and inference states, returned-type formation, retained beta
  origins, declaration scope support, and exact cache maps and history from
  the original child checks. Existing axiom sets are unchanged; no axioms or
  native proofs were added.
• lake test --wfail -- tc-unit: all 716 checks. Five additions cover exact
  child/parent cache maps, replay and fresh rebuilding, generated-type cheap
  beta, theorem admission under both clearing settings, nested capture
  avoidance, and partial-cache/scope cleanup after rejected values or bodies.
• lake run check-theory: all 145 foundation roots, 6,569 declarations, exact
  types and dependencies, baseline axioms, and 101 inventoried recursion
  workers. The saved report changes only its declaration count for the new
  structural annotation theorem. Provenance retains 121 selected files, six
  authored modules, 20 con-leche ports, and 105 named-support files.
• lake build IxKernelVerify IxCompileVerify: 838 jobs, 2,037 main kernel roots,
  143 compiler roots, 799 direct consistency roots, existing conditional/frontier
  roots, and no source sorryAx.
• lake run check-certified: all 86 host-adapter roots and the unchanged exact
  foundation report, native suites, frozen adapter bytes, CLI scenarios, and
  binary/text input regressions. The build completed 488 jobs.
• git diff --check.

The full-mode let proof follows the actual domain, value, and body calls,
value-type hash comparison, fresh opening, type abstraction/substitution,
selected cheap beta, cleanup, and outer cache insertion. It derives typing and
formation from the original checking derivations, which also retain all later
beta origins after value substitution. The same check enters declaration model
extension and constructs the raw cache history from its children's cache data.
The scoped reader and its supporting walkers handle nested lets, but the
three inference children still use the existing synthesis fragment. Arbitrary
recursive let integration and typed history for let roots remain unfinished.
General execution/resource construction, other inference/reduction/conversion
paths, general declaration admission, and whole-environment composition also
remain open. All seven full-refinement obligations remain incomplete. The
runtime regressions exercise production and do not construct those general
proof resources.

The preceding cache history increment (c9ba57cd9223) has passed:

• lake build --wfail IxKernelConsistency: all 766 exact theorem boundaries.
  Sixty-one additions cover preservation of initially populated full keys,
  exact publication folds for both complete maps, history from empty caches,
  source recovery from finite collision data, retained synthesis-event checks,
  and their extraction from the original rich inference recursion. Existing
  boundaries are unchanged; no axioms or native proofs were added.
• lake test --wfail -- tc-unit: all 711 checks. Two additions compare complete
  full/only maps through child and parent publications, temporary local scopes,
  loading on both outcomes, clearing, and repopulation, and check occupied-key
  priority against deliberately different syntax with the same address.
• lake run check-theory: all 145 foundation roots, exact types, dependencies,
  baseline axioms, and runtime inventory; provenance retains 121 selected
  files, six authored modules, 20 con-leche ports, and 105 named-support files.
• lake build IxKernelVerify IxCompileVerify: 834 jobs, 2,037 main kernel roots,
  143 compiler roots, 766 direct consistency roots, existing conditional/frontier
  roots, and no source sorryAx.
• git diff --check.

The exact event fold covers every present value in both inference caches for
the supported execution tree. New full entries retain actual synthesis checks,
with child annotations and contexts extracted from the rich original tree.
Finite query/history collision data selects the original source and constructs
its complete retained cache interface. Policy and scope changes, verified lookup
on both outcomes, clearing, and model-interface growth preserve these resources.
Selected checks retain their original local contexts; arbitrary context
compatibility after scope exit remains unproved. Older checking-only wrappers
still require operational resources and annotations for omitted child calls.
General execution/resource construction, other inference/reduction/conversion
paths, declaration admission, and full environment composition remain open.
All seven full-refinement obligations remain incomplete. Runtime tests do not
construct those general proof resources.

The preceding cache transport increment (95d07ce1da0a) has passed:

• lake build --wfail IxKernelConsistency: all 705 exact theorem boundaries.
  Forty-two additions cover structural inversion of lifted syntax, retained
  domain/body/argument checks through interface growth and local insertion,
  successive and hereditary beta origins, and concrete full-cache resources.
  Existing synthesis, declaration, and environment roots include transported
  cache hits and retain their exact axiom boundaries. No axioms or native
  proofs were added.
• lake test --wfail -- tc-unit: all 709 checks. Two additions combine actual
  declaration growth and nested dependent locals with cached lambda/Pi checks,
  later application and beta reduction, generated cheap beta from a retained
  variable-headed codomain, both checking policies, clearing, and repopulation.
• lake run check-theory: all 145 foundation roots, exact types, dependencies,
  baseline axioms, and runtime inventory; provenance retains 121 selected
  files, six authored modules, 20 con-leche ports, and 105 named-support files.
• lake build IxKernelVerify IxCompileVerify: 830 jobs, 2,037 main kernel
  roots, 143 compiler roots, 705 direct consistency roots, the existing
  conditional/frontier roots, and no source sorryAx.
• git diff --check.

SynthesisRetainedCheck carries the original executed check through interface
extension and insertion beneath dependent binders. Its structural inversions
retain the exact lambda domains and variable-headed argument checks used by
later beta proofs. Pi checks retain both domain and codomain checks.
CachedSynthesisCheck derives the physical full entry and result reading from
the actual call. Operational frames and fresh-local reading transport let
support materialize the transported hit in the original synthesis recursion;
run proves immediate replay without recursion fuel under either policy.
All seven full-refinement obligations remain incomplete. General composite
cache histories, agreement at arbitrary written keys, initial resource
construction, other inference/reduction/conversion paths, and full
declaration/environment composition remain open. Runtime regressions do not
construct those general proof resources.

The preceding composite cache increment (d849384119e0) has passed:

• lake build --wfail IxKernelConsistency: all 663 exact theorem boundaries.
  Ten additions cover cache publication after successful full inference,
  derived selection and replay, retained synthesis trees, and inference-cache
  frames through public beta WHNF and Pi exposure. Existing beta, declaration,
  and environment roots include the composite cache case and retain their
  exact axiom boundaries. No axioms or native proofs were added.
• lake test --wfail -- tc-unit: all 707 checks. Ten additions cover actual
  application, Pi, and lambda checks; zero-fuel reuse under both policies;
  exclusion of inference-only entries from full mode; lazy loading, scopes,
  clearing and repopulation; beta exposure and changed cheap-beta body types;
  later beta reduction using cached lambdas; and fresh local key separation.
• lake run check-theory: all 145 foundation roots, exact types, dependencies,
  baseline axioms, and runtime inventory; provenance retains 121 selected
  files, six authored modules, 20 con-leche ports, and 105 named-support files.
• lake build IxKernelVerify IxCompileVerify: 829 jobs, 2,037 main kernel
  roots, 143 compiler roots, 663 direct consistency roots, the existing
  conditional/frontier roots, and no source sorryAx.
• git diff --check.

Composite cache hits retain the actual tree behind the stored type, so later
beta proofs retain lambda domains, body checks, and dependent argument checks.
Successful full calls and proved frames construct the later hit and result
reading, including across supported recursive inference and public beta WHNF.
Reuse currently keeps the same semantic interface and annotated context.
All seven full-refinement obligations remain incomplete. General cache
histories and context/interface transport, initial resource construction,
other inference/reduction/conversion paths, and full declaration/environment
composition remain open. Runtime regressions do not construct those resources.

The preceding beta Pi-exposure increment (44fd6662c1a8) has passed:

• lake build --wfail IxKernelConsistency: all 653 exact theorem boundaries.
  The 38 additions cover argument-spine conversion, raw beta state frames,
  actual WHNF keys, instrumentation and fuel, the three public cache layers,
  Pi exposure, application execution, and conversion derived from retained
  type checks. Existing inference, beta, declaration, and environment roots
  include the new application case. No axioms or native proofs were added;
  every existing root retains its exact dependency boundary.
• lake test --wfail -- tc-unit: all 697 checks. Eleven additions cover beta
  function types, successive dependent Pi exposure, Prop/Type and universe
  parameters, fresh caches, local functions beneath three binders, exact
  cache writes and fuel consumption, both statistics and acceleration
  settings, zero-fuel cache reuse, context-key memoization, and rejected
  dependent arguments.
• lake run check-theory: all 145 foundation roots and exact types,
  dependencies, baseline axioms, and runtime inventory; provenance preserves
  all 121 selected files, six authored modules, 20 con-leche ports, and
  105 named-support files.
• lake build IxKernelVerify IxCompileVerify: 827 jobs completed, with
  2,037 main kernel roots, 143 compiler roots, 653 direct consistency roots,
  the existing conditional/frontier roots, and no source sorryAx.
• git diff --check.

Application inference now exposes a Pi through a supported public beta path
or its exact result in the outer cache. The earlier type check supplies the
conversion, and subsequent dependent arguments retain their checks through
the original inference and beta derivations. Cold paths compute all three
cache writes and require an inactive native guard; warm outer-cache hits
need no fuel. All seven full-refinement obligations remain incomplete.
General cache agreement and mixed cache states, initial resource construction
for arbitrary accepted programs, other inference and reduction branches,
general conversion, and full declaration/environment composition remain open.
Runtime regressions do not construct these general proof resources.

The preceding automatic-beta-origin increment (d44456c6894e) has passed:

• lake build --wfail IxKernelConsistency: all 615 exact theorem boundaries.
  The 28 additions cover dependent context insertion, retained lambda bodies
  and application children, hereditary substitution, automatic beta-step
  typing and conversion, source-inference extraction, raw WHNF path
  annotation, and declaration admission. No axioms or native proofs were
  added; existing roots retain their exact dependency boundaries.
• lake test --wfail -- tc-unit: all 686 checks. Ten additions cover supplied
  functions substituted under two dependent binders, up to twelve later
  prefixes, reductions of both types and ordinary terms, returned lambdas,
  changed body-type inference, universe parameters, cache clearing, both
  WHNF policies, and rejected dependent arguments.
• lake run check-theory: all 145 foundation roots and exact types,
  dependencies, baseline axioms, and runtime inventory; provenance preserves
  all 121 selected files, six authored modules, 20 con-leche ports, and
  105 named-support files.
• lake build IxKernelVerify IxCompileVerify: 823 jobs completed, with
  2,037 main kernel roots, 143 compiler roots, 615 direct consistency roots,
  the existing conditional/frontier roots, and no source sorryAx.
• git diff --check.

Every finite head-beta path of the currently supported source-inference
fragment now derives all semantic step origins from its original inference.
The generated typing derivation retains exact lambda domains and rebuilds
the lambda bodies and application children after each dependent substitution.
The raw production path supplies execution, reading, and finite representation
resources; automatic annotation connects it to the actual uncached WHNF loop
and the existing declaration and environment model-extension roots. All seven
full-refinement obligations above remain incomplete. The initial inference
trees, raw paths, and representation resources still need to follow from
arbitrary successful full-checker executions, and the other inference,
reduction, conversion, and admission branches need their proofs. Runtime
regressions do not construct these general proof resources.

The preceding finite-beta-trace increment (3377f3293c06) has passed:

• lake build --wfail IxKernelConsistency: all 587 exact theorem boundaries.
  Seventeen additions cover application-spine extraction, retained typing
  origins, finite beta-trace composition, computed production steps, the
  uncached WHNF loop, and definition admission. Existing roots retain their
  exact axiom boundaries; no axioms or native proofs were added.
• lake test --wfail -- tc-unit: all 676 checks. Eight additions exercise
  three and twelve prefixes, dependent final arguments, universe parameters,
  cache clearing, both WHNF policies, exact loop-fuel exhaustion, and rejected
  carrier or dependent-argument substitutions.
• lake run check-theory: all 145 foundation roots and exact types,
  dependencies, baseline axioms, and runtime inventory; provenance preserves
  all 121 selected files, six authored modules, 20 con-leche ports, and
  105 named-support files.
• lake build IxKernelVerify IxCompileVerify: 819 jobs completed, with
  2,037 main kernel roots, 143 compiler roots, 587 direct consistency roots,
  the existing conditional/frontier roots, and no source sorryAx.
• git diff --check.

Finite beta traces retain actual source checks and reuse earlier results as
later lambda or argument origins. They preserve the original type through
arbitrarily many retained prefixes, application suffixes, and dependent
substitutions. The corresponding structural-WHNF trace computes each raw
result and intern table, proves the production uncached loop under its bound,
and supplies the existing declaration and environment model-extension roots.
All seven full-refinement obligations above remain incomplete. In particular,
these traces are explicit finite resources; the theorem does not construct
them for arbitrary accepted source programs or cover the other WHNF/conversion
branches. Runtime regressions do not construct the general proof resources.

The preceding successive-beta increment (d700fd1a95a3) has passed:

• lake build --wfail IxKernelConsistency: all 570 exact theorem boundaries.
  Eleven additions cover fresh-local lambda-body typing, term conversion,
  extraction of actual body argument checks, origins for both beta results,
  two-prefix soundness, the actual intermediate WHNF step, and declaration
  admission. Existing roots retain their exact axiom boundaries; no axioms
  or native proofs were added.
• lake test --wfail -- tc-unit: all 668 checks. Thirteen new cases include
  two actual WHNF steps with distinct lambda heads, captured carriers,
  initial and body dependent arguments, changed body-type inference, suffix
  rebuilding, universe parameters, cache clearing, and rejected domains or
  selected carriers.
• lake run check-theory: all 145 foundation roots and exact types,
  dependencies, baseline axioms, and runtime inventory; provenance preserves
  all 121 selected files, six authored modules, 20 con-leche ports, and
  105 named-support files.
• lake build IxKernelVerify IxCompileVerify: 817 jobs completed, with
  2,037 main kernel roots, 143 compiler roots, 570 direct consistency roots,
  the existing conditional/frontier roots, and no source sorryAx.
• git diff --check.

An outer lambda that applies its parameter can now reduce through that
lambda and a prefix of the supplied lambda, using the original inference
calls for both origins. The body argument checks survive a changed inferred
codomain. This reaches the actual intermediate WHNF step and the existing
environment model-extension and no-False roots. Automatic origins for
arbitrary generated types, further repeated/general reduction, and all other
full-refinement obligations above remain open. The runtime tests do not
construct the general finite inference resources.

The preceding origin-composition increment (770271606397) has passed:

• lake build --wfail IxKernelConsistency: all 559 exact theorem boundaries.
  The five additions cover exact spine flattening after substitution, lifting
  existing argument checks beneath retained parameters, semantic composition
  of the two spines, the stronger checked-origin result, and its actual
  application-call connector. Existing production roots keep their exact
  axiom boundaries; no new axioms or native proofs were introduced.
• lake test --wfail -- tc-unit: all 655 checks. Eleven new runtime cases
  include both cheap-beta plans, two- and three-lambda prefixes, dependent
  initial arguments, caller locals, universe parameters, cache clearing/reuse,
  scope cleanup, and rejected initial arguments or selected carriers.
• lake run check-theory: all 145 foundation roots and exact types,
  dependencies, baseline axioms, and runtime inventory; provenance preserves
  all 121 selected files, six authored modules, 20 con-leche ports, and
  105 named-support files.
• lake build IxKernelVerify IxCompileVerify: 817 jobs completed, with
  2,037 main kernel roots, 143 compiler roots, 559 direct consistency roots,
  the existing conditional/frontier roots, and no source sorryAx.
• git diff --check.

The supplied argument may now be a partial lambda application, and the
existing lamBeta proof consumes its combined reduction origin. Each selected
prefix is still bounded by the retained head's original syntactic lambdas.
Automatic origins for arbitrary generated types, further exposed prefixes,
repeated/general reduction, and all other full-refinement obligations remain
open. The runtime regressions do not construct the general inference resources.

The preceding exposed-lambda-origin increment (2ce0631434ed) has passed:

• lake build --wfail IxKernelConsistency: all 554 exact theorem boundaries.
  The 29 additions cover retained argument origins, local lookup after
  dependent substitution, scoped extraction from actual nested codomain calls,
  and the mutual soundness of the new reduction origin. The actual argument's
  checked lambda domains justify the newly exposed prefix. The production
  roots keep their existing axiom boundaries; no new axioms or native proofs
  were introduced.
• lake test --wfail -- tc-unit: all 644 checks. Fifteen new cases cover
  Prop, Type, universe parameters, one- and two-lambda families, captured
  carriers, earlier and later dependent arguments, cache clearing/reuse,
  exact generated/reduced types, scope cleanup, and rejected domain mismatches.
• lake run check-theory: all 145 foundation roots and exact types,
  dependencies, baseline axioms, and runtime inventory; provenance preserves
  all 121 selected files, six authored modules, 20 con-leche ports, and
  105 named-support files.
• lake build IxKernelVerify IxCompileVerify: 817 jobs completed, with
  2,037 main kernel roots, 143 compiler roots, 554 direct consistency roots,
  the existing conditional/frontier roots, and no source sorryAx.
• git diff --check.

This increment connects an actual lambda argument's checked prefix to a
previously variable-headed codomain, and lamBeta consumes the proved result.
It does not complete automatic origins for arbitrary generated types, further
exposed prefixes, repeated reduction, or the other full-refinement obligations
above. The runtime regressions do not construct the general finite inference
resources.

The preceding dependent-substitution increment (e734650268d2) has passed:

• lake build --wfail IxKernelConsistency: all 525 exact theorem boundaries.
  The 28 additions cover arbitrary-cutoff substitution through retained
  dependent contexts, preservation of typing/checking/conversion, beta-prefix
  commutation, extraction of actual codomain checks, and the mutual soundness
  of transported checking origins. The argument's domain membership comes
  from its executed function/argument checks and hash comparison. lamBeta
  consumes the resulting transport, so the production environment and
  no-False roots include it. No new axioms or native proofs were introduced.
• lake test --wfail -- tc-unit: all 629 checks. Nine new cases cover
  substituted beta-redex codomains in Prop, Type, and at universe parameters;
  a later domain B x and result C x y; exact changed result hashes;
  cache clearing/reuse, scope cleanup, and rejected argument-domain mismatches.
• lake run check-theory: all 145 foundation roots and exact types,
  dependencies, baseline axioms, and runtime inventory; provenance preserves
  all 121 selected files, six authored modules, 20 con-leche ports, and
  105 named-support files.
• lake build IxKernelVerify IxCompileVerify: 817 jobs completed, with
  2,037 main kernel roots, 143 compiler roots, 525 direct consistency roots,
  the existing conditional/frontier roots, and no source sorryAx.
• git diff --check.

This increment preserves an earlier checked lambda prefix through dependent
argument substitution. Automatic origins for arbitrary generated types,
lambdas newly exposed beyond the original prefix, and the other
full-refinement obligations above remain open. The execution regressions do
not construct the general finite inference resources.

The preceding retained-type-origin increment (14bd090c3ec8) has passed:

• lake build --wfail IxKernelConsistency: all 497 exact theorem boundaries.
  The 27 additions cover the general lambda trace, raw spine inversion and
  selected cheap-beta reading, structural substitution/weakening/universe
  laws, retained checked lambda spines, and the mutual inference/context
  soundness proof. The new lamBeta case is included in the existing
  production environment and no-False roots. No new axioms or native proofs
  were introduced.
• lake test --wfail -- tc-unit: all 620 checks. Twelve new cases observe
  changed lambda body types from local and earlier declaration checks,
  dependent prefixes, reuse beneath another binder, both application
  positions, universe parameters, cache clearing, scope cleanup, and a
  rejected carrier returned in place of its witness.
• lake run check-theory: all 145 foundation roots and exact types,
  dependencies, baseline axioms, and runtime inventory; provenance preserves
  all 121 selected files, six authored modules, 20 con-leche ports, and
  105 named-support files.
• lake build IxKernelVerify IxCompileVerify: 817 jobs completed, with
  2,037 main kernel roots, 143 compiler roots, 497 direct consistency roots,
  the existing conditional/frontier roots, and no source sorryAx.
• git diff --check.

This increment connects retained checking origins to changed cheap beta in
recursive lambda inference. Automatic origins for arbitrary generated types
and the other full-refinement obligations above remain open.

The preceding multi-argument beta increment (073a42588e99) has passed:

• lake build --wfail IxKernelConsistency: all 470 exact theorem boundaries.
  The 57 added boundaries cover simultaneous substitution, typed lambda and
  argument prefixes, the actual multi-argument WHNF step, interned suffix
  rebuilding, selected cheap-beta plans, and declaration conversion through
  a prefix and suffix. No new axiom, native proof, or semantic oracle was added.
• lake test --wfail -- tc-unit: all 608 checks. Twelve new cases cover
  dependent argument order, partial prefixes, capture avoidance, both cheap
  fast paths, fresh-variable preservation, Prop/Type and parameterized
  declaration types, cache clearing, a remaining family application, and
  rejection of a witness from the other carrier.
• lake run check-theory: the unchanged 145-root, 6,568-declaration foundation
  report and exact provenance checks. Six model modules are authored in Ix;
  imported source hashes and notices are unchanged.
• lake build IxKernelVerify IxCompileVerify: 816 build jobs pass, including
  2,037 main kernel roots, 143 compiler roots, the 470-boundary direct audit,
  and the source proof-hole checks. Existing consumers of the moved
  operational helpers retain their audited interfaces.
• git diff --check passes. Production checker behavior is unchanged.

The preceding source-beta and declaration-conversion increment (a0a4dd3188cf) passed:

• lake build --wfail IxKernelConsistency: all 413 exact theorem boundaries.
  The 15 added boundaries cover model substitution, lambda-domain inversion,
  source beta soundness, the actual one-argument structural-WHNF step and its
  simultaneous walker, and declaration conversion from an executed type
  check. No new axiom, native proof, or semantic soundness premise was added.

• lake test --wfail -- tc-unit: all 596 checks. Seven new regressions cover
  declared beta types in Prop, Type, and at a universe parameter; fresh caches;
  substitution beneath a returned Pi; unequal initial hashes and repeated
  conversion; capture avoidance in returned lambdas; and rejection of a
  proposition as its own proof.

• lake run check-theory: the unchanged 145-root, 6,568-declaration foundation
  report and exact provenance checks. Substitution is the fourth Ix-authored
  model module; imported source hashes and notices are unchanged.

• lake build IxKernelVerify IxCompileVerify: both proof libraries pass,
  including 2,037 main kernel roots, 143 compiler roots, the 413-boundary direct
  consistency audit, and absence of source proof holes. The existing direct
  beta operational equation was moved to a shared module; its consumers pass
  the same audits.

• git diff --check passes. This increment changes proofs, tests, and
  documentation, with no production checker behavior change.

The earlier inference-formation increment (064301c7e8e9) passed:

• lake build --wfail IxKernelConsistency: all 398 exact theorem boundaries.
  The 31 new boundaries cover product-fibre universe bounds, formation from
  executed type checks, full synthesis for direct lambda applications, and
  extraction of reusable axiom/definition type checks from public checker
  success. The model lemmas use only the standard logical axioms. Inference
  retains the two existing expression/universe native proofs; public checker
  extraction retains the existing four. No new axiom, native proof, or semantic
  checker-soundness premise was introduced.
• lake test --wfail -- tc-unit: all 589 checks, including eleven new direct
  lambda cases for Prop, Type, universe parameters, returned functions,
  higher-order arguments, dependent families, earlier declaration type checks,
  cache/scope behavior, and rejected domains, arguments, and universe claims.
• lake run check-theory: the unchanged 145-root, 6,568-declaration foundation
  report and exact provenance checks. The universe-bound module is the third
  Ix-authored model addition; imported source hashes and notices are unchanged.
• lake build IxKernelVerify IxCompileVerify: both proof libraries pass,
  including 2,037 main kernel roots, 143 compiler roots, the absence of source
  proof holes, and the 398-boundary direct consistency audit.
• git diff --check passes. This increment changes proofs, tests, and
  documentation; it changes no production checker behavior.

The earlier increment rejecting circular safe definitions (2f0b47c2fc09) passed:

• lake build --wfail IxKernelConsistency: all 367 exact theorem boundaries,
  including twelve new boundaries for the production dependency order,
  well-foundedness, reference-collector completeness, and the connection from
  actual safe validation to references in the model reading. The new graph and
  collector proofs use only the standard logical axioms; the two member-trace
  roots additionally retain the existing expression/universe native proofs.
  No new axiom, native proof, or semantic checker-soundness premise was added.
• lake test --wfail -- tc-unit: all 578 checks, including fourteen new
  content-addressed cycle-admission cases. They cover standalone and mutual
  circular definitions, theorem/opaque variants, type cycles, hidden references,
  shared syntax, replayed block failures, acyclic forward references, cache
  clearing, and the existing partial/unsafe policy.
• cargo test -p ix-kernel --offline: 844 passed, eight existing tests ignored,
  including six new tests for the Rust traversal and admission guard.
• lake test --wfail -- --ignored tc-anon-diff: all fourteen Rust/Lean anonymous
  verdict parity groups. Six compile ordinary Lean closures, including the Char
  ordinal regression; eight serialize the actual cycle-policy fixtures and
  compare exact target sets, pass/fail verdicts, failure counts, and cycle errors.
• lake run check-theory: the unchanged 145-root foundation report and exact
  provenance checks, with the two Ix-authored model additions inventoried.
• lake build IxKernelVerify IxCompileVerify: both existing proof libraries
  and their exact audits, with 2,037 main kernel roots after adding three state
  frames. The declaration-validator frame now includes Classical.choice,
  inherited from the new production step; its exact manifest records this
  standard logical dependency. Existing warnings in the broader libraries remain.
• rustfmt --edition 2024 --check crates/kernel/src/check.rs and git diff --check.

The CLI input-format change also passed lake run check-certified, including
strict adapter/executable builds, exact foundation and provenance checks,
frozen native/legacy CLI comparisons, and binary/text regressions. These compare
every typed field in 86 source requests and 1,652 claim requests and envelopes,
preserve authenticated envelope bytes, and exercise all mixed-format
combinations through the actual commands.

The broader checks below passed on the earlier PR revision before rebasing onto
origin/main at 58eb0977. The rebase preserved all four patches exactly;
rustfmt and Clippy were rerun successfully afterward. The complete aggregate
gate and the remaining broad suites have not been rerun on the current head.

CUDA, SP1, and Zisk jobs are outside this validation run. The expensive general
compiler/decompiler merge-queue partitions are separate from the standard PR
checks; the kernel parity partition is included below.

Check	Result
cargo fmt --all -- --check	Passed
cargo clippy --release --workspace --all-targets --features ix-ffi/parallel,ix-ffi/net,ix-ffi/test-ffi -- -D warnings	Passed
cargo check --release --workspace --all-targets --features ix-ffi/parallel,ix-ffi/net,ix-ffi/test-ffi	Passed
cargo nextest run --release --profile ci --workspace	Passed: 1,506 tests; 14 skipped
cargo deny check	Passed: advisories, bans, licenses, and sources; existing unmatched-advisory allowlist warnings remain
Root/benchmark/model Lean toolchain agreement	Passed
lake build IxKernelVerify IxCompileVerify	Passed
lake build --wfail IxKernelConsistency	Passed
lake run check-theory	Passed
lake run check-kernel --with-model	Passed, including certified-host audits/regressions, kernel unit tests, and the set-theory model build
lake build --wfail -v	Passed
lake lint -- --wfail -v	Passed: every target selected by CI's lint driver
lake test	Passed: complete primary test tier
lake test --wfail -- cli	Passed
lake exe ix codegen --check	Passed: all three generated Rust modules match
Compile the CI Nat.add_comm Ixon fixture	Passed: 47 constants, 39,646 serialized bytes
Kernel merge-queue parity suites	Passed: all seven selected suites, including pinned regressions and accelerated/pure comparisons
Nix package build	Passed
Packaged Ix CLI smoke test	Passed
nix flake check	Passed on x86_64-linux: packaged Lean tests, Rust Clippy, and 1,506 Rust tests
Nix development-shell build and primary tests	Passed

The documentation pass additionally passed a comment-only comparison for all
181 edited Lean files against its preceding commit, preserving the non-comment
code lines. This describes the documentation pass, not the full implementation
diff. git diff --check also passed.

The kernel parity command is:

lake test --wfail -- --ignored \
  tc-anon-diff tc-init tc-tutorial tc-roundtrip tc-ingress-meta \
  tc-pins tc-accel-diff

The central review questions are whether the source/workset witnesses identify
the actual production executions, whether fresh definitions can only use the
preceding model, and whether the exact dependency audits preserve each stated
trust boundary. These conditions determine the scope of the relative
consistency claim.