TrapRegime
plain-language theorem explainer
An inductive type enumerates the five canonical optical trapping regimes distinguished by particle size relative to wavelength. Physicists modeling dipole traps, Mie scattering, or quantum optical forces would cite this classification when partitioning trap behavior. The definition is a direct inductive construction that automatically derives decidable equality and finite-type instances.
Claim. The type of optical trap regimes is the inductive type whose five constructors are the Rayleigh regime (particle diameter much smaller than wavelength), the intermediate regime, the Mie regime (particle size comparable to wavelength), the ray-optics regime (particle much larger than wavelength), and the quantum-optical regime.
background
The module introduces five canonical optical-trapping regimes corresponding to configDim D = 5. These regimes are distinguished by the ratio of particle diameter to trapping wavelength: Rayleigh for dipole scattering when the particle is much smaller than the wavelength, Mie for resonant scattering when sizes are comparable, ray optics for large particles, plus intermediate and quantum-optical cases. The classification is derived from the J-cost functional that governs recognition cost in the underlying physics.
proof idea
The declaration is an inductive definition that introduces five named constructors and derives the required typeclass instances (decidable equality, representation, boolean equality, and finite type) via the deriving clause.
why it matters
This enumeration supplies the discrete set used by the structure that certifies exactly five regimes and by the theorem that proves the finite-type cardinality equals 5 by decision. It completes the B15 depth specification of optical trap regimes in the Recognition Science framework, where the five regimes align with the five-dimensional configuration space.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.