The mathematics underlying 13 publications at the intersection of materials chemistry and nanophotonics. 171 machine-checked theorems. 2 open goals remaining.
On the mathematics underlying perovskite nanocrystal photonics — orientation, cooperative emission, and spectrum splitting.
I put your papers into a theorem prover and made a computer check every step of the math — from how a polyhedral reflector sorts sunlight across seven subcells, to how the color, polarization, and direction of light can be tuned by the structure of a nanocrystal, to how a thousand emitters synchronize their dipoles into a single coherent pulse. Along the way, the formalization revealed a few things.
Every paper on dipole orientation compares to Θ = 2/3. The standard derivation integrates sin²θ over the sphere. But it follows from symmetry alone:
Three lines. No integration. Generalizes to ddimensions: Θ = (d − 1)/d.
Nanoplatelets outperform nanocubes. Two independent mechanisms, both increasing with aspect ratio:
AR is the onlyparameter that improves both intrinsic orientation and alignment simultaneously. There is no tradeoff — aspect ratio is a free lunch.
Eisler/Conjectures/OrientationOptimization.lean · 26 theorems
Dicke superradiance gives a peak emission rate that scales as N², not N. The standard claim assumes the symmetric Dicke state. The formalization proves something stronger:
Γ(J, M) ≤ γ0· (N/2)(N/2 + 1) on the physical Dicke ladder
It's a proved upper bound, not an assumption. And the buildup time τD = ln(N)/(N·γ0) is strictly decreasing for N ≥ 3. Bigger domains give both more intensity and faster onset. Named and proved:
Key step uses Mathlib's MonotonOn.strictMono for the ln(N)/N decay above e.
Transition dipole orientation and Dicke superradiance had been studied independently for decades. The formalization proves: for N ≥ 3 emitters with Θ > 2/3, directed superradiant power always exceeds isotropic independent power.
Θ · γ0· N(N+2)/4 > (2/3) · N · γ0
At the measured Jurow 2019 value Θ = 0.89 — i.e. 〈sin²θ〉 = 0.89, meaning 89% of the dipole power sits in the in-plane component. The far-field forward/backward ratio additionally depends on substrate index and outcoupling geometry (Brütting 2013) and is not claimed here.
Two independently demonstrated effects — orientation (Θ) and cooperative emission (N²) — compose multiplicatively. The directed superradiant dominance theorem proves they never cancel.
Eisler/Conjectures/DirectionalSuperfluorescence.lean · 6 theorems
A first-order product score that captures the direction of improvement across solar cells, LEDs, and directed quantum sources when the three factors are held approximately independent. This is not a derived thermodynamic bound — it is a useful design-space gradient:
Dimensionless score, not an efficiency. Linewidth held at reference.
Under the product FoM, improving Θ from 0.89 → 1.0 yields ΔFoM = 0.95·0.11 = 0.1045; improving PLQY from 0.95 → 1.0 yields 0.05·0.89 = 0.0445. Ratio 2.35×— orientation is the bigger lever under this heuristic. Even with worst-case 5% PLQY loss from the shape change, the net FoM still increases. Orientation is the bigger lever.
Eisler/Conjectures/OptimalDesign.lean · 15 theorems
The SQ bound is a rigorous thermodynamic result for a single junction illuminated by a blackbody spectrum under detailed balance — it is not a bound on solar conversion in general. Relax the single-junction assumption and the bound lifts. The polyhedral specular reflector sorts photons by energy onto seven subcells; the paper reports:
The blackbody flux above any bandgap is proved strictly decreasing in Eg. The proof: the Wien function f(x) = (x² + 2x + 2)·e−x loses to exponential decay because 1 + h + h²/2 ≤ eh. Foundation for Stokes shift concentration.
Every photon that enters the module must first cross a dielectric interface. The loss is set by Fresnel—drag the sliders and watch Rs, Rp, and the unpolarized average evolve. Brewster's angle is the zero of the p-curve.
Eisler/Thermodynamics/ · 29 theorems
5 files
4 files
5 files
3 files
2 files
2 files
8 files
Kernel-checked. propext, Quot.sound, Classical.choice. Nothing else.
200K+ theorems of community-maintained formalized mathematics.
2 sorry. 0 axioms. 3 physical hypotheses, documented.
For Carissa — who taught light where to go.
— Tim