labreports.app

Lab report · Perovskite quantum light

Coherence and Relaxation Specify Photon Indistinguishability

Interface-regulated perovskite nanocrystals provide measurable coherence and relaxation states for specifying quantum-light emission. This report isolates two quantitative constraints from Yitong Dong's CU seminar and supporting literature, then follows their combination into a source-supported model of photon indistinguishability.

Open lean-perovskite Read Basic.lean Engineering statement Source trail
\[ C=\frac{T_2}{2T_1} \qquad L=\frac{\Gamma_{\mathrm{relaxation}}}{\Gamma_{\mathrm{relaxation}}+\Gamma_X} \qquad I=CL \]

Specification 01

Coherence

Radiative recombination time \(T_1\) and coherence time \(T_2\) specify normalized coherence \(C\). The transform limit gives the endpoint \(C=1\).

Figure A showing a perovskite nanocrystal emitter, the normalized coherence ratio C equals T2 divided by twice T1, and the transform-limit relation T2 equals twice T1 giving C equals one.
Figure A. Coherence specifies the transform limit for single-photon emission from a perovskite nanocrystal emitter.

Specification 02

Stochastic relaxation

Stochastic relaxation introduces emission-time jitter. The factor \(L\) specifies a relaxation-limited constraint associated with Hong-Ou-Mandel two-photon interference visibility.

Figure B showing stochastic relaxation in a photoexcited perovskite nanocrystal, the relaxation factor L, and a Hong-Ou-Mandel beam-splitter measurement with visibility bounded by L.
Figure B. Stochastic relaxation specifies a limit on photon indistinguishability through timing jitter.

Specification 03

Combined indistinguishability

A source-supported quantum-dot model combines the coherence and stochastic-relaxation factors multiplicatively as \(I=CL\).

Figure C combining coherence and relaxation into I equals C times L and listing the constraints verified in Lean version 0.3.
Figure C. The combined specification and its machine-checked consequences.
Lean-verified consequences

Given the positive timing and rate quantities and the stated coherence and combined-model specifications, Lean verifies:

\( \displaystyle 0 < I < 1,\qquad I < C,\qquad I \le L. \)

The transform-limit equivalence

\( \displaystyle C = 1 \iff T_2 = 2T_1 \)

and the related relaxation result

\( \displaystyle 0 \le V_{\mathrm{HOM}} \le L \)

remain explicit parts of the formalization.

What is Lean?

Lean is a proof assistant. In this repo, scientific relationships are written as explicit specifications and Lean checks whether the stated mathematical consequences follow.

Engineering reading

Within the combined model, improving coherence alone leaves indistinguishability constrained by the relaxation factor, while improving the relaxation factor alone leaves it constrained by coherence.

Repository development

From result to next specification

The current repo turns seminar and paper relationships into a small, inspectable specification space for subsequent measurements and models.

01Seminar + papers
02Measured relationships
03Lean specifications
04Verified consequences
05Next specifications

Interface → coherence

Admit measured interface properties that specify quantitative constraints on \(T_2\) or \(C\).

Interface → relaxation

Admit interface or relaxation measurements that specify \(\Gamma_{\mathrm{relaxation}}\), \(\Gamma_X\), or \(L\).

Measurements → combined model

Test source-supported refinements that specify photon indistinguishability more tightly than the present component bounds.

Emitter
 ├─ T1
 ├─ T2
 └─ coherenceRatio

RelaxationSpec
 ├─ Γrelaxation
 ├─ ΓX
 └─ relaxationLimit

Combined model
 └─ I = C L

Verified
 ├─ 0 < C ≤ 1
 ├─ 0 < L < 1
 ├─ 0 < I < 1
 ├─ I < C
 └─ I ≤ L

Current artifact

lean-perovskite

A compact Lean project for formalizing and testing quantitative specifications for perovskite quantum light emission.

Repository Basic.lean v0.3
Reading Point

Measurements specify physical states. Models specify relationships. Lean checks consequences of those stated relationships.