trapRegime_count
plain-language theorem explainer
The inductive type enumerating optical trapping regimes has cardinality five. Physicists classifying particle-light interactions by size parameter cite this count when fixing the dimension of the regime space. The proof is a single decision tactic that exhausts the five constructors of the regime type.
Claim. The set of optical trapping regimes has cardinality five: $|T| = 5$, where $T$ consists of the regimes Rayleigh, intermediate, Mie, ray optics, and quantum optical trapping.
background
The module encodes five canonical optical-trapping regimes that arise when particle size is compared to wavelength. These regimes are collected in the inductive type TrapRegime whose constructors are rayleigh, intermediate, mie, rayOptics, and quantumOptical. The local setting states that this enumeration equals configDim D = 5 and supplies the completeness datum for optical-trap certification.
proof idea
The proof is a one-line wrapper that invokes the decide tactic on the Fintype instance derived from the inductive definition of TrapRegime.
why it matters
The result populates the five_regimes field of opticalTrapCert. It completes the enumeration step in the B15 treatment of optical traps derived from J-cost. Within the Recognition framework the fixed count of five aligns with the requirement that configDim equal the number of distinct scattering regimes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.