Information and communication theory, circuits
The Lean Pool projects whose card's first MSC2020 code is in class 94, “Information and communication theory, circuits”: 5 articles, one per card.
TheoremImproved asymptotic bounds for binary and spherical codes#
Formalizes asymptotic coding bounds obtained from multilevel harmonic analysis, branching rules, and spectral decompositions. The development proves a binary-code exponent strictly below the MRRW rate, constructs a strict hierarchy of spherical-code bounds, and derives the published 0.39661 asymptotic kissing-number exponent. This import incorporates substantial proof and performance optimizations by Dean Cureton.
Quoted from the card LeanPool/projects/metric-codes.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 4 main results, each with its informal statement quoted from the card. The scan finds 4 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
MetricCodes.Johnson.main_binary_theorem(theorem; a main declaration), declared in LeanPool/MetricCodes/Conclusion.lean, line 7342: “For every relative distance strictly between zero and one half, the combined variational upper bound on the asymptotic binary-code rate is valid and is strictly smaller than the MRRW rate.”MetricCodes.Spherical.HigherHierarchy.main_general(theorem), declared in LeanPool/MetricCodes/Conclusion.lean, line 7299: “Every feasible finite interlacing certificate gives an eventual exponential upper bound for spherical codes, while the spherical-code rate is bounded by the closed hierarchy's variational rate.”MetricCodes.Spherical.HigherHierarchy.strict_hierarchy(theorem), declared in LeanPool/MetricCodes/Conclusion.lean, line 7308: “At every angle parameter strictly between zero and one, successive levels of both the global and localized hierarchies improve strictly, with the localized hierarchy also strictly improving the row and classical bounds.”MetricCodes.Spherical.HigherHierarchy.NumericalMaximum.eventually_kissingNumber_lt_published(theorem), declared in LeanPool/MetricCodes/Conclusion.lean, line 7353: “In all sufficiently large dimensions, the kissing number is at most 2 raised to 0.39661 times the dimension.”
Project
- Authors: OpenAI, Dean Cureton.
- Source: Ten Advances in Mathematics and Theoretical Computer Science by OpenAI.
- Project repository: openai/ten-proofs, at commit 94bc0feb.
- Provenance: mix, which in Lean Pool's terms means people and AI “both contributed substantially” to its Lean proofs.
- License: Apache-2.0.
- MSC2020: 94B65, 52C17, 41A60.
- In Lean Pool: LeanPool/MetricCodes, from the card LeanPool/projects/metric-codes.yaml.
Sources
TheoremMicrowave network synthesis and power-of-two DFT implementation#
Characterizes the complex transmission matrices synthesized from phase shifters and permutations, with or without hybrid couplers, using series and parallel composition. Phase-only networks are permuted phase-diagonal matrices; networks with hybrid couplers are products of permutation and phase-parametrized block-diagonal layers. Proves that the normalized DFT of every power-of-two size is implementable, with reusable finite-type reindexing, independent row and column permutations, and block-diagonal composition infrastructure. Uses the reciprocal matched network matrix model of the source paper; no general scattering-physics theorem is claimed.
Quoted from the card LeanPool/projects/microwave-networks.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 3 main results, each with its informal statement quoted from the card. The scan finds 3 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
MiLAC.PhaseShifters.implementable_iff_permutedPhaseDiagonal(theorem), declared in LeanPool/MicrowaveNetworks/PhaseShifters.lean, line 131: “A finite phase-only network is implementable exactly when its matrix is a permutation matrix times a diagonal matrix of complex phases.” Its source, as the card gives it: “Upstream PhaseShifters.lean.”MiLAC.HybridCouplersPhaseShifters.implementable_iff_layered(theorem), declared in LeanPool/MicrowaveNetworks/HybridCouplersPhaseShifters.lean, line 581: “A finite network is implementable with hybrid couplers and phase shifters exactly when its matrix is an initial permutation preceded by finitely many permutation and phase-parametrized block-diagonal layers.” Its source, as the card gives it: “Theorem 1 and Section IV of arXiv:2610.04774.”MiLAC.HybridCouplersPhaseShifters.implementable_dft(theorem; a main declaration), declared in LeanPool/MicrowaveNetworks/HybridCouplersPhaseShifters.lean, line 642: “For every natural L, the normalized DFT matrix of size 2^L can be implemented by hybrid couplers, phase shifters, and permutation networks.” Its source, as the card gives it: “Section V of arXiv:2610.04774.”
Project
- Authors: Matteo Nerini, Claude AI.
- Source: Toward a Lean Formalization of Analog Computing with Microwaves, arXiv:2610.04774.
- Project repository: matteonerini/formalizing-analog-computing, at commit a89c1e92.
- Provenance: mix, which in Lean Pool's terms means people and AI “both contributed substantially” to its Lean proofs.
- License: Apache-2.0.
- MSC2020: 94A12, 15A23, 42A38.
- In Lean Pool: LeanPool/MicrowaveNetworks, from the card LeanPool/projects/microwave-networks.yaml.
Sources
TheoremShannon Entropy Characterization#
Formalizes Shannon's finite-alphabet characterization theorem for entropy from the 1948 paper.
Quoted from the card LeanPool/projects/shannon-1948-formalization.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 5 main results, each with its informal statement quoted from the card. The scan finds 4 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
LeanPool.Shannon1948Formalization.entropyNat_unique(theorem; a main declaration), declared in LeanPool/Shannon1948Formalization/Entropy/Final.lean, line 46: “Proves that any finite-alphabet uncertainty functional satisfying Shannon's conditions equals natural-log entropy up to a positive scale.”LeanPool.Shannon1948Formalization.entropyBase_unique(theorem), declared in LeanPool/Shannon1948Formalization/Entropy/Final.lean, line 68: “Restates the characterization for any logarithm base greater than one.”LeanPool.Shannon1948Formalization.entropyNat_shannonAxioms(theorem), declared in LeanPool/Shannon1948Formalization/Entropy/Converse.lean, line 94: “Proves the converse, showing that Shannon entropy satisfies the formal condition bundle.”LeanPool.Shannon1948Formalization.chain_rule(theorem), declared in LeanPool/Shannon1948Formalization/Entropy/Joint.lean, line 127: “Proves the finite joint-entropy chain rule.”LeanPool.Shannon1948Formalization.entropyNat_joint_le_add, which the scan does not find declared in the project's files at this commit: “Proves subadditivity of finite joint entropy.”
Project
- Authors: Samuel Schlesinger.
- Source: doi:10.1002/j.1538-7305.1948.tb01338.x.
- Project repository: SamuelSchlesinger/shannon-1948-formalization.
- Provenance: mix, which in Lean Pool's terms means people and AI “both contributed substantially” to its Lean proofs.
- License: MIT, under which the project was published; Lean Pool redistributes it under Apache-2.0. Lean Pool's notice file notes: “The upstream MIT LICENSE file gives the copyright line as "Copyright (c) 2026" with no name; the repository owner of record is "SamuelSchlesinger".”
- MSC2020: 94A17, 60C05.
- In Lean Pool: LeanPool/Shannon1948Formalization, from the card LeanPool/projects/shannon-1948-formalization.yaml.
Sources
TheoremUniqueness of Shannon Capacity-Achieving Priors#
Formalizes uniqueness of the capacity-achieving input distribution for a Markov-kernel channel in three aligned layers: a finite-alphabet theorem (compactness, continuity, and strict concavity of mutual information on Mathlib's weak topology for
ProbabilityMeasure), a concrete discharged theorem for compact-Polish channels with a common strictly positive jointly continuous density, and a general measure-theoretic packaging that isolates the abstract well-conditioning hypotheses, plus a counterexample showing pairwise-distinct rows do not give an injective prior pushforward (the non-degeneracy required for uniqueness).
Quoted from the card LeanPool/projects/channel-capacity.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 3 main results, each with its informal statement quoted from the card. The scan finds 3 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
ChannelCapacity.exists_unique_capacity_achieving_prior_of_finite(theorem; a main declaration), declared in LeanPool/ChannelCapacity/Finite.lean, line 632: “For a Markov kernel between finite alphabets (nonempty input) whose rows are linearly independent (Kernel.RowMatrixFullRank), a capacity-achieving input prior exists and is unique.” Its source, as the card gives it: “R. G. Gallager, Information Theory and Reliable Communication, Wiley, 1968, Section 4.5.”ChannelCapacity.exists_unique_capacity_achieving_prior_discharged(theorem), declared in LeanPool/ChannelCapacity/Discharged.lean, line 419: “For compact-Polish channels with a common strictly positive jointly continuous density, given injectivity of the prior-pushforward map and upper semicontinuity of mutual information (the latter carried as a field ofKernel.ContinuousPositiveDensity, not derived), the capacity-achieving prior is unique.”ChannelCapacity.exists_unique_capacity_achieving_prior(theorem), declared in LeanPool/ChannelCapacity/Capacity.lean, line 78: “General measure-theoretic packaging: under abstract well-conditioning hypotheses, the capacity-achieving prior is unique.”
Project
- Authors: Adam Benenson.
- Source: Elements of Information Theory by Thomas M. Cover, Joy A. Thomas, doi:10.1002/047174882X.
- Project repository: abenenson/channel-capacity.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 94A17, 94A15, 60A10.
- In Lean Pool: LeanPool/ChannelCapacity, from the card LeanPool/projects/channel-capacity.yaml.
Sources
TheoremThe Zhang-Yeung non-Shannon information inequality#
Formalizes the Zhang-Yeung inequality, the first known non-Shannon-type entropy inequality, together with its dual and averaged forms derived through the copy lemma.
Quoted from the card LeanPool/projects/zhang-yeung-inequality.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 3 main results, each with its informal statement quoted from the card. The scan finds 3 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
ZhangYeung.zhangYeung(theorem; a main declaration), declared in LeanPool/ZhangYeungInequality/Theorem3.lean, line 218: “Proves the Zhang-Yeung non-Shannon-type information inequality for four discrete random variables.”ZhangYeung.zhangYeung_dual(theorem), declared in LeanPool/ZhangYeungInequality/Theorem3.lean, line 238: “Proves the dual form of the Zhang-Yeung inequality.”ZhangYeung.zhangYeung_averaged(theorem), declared in LeanPool/ZhangYeungInequality/Theorem3.lean, line 257: “Proves the averaged symmetric form of the Zhang-Yeung inequality.”
Project
- Authors: Christopher Boone.
- Source: doi:10.1109/18.681320.
- Project repository: cboone/zhang-yeung-inequality.
- Provenance: mix, which in Lean Pool's terms means people and AI “both contributed substantially” to its Lean proofs.
- License: Apache-2.0.
- MSC2020: 94A17, 94A15.
- In Lean Pool: LeanPool/ZhangYeungInequality, from the card LeanPool/projects/zhang-yeung-inequality.yaml.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.