feat: Add paper materials for AFM-style paper#14
Open
cameronfreer wants to merge 15 commits intomainfrom
Open
Conversation
Create comprehensive documentation for de Finetti theorem formalization: - 00-03: Environment, repo map, theorems, definitions - 04-07: Three proof route comparisons (Martingale, L², Koopman) - 08-09: Common ending (π-system) and infrastructure - 10-12: API examples, commit history, compiler outputs - 13-16: Snippet library, figures, bibliography, future work - README.md: Index and guide - PaperIntrospection.lean: Lean file for #check/#print outputs - commands_run.log: Session command log All files follow AFM header format with commit hash, date, and build status.
- Fix repo URL: human-oriented → cameronfreer in all file headers - Fix ConditionallyIID: document as `def` with `∃`, not `structure` - Fix ForMathlib count: 45 files → 1 file (TrimInstances.lean) - Fix lemma names throughout: - `contraction_independence` → `pair_law_eq_of_contractable` - `condExp_tail_convergence` → `condexp_convergence` - `kallenberg_correlation_bound` → `l2_contractability_bound` - `mean_ergodic_L2` → `birkhoffAverage_tendsto_metProjection` - `koopmanOp` → `koopman` - `reverse_martingale_ae_tendsto` → `reverse_martingale_subsequence_convergence` - Update code snippets to match actual implementations - Fix line numbers in lemma tables - Update infrastructure catalog with actual file locations
Create paper_draft/ directory with compilable LaTeX document: - Main document with Unicode-aware Lean code listings - 12 section files covering definitions, three proof routes, comparison - 3 appendices (axioms, snippets, reproducibility) - BibTeX bibliography with primary sources - Makefile for build automation Paper follows "One theorem, three proofs, one interface" narrative with math-first presentation per AFM guidelines. Code snippets match actual repository with proper Unicode rendering.
- Fix stats: 112 files, ~43,500 LOC (not 67/16,500) - Fix per-route stats: Martingale 14/4200, L2 13/12500, Koopman 19/7500 - Remove "and in L1" claim from martingale.tex (repo only proves a.e.) - Add caveat about tail σ-algebra equivalence in koopman.tex - Fix common-ending.tex to use correct lemma name - Change lakefile.lean to lakefile.toml in reproduce.tex - Remove placeholder email in reproduce.tex
…tion - Make clear ConditionallyIID is about existence of directing kernel ν - Tail σ-algebra construction is specific to martingale route - Fix 'hard direction' to 'key implication (contractable ⇒ conditionally i.i.d.)' - Add 'implement the same specification' to reinforce interface story
- Add coin flip running example to make directing measure concrete - Fix 'hard direction' to 'key implication (contractable ⇒ conditionally i.i.d.)' - Make 'one interface, three implementations' a distinct contribution - Clarify that ConditionallyIID is about existence of directing kernel
- Show actual theorem signatures in Lean API paragraph - Explain how the two theorems yield three-way equivalence - Add callback to coin-flip example to make directing measure concrete
- Explain that all three proofs extract ν via a limit theorem - Each proof uses a different 'asymptotic summary' of the sequence - Symmetry (contractability) provides regularity for the limit
Per AFM guidelines, note that SWHID will be provided upon publication
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
paper_materials/directory with 17 curated markdown files documenting the de Finetti formalizationPaperIntrospection.leanfor compiler #check/#print outputsContents
Statistics Captured
Recent Updates
Test Plan
PaperIntrospection.leancompiles