scottnarmstrong/leanautoformalizationskills/lean-statement-audit

Audit an exact frozen Lean declaration

The audit target is the actual frozen Lean declaration. A Markdown note, “contract,” candidate, probe, helper, alias, facade, or similarly named theorem is never a substitute.

For a theorem, proving B → A is not proving source statement A, even if B is proved elsewhere. For a definition, constructing some inhabitant of the right codomain is not defining the source object. Both errors move mathematics out of the declaration while leaving Lean code that compiles.

Only proofs may be provisional

Before author approval or manifestation, every theorem type and every definition type/body must be the exact final source-facing declaration. Pre-approval elaboration may use an untracked temporary file containing that exact command; delete it after use. Tracked candidates and proposed Lean surfaces have no audit status.

Only the proof body of an exact author-approved keystone theorem may be the manifest-bound by sorry with state DRAFT_SORRY. This is the normal statement-freezing stage, not a proof shortcut. Its statement is already final. It is FROZEN_UNPROVED, unavailable, non-importable by production/provider code, and not proof progress. Definitions neither contain nor depend on this exception. Its registered provider module/export is also quarantined from every consumer except the provider itself and the frozen anchor until sealing and audit, so implementation code cannot bypass the frozen export.

Pin the exact target

Before reading implementation code, pin from the project manifest:

• versioned anchor ID;
• frozen path and fully qualified export;
• declaration kind and state;
• source revision, hash, and exact ranges;
• frozen declaration bytes/hashes;
• provider path/export for a theorem; and
• any author rulings and paired characterization export required by the

repository workflow.

Recompute the mechanical values and stop on any mismatch. Every Lean file in the frozen tree must have exactly one manifest owner. A graph node must name this exact manifest entry and export.

Source transcriptions and audit reports are evidence only. They cannot override the manuscript, adopted errata/rulings, or the exact author-approved Lean code. A wrong declaration requires an author-approved versioned successor and invalidation of dependent graph/audit evidence; never repair it in place.

Reconstruct the mathematics independently

Read the raw source statement or definition and approved errata/rulings, not its proof, old Lean code, or a prior audit summary. Record:

• all source premises;
• outer-to-inner quantifier order;
• exact conclusion or definiens/characteristic property;
• constant and witness scope;
• carrier, domain, normalization, notation, and endpoint conventions; and
• any author-approved split or domain-strengthening decision.

The source reviewer must be independent of the declaration author. Convenience hypotheses, specializations, weaker conclusions, fallback values, and proof obligations are not errata.

Theorem audit: five-bin binder test

Enumerate every explicit, implicit, and instance binder. Recursively expand project-owned assumption, witness, gate, structure, typeclass, and Prop aliases so one bundle cannot hide many premises. Classify every logical input into exactly one bin:

Any EXCESS is an automatic failure. A producer does not change its bin: apply the producer in the proof and remove the binder. A source proof step is still a proof step, not a theorem premise.

Also compare binder names/information/types, order, dependency, implicitness, universal/existential scope, conclusion carrier, normalization, exponent, window, and constant dependence. “C depends only on d” is enforced by quantifier order, not prose.

The report must contain one row per expanded binder with a source/ruling citation and counts for every bin. No table means no passing theorem audit.

Definition audit: body and source characterization

First classify how the manuscript defines the object.

Literal definition

If the source gives a formula or predicate, audit the complete Lean body against that formula on the entire declared carrier. A genuine manuscript-defined predicate may be a literal def : Prop. A theorem-shaped predicate, assumption package, result bundle, or generic “input/bridge/consequence” proposition fails.

Characterization-defined object

If the source defines an object as the unique object satisfying Φ, the definition is eligible only after:

1. the exact well-definedness theorem ∃! x, Φ x has been frozen, proved, and

independently audited on the real source carriers;

1. the definition is constructed from that proved result, or from an already

proved equivalent construction; and

1. a separately named, sorry-free theorem proves the complete source

characterization and uniqueness for the exported definition.

Apply the theorem five-bin test to the well-definedness theorem itself. Existence of response objects, integrability, linearity, quadraticity, symmetry, representability, and other proof steps are EXCESS if assumed rather than proved, unless the source explicitly states them as premises. Classical.choose from the proved ∃! is legitimate; a choice from mere existence or a non-unique family fails.

Audit the definition and characterization theorem as one semantic unit, even when each occupies its own one-declaration file. Both must be manifested and versioned together and landed in the same commit. Every downstream proof/graph use must depend on the characterization theorem, not merely on the definition's result type.

