satchlj/natural-latents-lean
Watch
1
0
Fork
You've already forked natural-latents-lean
 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
No description
2 commits 1 branch 0 tags 68 KiB
  • Lean 100%
Find a file
Exact
Repository files (latest commit first)
Filename Latest commit message Latest commit date
Satya Benson e7bc5a5b9a
Some checks failed
Lean Action CI / build (push) Has been cancelled
Details
Docs: drop local filesystem paths 
Refer to the thesis drafts by name instead of by their path on the
author's machine.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
2026-10-05 15:31:52 -04:00
.github/workflows Initial commit: Natural Latents Lean formalization 2026-10-01 12:33:55 -04:00
docs Docs: drop local filesystem paths 2026-10-05 15:31:52 -04:00
NaturalLatents Initial commit: Natural Latents Lean formalization 2026-10-01 12:33:55 -04:00
.gitignore Initial commit: Natural Latents Lean formalization 2026-10-01 12:33:55 -04:00
FORMALIZATION_TODO.md Docs: drop local filesystem paths 2026-10-05 15:31:52 -04:00
lake-manifest.json Initial commit: Natural Latents Lean formalization 2026-10-01 12:33:55 -04:00
lakefile.toml Initial commit: Natural Latents Lean formalization 2026-10-01 12:33:55 -04:00
lean-toolchain Initial commit: Natural Latents Lean formalization 2026-10-01 12:33:55 -04:00
LICENSE Initial commit: Natural Latents Lean formalization 2026-10-01 12:33:55 -04:00
NaturalLatents.lean Initial commit: Natural Latents Lean formalization 2026-10-01 12:33:55 -04:00
README.md Initial commit: Natural Latents Lean formalization 2026-10-01 12:33:55 -04:00

README.md

NaturalLatents

Lean 4 project for formalizing information-theoretic natural latents.

The project is pinned to Lean 4.31.0 and Mathlib 4.31.0 through lean-toolchain and lakefile.toml. It also depends on teorth/pfr at tag v4.31.0 for the finite entropy API used by the current formalization.

Build

Install Elan, then run:

lake build

If Elan is installed but not on your shell PATH, the direct binary also works:

~/.elan/bin/lake build

The project currently builds with no sorry, admit, or local axioms.

Survey Notes

The current Mathlib survey is in docs/mathlib-information-theory-gap-analysis.md.

Short version: Mathlib has strong measure-theoretic KL divergence and conditional-independence infrastructure, plus set partitions and Bell numbers. It does not yet appear to have the finite Shannon layer needed for the thesis: entropy, conditional entropy, mutual information, conditional mutual information, total correlation, and conditional total correlation.

The project currently uses PFR's ForMathlib entropy layer as that finite discrete Shannon API. The separator-determines-redund theorem and the exact common-information order results are formalized on top of it.

Formalization Notes

  • NaturalLatents.Information contains the reusable observable-vector, total-correlation, separator, redund, natural-latent, stochastic-kernel, packaged finite-latent, coarsening, objective/class, and exact information-order API.
  • NaturalLatents.SeparatorDeterminesRedund contains the zero/approximate separator-to-redund entropy theorem.
  • NaturalLatents.CommonInformation contains exact information-order, containment-bottom, leave-one-out core, and Theorem C helper results.
  • NaturalLatents.Translation contains the named guaranteed-translatability theorem layer, the two-coordinate converse, and the immediate natural-latent translation corollaries.
  • NaturalLatents.MathlibInformationTheorySurvey records the relevant Mathlib imports and smoke tests.
  • FORMALIZATION_TODO.md is the durable status-tracked formalization checklist for the universal-abstractions draft.
  • docs/outstanding-formalization.md tracks the remaining theorem and API work against the current thesis draft.