From examples to papers, proofs, Lean, and code
Choose a topic to move from a hand calculation to definitions and related source material. Each linked work has return links to these examples. These are subject routes, not new theorem-to-Lean correspondences.
All hand-worked examples · Glossary · Browse works · Example coverage by work
Jump to: Core papers · Monographs and other works · Topics
Start from a core paper
Choose the paper you are reading. The examples introduce selected ideas. They do not cover every result or establish new Lean correspondences.
- Paper I: 1. Split and reconstruct a vector · 2. Generate a space from one seed · 3. Change coordinates · 6. Use redundant coordinates · 10. Find a kernel and its fibers · 11. Build spectral projectors · 15. Compose typed operations
- Paper II: 4. Assemble transfer blocks · 5. Refine a signal · 11. Build spectral projectors
- Paper III: 7. Detect lost information · 15. Compose typed operations
- Paper IV: 16. Split reciprocal coefficients into cyclic packets
- Paper V: 5. Refine a signal · 14. Separate averages and details
- Paper VI: 8. Average with unequal weights · 12. Eliminate a block of unknowns
- Paper VII: 17. Calculate quantum measurement and dephasing
- Paper VIII: 4. Assemble transfer blocks
- Paper IX: 9. Round a binary number · 13. Reconstruct from residues
- Paper X: 18. Follow a modular lift branch
- Paper XI: 19. Compute Frobenius in a quadratic finite field
- Paper XII: 20. Separate support from multiplicity
Start from a monograph or another work
These works have introductory examples in this guide. The coverage list also shows works still awaiting a tutorial. A source edition may contain its own worked examples.
- Proof Path Theory: 21. Choose a certificate with shared premises
- Special Functions: 24. Calculate coefficients of contracted feedback
- Machine Societies: 22. Recover the memory hidden by a summary
- Certified Inference: 26. Update a Gaussian model from one observation
- Constructive Repair: 25. Choose repair directions from a finite menu
- Information Realization: 10. Find a kernel and its fibers · 14. Separate averages and details
- Realization Boundaries: 7. Detect lost information
- Sufficient Resolution: 22. Recover the memory hidden by a summary
- Quantum and Circuits: 17. Calculate quantum measurement and dephasing
- Grounded Abstraction: 23. Find the reusable part of a calibration
- Certified Bayesian Inference: 26. Update a Gaussian model from one observation
- Gaussian Elimination: collected guide: 12. Eliminate a block of unknowns
Topics
- 1. Split and reconstruct a vector
- 2. Generate a space from one seed
- 3. Change coordinates
- 4. Assemble transfer blocks
- 5. Refine a signal
- 6. Use redundant coordinates
- 7. Detect lost information
- 8. Average with unequal weights
- 9. Round a binary number
- 10. Find a kernel and its fibers
- 11. Build spectral projectors
- 12. Eliminate a block of unknowns
- 13. Reconstruct from residues
- 14. Separate averages and details
- 15. Compose typed operations
- 16. Split reciprocal coefficients into cyclic packets
- 17. Calculate quantum measurement and dephasing
- 18. Follow a modular lift branch
- 19. Compute Frobenius in a quadratic finite field
- 20. Separate support from multiplicity
- 21. Choose a certificate with shared premises
- 22. Recover the memory hidden by a summary
- 23. Find the reusable part of a calibration
- 24. Calculate coefficients of contracted feedback
- 25. Choose repair directions from a finite menu
- 26. Update a Gaussian model from one observation
1. Split and reconstruct a vector
Terms: Projector · Packet · Complete packet family · Orthogonal projector · Direct sum
Exact packet coordinates provide the source setting for the elementary decomposition.
Paper I: Typed Operator Systems, Seed Rank, and Exact Packet Coordinates
Read · Written proofs · Lean coverage · Code and setup · Evidence
Related library guide and code examples. The guide covers related constructions and their software interfaces.
Python arithmetic check for this example: packets(). This checks the displayed rational, modular or finite-set calculations exactly.
The Lean links open each work’s recorded coverage and sources. They do not certify this tutorial. A work may have limited coverage or no linked Lean or code. Its page states what is available.
2. Generate a space from one seed
Terms: Seed · Seed rank · Cyclic vector · Span · Operator algebra
Paper I develops seed generation with its stated algebra and module hypotheses.
Paper I: Typed Operator Systems, Seed Rank, and Exact Packet Coordinates
Read · Written proofs · Lean coverage · Code and setup · Evidence
Related library guide and code examples. The guide covers related constructions and their software interfaces.
Python arithmetic check for this example: seeds(). This checks the displayed rational, modular or finite-set calculations exactly.
The Lean links open each work’s recorded coverage and sources. They do not certify this tutorial. A work may have limited coverage or no linked Lean or code. Its page states what is available.
3. Change coordinates
Terms: Coordinates · Coordinate change · Inverse · Operator conjugation · Linear isomorphism
Use Paper I for exact packet coordinates and the library atlas for general coordinate changes.
Paper I: Typed Operator Systems, Seed Rank, and Exact Packet Coordinates
Read · Written proofs · Lean coverage · Code and setup · Evidence
Related library guide and code examples. The guide covers related constructions and their software interfaces.
Python arithmetic check for this example: coordinates(). This checks the displayed rational, modular or finite-set calculations exactly.
The Lean links open each work’s recorded coverage and sources. They do not certify this tutorial. A work may have limited coverage or no linked Lean or code. Its page states what is available.
4. Assemble transfer blocks
Terms: Transfer block · Composition · Block matrix
Paper II supplies transfer background. Paper VIII develops operator algorithms and compilation.
Paper II: Refinement Towers, Weighted Transfer, and Integral Separation of Operator Packets
Read · Written proofs · Lean coverage · Code and setup · Evidence
Paper VIII: Packet Operator Algorithms, Exact Compilation, and GPU Realization
Read · Written proofs · Lean coverage · Code and setup · Evidence
Related library guide and code examples. The guide covers related constructions and their software interfaces.
Python arithmetic check for this example: transfer(). This checks the displayed rational, modular or finite-set calculations exactly.
The Lean links open each work’s recorded coverage and sources. They do not certify this tutorial. A work may have limited coverage or no linked Lean or code. Its page states what is available.
5. Refine a signal
Terms: Refinement · Coarsening · Polyphase decomposition · Residue class · Compatibility
Read Paper II for refinement and Paper V for signal and polyphase constructions.
Paper II: Refinement Towers, Weighted Transfer, and Integral Separation of Operator Packets
Read · Written proofs · Lean coverage · Code and setup · Evidence
Paper V: Polyphase Signal Calculus
Read · Written proofs · Lean coverage · Code and setup · Evidence
Related library guide and code examples. The guide covers related constructions and their software interfaces.
Python arithmetic check for this example: refinement(). This checks the displayed rational, modular or finite-set calculations exactly.
The Lean links open each work’s recorded coverage and sources. They do not certify this tutorial. A work may have limited coverage or no linked Lean or code. Its page states what is available.
6. Use redundant coordinates
Terms: Analysis and synthesis · Left inverse · Redundant coordinates · Reconstruction
Compare the exact packet setting of Paper I with the broader analysis and synthesis construction in the library guide.
Paper I: Typed Operator Systems, Seed Rank, and Exact Packet Coordinates
Read · Written proofs · Lean coverage · Code and setup · Evidence
Related library guide and code examples. The guide covers related constructions and their software interfaces.
Python arithmetic check for this example: redundant_coordinates(). This checks the displayed rational, modular or finite-set calculations exactly.
The Lean links open each work’s recorded coverage and sources. They do not certify this tutorial. A work may have limited coverage or no linked Lean or code. Its page states what is available.
7. Detect lost information
Terms: Obstruction · Fiber · Factorization through a map · Kernel · Quotient space
The finite recovery obstruction is an entry point to the works on compatibility and realization boundaries.
Paper III: Typed Transfer, Nonlinear Packets, and Obstruction Theory
Read · Written proofs · Lean coverage · Code and setup · Evidence
Realization Boundaries
Read · Written proofs · Lean coverage · Code and setup · Evidence
Related library guide and code examples. The guide covers related constructions and their software interfaces.
Python arithmetic check for this example: obstructions(). This checks the displayed rational, modular or finite-set calculations exactly.
The Lean links open each work’s recorded coverage and sources. They do not certify this tutorial. A work may have limited coverage or no linked Lean or code. Its page states what is available.
8. Average with unequal weights
Terms: Finite conditional expectation · Inner product · Orthogonal projector · Residual
Paper VI includes stochastic and Bayesian realizations. Its assumptions extend beyond this finite partition.
Paper VI: Transfer Semigroups: Stochastic, Bayesian, Fractional, and PDE Realizations
Read · Written proofs · Lean coverage · Code and setup · Evidence
Related library guide and code examples. The guide covers related constructions and their software interfaces.
Python arithmetic check for this example: weighted_averages(). This checks the displayed rational, modular or finite-set calculations exactly.
The Lean links open each work’s recorded coverage and sources. They do not certify this tutorial. A work may have limited coverage or no linked Lean or code. Its page states what is available.
9. Round a binary number
Terms: Precision · Dyadic rational · Rounding · ULP · Numerical ternary · Exact · Numerical
Paper IX supplies dyadic arithmetic background. The rounding implementation and its contracts belong to Polyphase Float.
Paper IX: Arithmetic Packets, Dyadic Towers, and Local Polynomial Deformation
Read · Written proofs · Lean coverage · Code and setup · Evidence
Related library guide and code examples. The guide covers related constructions and their software interfaces.
Python arithmetic check for this example: binary_rounding(). This checks the displayed rational, modular or finite-set calculations exactly.
The Lean links open each work’s recorded coverage and sources. They do not certify this tutorial. A work may have limited coverage or no linked Lean or code. Its page states what is available.
10. Find a kernel and its fibers
Terms: Kernel · Image · Rank · Nullity · Rank–nullity identity · Injective map · Surjective map · Quotient space · Subspace
These finite linear calculations give background for typed realizations and information loss. Read each work for its own claims.
Paper I: Typed Operator Systems, Seed Rank, and Exact Packet Coordinates
Read · Written proofs · Lean coverage · Code and setup · Evidence
Information Realization
Read · Written proofs · Lean coverage · Code and setup · Evidence
Related library guide and code examples. The guide covers related constructions and their software interfaces.
Python arithmetic check for this example: kernels(). This checks the displayed rational, modular or finite-set calculations exactly.
The Lean links open each work’s recorded coverage and sources. They do not certify this tutorial. A work may have limited coverage or no linked Lean or code. Its page states what is available.
11. Build spectral projectors
Terms: Eigenvector · Eigenvalue · Eigenspace · Diagonalizable operator · Polynomial in an operator · Minimal polynomial · Spectral projector
The example uses a diagonalizable two-dimensional matrix. The works develop wider packet and spectral constructions with additional hypotheses.
Paper I: Typed Operator Systems, Seed Rank, and Exact Packet Coordinates
Read · Written proofs · Lean coverage · Code and setup · Evidence
Paper II: Refinement Towers, Weighted Transfer, and Integral Separation of Operator Packets
Read · Written proofs · Lean coverage · Code and setup · Evidence
Related library guide and code examples. The guide covers related constructions and their software interfaces.
Python arithmetic check for this example: spectral_projectors(). This checks the displayed rational, modular or finite-set calculations exactly.
The Lean links open each work’s recorded coverage and sources. They do not certify this tutorial. A work may have limited coverage or no linked Lean or code. Its page states what is available.
12. Eliminate a block of unknowns
Terms: Block matrix · Schur complement · Elimination · Determinant · Inverse
Paper VI gives elimination background. The collected Gaussian elimination guide retains its pending source qualification and unassessed confidence.
Paper VI: Transfer Semigroups: Stochastic, Bayesian, Fractional, and PDE Realizations
Read · Written proofs · Lean coverage · Code and setup · Evidence
Gaussian Elimination: collected guide
Read · Written proofs · Lean coverage · Code and setup · Evidence
Related library guide and code examples. The guide covers related constructions and their software interfaces.
Python arithmetic check for this example: block_elimination(). This checks the displayed rational, modular or finite-set calculations exactly.
The Lean links open each work’s recorded coverage and sources. They do not certify this tutorial. A work may have limited coverage or no linked Lean or code. Its page states what is available.
13. Reconstruct from residues
Terms: Integer congruence · Coprime integers · Modular inverse · Chinese remainder theorem · Residue class
The example is ordinary integer CRT. Paper IX develops arithmetic packets and local deformation beyond this calculation.
Paper IX: Arithmetic Packets, Dyadic Towers, and Local Polynomial Deformation
Read · Written proofs · Lean coverage · Code and setup · Evidence
Related library guide and code examples. The guide covers related constructions and their software interfaces.
Python arithmetic check for this example: modular_reconstruction(). This checks the displayed rational, modular or finite-set calculations exactly.
The Lean links open each work’s recorded coverage and sources. They do not certify this tutorial. A work may have limited coverage or no linked Lean or code. Its page states what is available.
14. Separate averages and details
Terms: Haar pair · Detail coefficient · Normalization · Orthogonal matrix · Refinement
Paper V supplies signal background. Information Realization includes a finite Haar contract within its recorded formal core.
Paper V: Polyphase Signal Calculus
Read · Written proofs · Lean coverage · Code and setup · Evidence
Information Realization
Read · Written proofs · Lean coverage · Code and setup · Evidence
Related library guide and code examples. The guide covers related constructions and their software interfaces.
Python arithmetic check for this example: haar_pairs(). This checks the displayed rational, modular or finite-set calculations exactly.
The Lean links open each work’s recorded coverage and sources. They do not certify this tutorial. A work may have limited coverage or no linked Lean or code. Its page states what is available.
15. Compose typed operations
Terms: Typed system · Typed path · Operator relation · Domain and codomain · Intertwiner · Commutator
Paper I develops typed systems and their realizations. Paper III continues with typed transfer and obstructions.
Paper I: Typed Operator Systems, Seed Rank, and Exact Packet Coordinates
Read · Written proofs · Lean coverage · Code and setup · Evidence
Paper III: Typed Transfer, Nonlinear Packets, and Obstruction Theory
Read · Written proofs · Lean coverage · Code and setup · Evidence
Related library guide and code examples. The guide covers related constructions and their software interfaces.
Python arithmetic check for this example: typed_paths(). This checks the displayed rational, modular or finite-set calculations exactly.
The Lean links open each work’s recorded coverage and sources. They do not certify this tutorial. A work may have limited coverage or no linked Lean or code. Its page states what is available.
16. Split reciprocal coefficients into cyclic packets
Terms: Coefficient · Power series · Truncation · Formal reciprocal · Coefficient convolution · Root of unity
This coefficient model introduces cyclic projection and reciprocal recursion in Paper IV. Its finite product check does not address the paper’s analytic growth or spectral-zero results.
Paper IV: Cyclic Analytic Functions, Reciprocal Families, and Spectral Zero Data
Read · Written proofs · Lean coverage · Code and setup · Evidence
Source passages:
Related library guide and code examples. The guide covers related constructions and their software interfaces.
Python arithmetic check for this example: cyclic_reciprocals(). This checks the displayed rational, modular or finite-set calculations exactly.
The Lean links open each work’s recorded coverage and sources. They do not certify this tutorial. A work may have limited coverage or no linked Lean or code. Its page states what is available.
17. Calculate quantum measurement and dephasing
Terms: Complex conjugate · Adjoint matrix · Unitary matrix · Quantum amplitude · Density matrix · Matrix trace · Born probability · Purity of a density matrix · Dephasing · Kraus operators · Hermitian matrix · Positive semidefinite matrix · Coherence in a chosen basis
This introductory calculation covers one two-dimensional state, a unitary phase change and a measurement channel. Paper VII develops the finite quantum setting and separate continuum research targets. Quantum and Circuits provides a related route through arithmetic realizations and symmetry; the extended demonstration also reproduces its modulus-12 phase example. These subject routes add no formal claim correspondence.
Paper VII: Quantum Seed Calculus
Read · Written proofs · Lean coverage · Code and setup · Evidence
Quantum and Circuits
Read · Written proofs · Lean coverage · Code and setup · Evidence
Source passages:
Related library guide and code examples. The guide covers related constructions and their software interfaces.
Python arithmetic check for this example: quantum_measurement(). This checks the displayed rational, modular or finite-set calculations exactly.
The Lean links open each work’s recorded coverage and sources. They do not certify this tutorial. A work may have limited coverage or no linked Lean or code. Its page states what is available.
18. Follow a modular lift branch
Terms: Prime power · Modular reduction · Lift branch · Compatible tower · p-adic integer · Survival to a finite level
Finite lift branches give elementary background for Paper X’s residual constructions. Its completion result requires supplied all-depth data, closure and the other stated inputs.
Paper X: Universal Residual Seeds and Conditional Occupied-System Completion
Read · Written proofs · Lean coverage · Code and setup · Evidence
Source passages:
Related library guide and code examples. The guide covers related constructions and their software interfaces.
Python arithmetic check for this example: lift_branches(). This checks the displayed rational, modular or finite-set calculations exactly.
The Lean links open each work’s recorded coverage and sources. They do not certify this tutorial. A work may have limited coverage or no linked Lean or code. Its page states what is available.
19. Compute Frobenius in a quadratic finite field
Terms: Prime field · Extension field · Finite-field Frobenius · Field trace · Field norm · Irreducible polynomial
This is finite-field background for Paper XI’s finite packet theory. Conjecture 66 separately asks for an actual arithmetic realizer with its declared comparison data.
Paper XI: Packets, Arithmetic Realization, and Conditional Comparison
Read · Written proofs · Lean coverage · Code and setup · Evidence
Source passages:
Related library guide and code examples. The guide covers related constructions and their software interfaces.
Python arithmetic check for this example: finite_frobenius(). This checks the displayed rational, modular or finite-set calculations exactly.
The Lean links open each work’s recorded coverage and sources. They do not certify this tutorial. A work may have limited coverage or no linked Lean or code. Its page states what is available.
20. Separate support from multiplicity
Terms: Commutative ring with identity · Module · Module presentation · Cokernel · Nilpotent operator · Module annihilator · Module support · Zeroth Fitting ideal · Multiplicity in the module example · Ideal · Prime ideal · Localization at a prime
Paper XII distinguishes module support from packet and arithmetic constructions. This example compares two explicitly supplied modules. Patching, classicality and the other arithmetic inputs remain separate.
Paper XII: Patching Support, Hecke Packets, and Conditional Automorphic Completion
Read · Written proofs · Lean coverage · Code and setup · Evidence
Source passages:
Related library guide and code examples. The guide covers related constructions and their software interfaces.
Python arithmetic check for this example: support_multiplicity(). This checks the displayed rational, modular or finite-set calculations exactly.
The Lean links open each work’s recorded coverage and sources. They do not certify this tutorial. A work may have limited coverage or no linked Lean or code. Its page states what is available.
21. Choose a certificate with shared premises
Terms: Finite proof field · Admissible leaf · Recorded inference rule · Verification closure · Inclusion-minimal certificate · Least certificate · Minimum-cost certificate
This example compares certificates in a supplied finite rule system. It illustrates verification closure and cost selection in Proof Path Theory. It does not certify arbitrary inference rules or Python implementations.
Proof Path Theory
Read · Written proofs · Lean coverage · Code and setup · Evidence
Source passages:
- Proof Path Theory: certificates and verification closure
- Proof Path Theory: alternative derivations and costs
Edition guide and reproduction instructions. Use each work’s Code and setup link for its implementation. The arithmetic check below covers this tutorial separately.
Python arithmetic check for this example: proof_certificates(). This checks the displayed rational, modular or finite-set calculations exactly.
The Lean links open each work’s recorded coverage and sources. They do not certify this tutorial. A work may have limited coverage or no linked Lean or code. Its page states what is available.
22. Recover the memory hidden by a summary
Terms: Visible state · Hidden state · Prepared hidden initialization · Discrete memory maps · Autonomous dynamics of a summary · State augmentation · Semigroup law for evolution maps
This two-coordinate model illustrates prepared evolution and hidden-memory return in Sufficient Resolution, and the deterministic quotient criterion in Machine Societies. The works’ broader assumptions and review records remain separate.
Sufficient Resolution
Read · Written proofs · Lean coverage · Code and setup · Evidence
Machine Societies
Read · Written proofs · Lean coverage · Code and setup · Evidence
Source passages:
- Sufficient Resolution: exact hidden elimination and closure
- Machine Societies: deterministic quotient criterion
Edition guide and reproduction instructions. Use each work’s Code and setup link for its implementation. The arithmetic check below covers this tutorial separately.
Python arithmetic check for this example: hidden_memory(). This checks the displayed rational, modular or finite-set calculations exactly.
The Lean links open each work’s recorded coverage and sources. They do not certify this tutorial. A work may have limited coverage or no linked Lean or code. Its page states what is available.
23. Find the reusable part of a calibration
Terms: Exact operator calibration · Calibration span · Compatible model · Linear extension · Reusable calibrated core · Identifiability relative to a model class
Grounded Abstraction supplies the three-coordinate calibration used here. The reusable domain is computed for exact full-state output and the unrestricted class of compatible linear extensions.
Grounded Abstraction
Read · Written proofs · Lean coverage · Code and setup · Evidence
Source passages:
- Grounded Abstraction: the calibrated continuation domain
- Grounded Abstraction: the three-coordinate example
Edition guide and reproduction instructions. Use each work’s Code and setup link for its implementation. The arithmetic check below covers this tutorial separately.
Python arithmetic check for this example: calibrated_continuation(). This checks the displayed rational, modular or finite-set calculations exactly.
The Lean links open each work’s recorded coverage and sources. They do not certify this tutorial. A work may have limited coverage or no linked Lean or code. Its page states what is available.
24. Calculate coefficients of contracted feedback
Terms: Derivative in the series example · Differential equation · Initial condition · Contracted argument · Coefficient recurrence
This example expands the defining coefficient recurrence for a member of Special Functions. Finite coefficient checks do not replace the monograph’s analytic existence, growth or separation arguments.
Special Functions
Read · Written proofs · Lean coverage · Code and setup · Evidence
Source passages:
Edition guide and reproduction instructions. Use each work’s Code and setup link for its implementation. The arithmetic check below covers this tutorial separately.
Python arithmetic check for this example: contracted_feedback(). This checks the displayed rational, modular or finite-set calculations exactly.
The Lean links open each work’s recorded coverage and sources. They do not certify this tutorial. A work may have limited coverage or no linked Lean or code. Its page states what is available.
25. Choose repair directions from a finite menu
Terms: Repair direction · Free linear repair · Finite repair menu · Repair selection cost · Feasibility · Linear obstruction witness
The example uses rational linear repair with supplied menu costs. It distinguishes feasibility, optimal selection and rejection of a proposed certificate. Python checks and Lean acceptance retain their separate recorded meanings.
Constructive Repair
Read · Written proofs · Lean coverage · Code and setup · Evidence
Source passages:
Edition guide and reproduction instructions. Use each work’s Code and setup link for its implementation. The arithmetic check below covers this tutorial separately.
Python arithmetic check for this example: repair_menus(). This checks the displayed rational, modular or finite-set calculations exactly.
The Lean links open each work’s recorded coverage and sources. They do not certify this tutorial. A work may have limited coverage or no linked Lean or code. Its page states what is available.
26. Update a Gaussian model from one observation
Terms: Finite-dimensional Gaussian model · Prior distribution · Likelihood · Posterior distribution · Covariance matrix · Precision matrix · Observation innovation · Exact Gaussian gain · Joseph covariance
These calculations explain the exact Gaussian model and a candidate Joseph covariance. The release’s law-error tolerance, interval output and emitted Lean-instance checks require their full contracts.
Certified Inference
Read · Written proofs · Lean coverage · Code and setup · Evidence
Certified Bayesian Inference
Read · Written proofs · Lean coverage · Code and setup · Evidence
Source passages:
- Certified Bayesian Inference: Gaussian model and posterior formulas
- Certified Inference: execution and evidence contract
Edition guide and reproduction instructions. Use each work’s Code and setup link for its implementation. The arithmetic check below covers this tutorial separately.
Python arithmetic check for this example: gaussian_update(). This checks the displayed rational, modular or finite-set calculations exactly.
The Lean links open each work’s recorded coverage and sources. They do not certify this tutorial. A work may have limited coverage or no linked Lean or code. Its page states what is available.