Automatically fail a definition that uses or hides any of the following to paper over missing mathematics:

• an if/dite/zero/default branch outside the source domain;
• a valid-locus-only theorem for a globally exported object;
• an arbitrary non-unique witness or selected family whose independence is

deferred;

• an over-broad carrier with invented off-source semantics;
• a reconstruction or polarization whose equivalence to Φ is not already

proved; or

• prose saying a later theorem will make the present definition faithful.

For any classical choice, identify the exact proved existence/uniqueness theorem and verify choice independence through uniqueness. Check every source-defining property—symmetry, normalization, locality, all-loadings identity, or analogous structure—rather than accepting the codomain as a surrogate.

A definition verdict has separate lines:

BODY_MATCH: OK|FAIL PUBLIC_CARRIER: OK|FAIL WELL_DEFINEDNESS: OK|FAIL|N/A_LITERAL CHARACTERIZATION: OK|FAIL|N/A_LITERAL CHOICE_INDEPENDENCE: OK|FAIL|N/A DEFINITION_VERDICT: PASS|FAIL

Any failure is non-waivable. Compilation and a matching whole-file hash prove only identity/elaboration, never mathematical meaning.

Check semantic closure and exact use

Inspect every project-owned definition appearing in the declaration's type or body, including notation, reducible aliases, structures, typeclasses, bundled predicates, and coercions. Audit its body or bind it to an already audited version. A meaning-carrying definition change is a declaration change even if pretty-printed theorem text is unchanged.

Use transient, reproducibly generated Lean checks—never tracked candidate files:

• for a theorem, an example at the independently reconstructed exact type whose

body is exact Frozen.export;

• for a literal definition, checks of its elaborated type and defining

equations;

• for a characterized definition, exact applications of its full

characterization and uniqueness theorem; and

• at each conditional application, a term-level composition witness supplying

every source premise from actual dependencies.

Delete temporary files after recording commands and output. Name reachability, imports, graph edges, and file existence do not demonstrate term-level consumption.

Seal and axiom checks

For a sealed theorem, verify that the only frozen-file change from its approved DRAFT_SORRY baseline is the proof body, now a short assembly such as by exact Provider.result. Compile the frozen export and inspect #print axioms. Unauthorized sorryAx, project axiom, or constant is fatal. Apply any explicitly approved trust boundary exactly as local rules specify.

For definitions and their characterization theorems, require sorry-free axiom closure before they are admitted as a semantic unit.

Fail-fast procedure

1. Pin manifest identity, source, exact declaration bytes, state, and rulings.
2. Reconstruct the source mathematics independently.
3. Verify the frozen path/export/kind/bytes before inspecting helpers.
4. If a theorem is DRAFT_SORRY, verify its one allowed proof hole, record

FROZEN_UNPROVED, and stop proof promotion.

1. For a theorem, emit the five-bin table; fail immediately on EXCESS.
2. For a definition, run the body/carrier/characterization audit; fail on any

fallback, deferred semantics, missing proved well-definedness, or raw-codomain substitution.

1. Compile transient exact-type/characterization checks.
2. Verify source carriers, normalizations, scopes, and project watch items.
3. For sealed results, verify proof-body-only sealing and axiom cleanliness.
4. Compile producer-to-consumer composition for every closure claim.

For a draft anchor, emit these separate verdicts before stopping:

DECLARATION_FIDELITY: PASS|FAIL
DRAFT_ALLOWLIST: PASS|FAIL
PROOF_STATUS: FROZEN_UNPROVED

A draft may pass declaration fidelity. It never passes theorem closure or axiom closure.

A root cannot pass with inhabit=N/A, consume=N/A, “conditional assembly,” or “characterization later.”

Honest statuses and durable regressions

• FROZEN_UNPROVED: exact DRAFT theorem; unavailable.
• PROVED: exact sealed declaration, passing source/semantic and axiom audits.
• approved relative/trust status: exact declaration passes, with the named

authorized input reported visibly.

• CONDITIONAL: internal helper with extra produced premises.
• SHELL: internal helper with unproduced premises.
• CLAIMED/PARTIAL: evidence is incomplete.

Only the exact frozen export can make its source node PROVED. Keep negative regression fixtures that must fail:

1. a theorem with the right conclusion and 65 extra explicit hypotheses;
2. the same 65 obligations hidden in a project-owned bundle or Prop alias;
3. a definition returning the right codomain via a zero/default fallback; and
4. a definition whose audit admits that its source characterization will be

proved later.

An audit process that passes any fixture cannot certify a project.