Teaching Light
Where to Go

Two named Lean declarations, bound to one pinned source snapshot. The first turns a sphere integral into three lines of algebra: equal coordinate averages that sum to one give  〈sin²θ〉 = 2/3. The second proves the defined Dicke delay ln N over N·γ₀ strictly decreases from N ≥ 3.

The surrounding source map, browser calculations, model assumptions, and publication bibliography are shown as separate evidence layers.

Formal model consequences are not experimental validation. Structural inventory is not a whole-corpus proof result.

Three lines instead of an integral

The textbook route to 〈sin²θ〉 = 2/3 integrates over the unit sphere. The pinned source takes the shorter path: assume the three coordinate averages are equal, assume they sum to one, and the conclusion is arithmetic. The source does not formalize the sphere integral itself; it proves the algebraic consequence of the stated symmetry.

Two thirds, from symmetry alone

The pinned declaration accepts three real-valued averages. If all three are equal and their sum is one, the first two sum to 2/3. The theorem does not construct a probability measure on the sphere, prove rotational invariance, or show that a physical emitter population satisfies those hypotheses.

This is the complete public scope of the receipt: a named conditional equality, not a formalization of spherical integration or an empirical orientation measurement.

Adding emitters shortens the defined delay

The source defines superradiantDelay N gamma0as ln(N)/(N·gamma0). For natural numbers 3 ≤ N₁ < N₂ and a positive gamma0, the named declaration proves the defined expression is smaller at N₂. The mechanism is analytic: ln(x)/x decreases past e, and the hypothesis N₁ ≥ 3 clears it.

the defined expression superradiantDelay N 1 for 3 ≤ N ≤ 48, evaluated for illustration; not one of the two named receipts

The receipt does not establish that a material realizes the Dicke model, that gamma0 is measured correctly, that larger physical domains produce a faster burst, or that the manifest's named runtime handler implements this definition.

A formal implication is not a physical discovery

The pinned tree includes conjecture modules that combine chosen orientation, rate, and directionality formulas. Lean can check an implication once those definitions and hypotheses are supplied. That does not establish novelty, validate the formulas for a sample, or show that separately measured effects compose in an experiment.

Eisler/Conjectures/DirectionalSuperfluorescence.lean · conditional source model; no named receipt on this page

A chosen product score, not an efficiency or design rule

One source model defines the product below. Multiplying selected input values is arithmetic; neither the choice of factors nor their independence is established by the two named receipts. The score must not be read as a measured device efficiency, an optimization result, or a recommendation.

Illustrative dimensionless inputs; not measurement evidence.

Eisler/Conjectures/OptimalDesign.lean · chosen model and conditional lemmas; no empirical receipt

Fresnel reflectance, evaluated in your browser

The widget below evaluates a TypeScript implementation of the Fresnel equations for user-selected refractive indices and incidence angle. It is not generated from Lean, is not covered by either named receipt, and does not validate the preset refractive indices for a particular material, wavelength, interface, or experiment.

apps/hub/app/_waddles/eisler/components/FresnelWidget.tsx · browser implementation; not a Lean receipt

Bibliography, not proof coverage

These external publication links provide scientific context. Their presence does not mean this repository formalizes every argument, reproduces any experiment, or verifies any reported measurement.

Exact bindings and explicit non-claims

The source repository is private; public clone and independent build commands are not currently available.

Reading is free. Patronage is not open.

This page, both receipts, and the structural proof explorer are public. Patronage checkout is closed on this deployment: the endpoint answers FEATURE_NOT_CONFIGURED, and that refusal is covered by a route test. If access changes, the status page changes first.

Live access status →

Names, hypotheses, and evidence
stay in their own lane.

For Carissa, who taught light where to go.

Tim