AAT/SFT Research Notes

Appendix

AAT Lean Status

This page is deliberately separate from the mathematical article. It explains how to read proved Lean declarations, defined-only API, future proof obligations, tooling claims, and empirical hypotheses without merging them into one status.

Source map

The AAT mathematical text stays focused on definitions, theorem candidates, non-goals, and design boundaries. Lean status and issue progress are managed elsewhere so a public exposition cannot accidentally promote a future theorem into a proved claim.

  • Mathematical definitions `docs/aat/mathematical_theory.md` is the first-class theory text.
  • Implemented Lean API `docs/aat/lean_theorem_index.md` lists declarations, file paths, meanings, and status.
  • Future work and empirical hypotheses `docs/aat/proof_obligations.md` tracks proof obligations and empirical boundaries.

Formal claim map

The website states AAT as a theory, but only some parts are current Lean-proved claims. The status boundary is part of the exposition, not an implementation appendix.

  • Current proved core Static structural theorem packages, finite witness-count bridges, selected required-axis exactness bridges, projection / LSP bridges, graph / matrix finite-universe bridges, and representative counterexamples tracked in the theorem index.
  • Defined-only surfaces Operation schemas, extension schemas, analytic representation records, valuation records, repair and synthesis records, and tooling-facing metadata where the carrier exists but full correctness or completeness theorem packages are not universal.
  • Future proof obligations Broader semantic completeness, global filling completeness, universe-wide obstruction coverage, and stronger operation laws that require additional theorem work.
  • Empirical hypotheses Real-code extraction completeness, cost correlation, operational outcome improvement, and repository-wide calibration claims.
Status phrase Meaning in this website Reader rule
`proved theorem` A Lean theorem, lemma, or example theorem establishes the claim under its stated assumptions. Read only within the universe, coverage, exactness, and observation assumptions of that theorem.
`schema accessor theorem` Lean proves that a record or package exposes the intended field, boundary, or non-conclusion data. Do not promote this to the full correctness theorem for every instance of the schema.
`defined-only carrier` A structure, predicate, executable metric, or representation exists as a formal carrier. It supports precise statement of future theorems, but does not by itself prove the intended semantic claim.

Status vocabulary

AAT uses a small status vocabulary to avoid mixing proof, schema, tooling, and empirical claims.

  • proved A Lean declaration has been proved, including main theorems, accessors, bridge theorems, bounded completeness results, or examples.
  • defined only A Lean schema, structure, predicate, or executable metric exists, but the corresponding correctness theorem is not complete.
  • future proof obligation A mathematical claim intended for Lean proof later.
  • empirical hypothesis A claim to test against repositories, operations, datasets, or case studies; it is not a Lean proof blocker.

Tool output, extractor output, generated patches, author provenance, and unmeasured axes do not become `proved` merely by appearing in a report.

Promotion rule

AAT promotes a claim only when the artifact that states it also carries the boundary needed to read it. A theorem candidate in the mathematical text, a Lean definition, a tool report, and a proved theorem are different objects.

Claim promotion path
mathematical candidate
  -> defined Lean schema
  -> proved theorem under boundary B
  -> public claim with non-conclusions recorded

Tooling evidence can support a claim, but it does not replace the theorem boundary. Empirical validation can motivate or calibrate a hypothesis, but it is not promoted to `proved`.

Current QED boundary

The current Lean-proved core is the static structural theorem package. It connects lawfulness with required signature axes zero under explicit law-family, witness-coverage, axis exactness, universe, coverage, and observation assumptions.

Static structural core
under explicit boundary B:

ArchitectureLawful X
  <-> RequiredSignatureAxesZero (ArchitectureLawModel.signatureOf X)

ArchitectureLawful X
  <-> ArchitectureZeroCurvatureTheoremPackage X

This boundary excludes runtime metric completeness, general numerical curvature as a signature axis, empirical cost correlation, and any claim that a real-code extractor produces a complete `ComponentUniverse`.