OpticalTrapCert
plain-language theorem explainer
The OpticalTrapCert structure certifies that the set of optical trap regimes has cardinality exactly five. Optical physicists and Recognition Science modelers cite it to fix configuration dimension at five when classifying particle-light interactions. It is introduced as a structure definition whose single field is discharged by the Fintype instance on the five-constructor inductive type.
Claim. The structure certifying that the set of optical trap regimes has cardinality five, where the regimes are the five cases Rayleigh (particle ≪ λ), intermediate, Mie (particle ~ λ), ray optics (particle ≫ λ), and quantum optical trap.
background
The module defines an inductive type TrapRegime with exactly five constructors: rayleigh, intermediate, mie, rayOptics, quantumOptical, each corresponding to a distinct size regime relative to wavelength. This enumeration is presented as the canonical set for optical trapping and is tied to configuration dimension D = 5 in the Recognition Science setting. The structure OpticalTrapCert simply records the cardinality assertion for this finite set.
proof idea
This is a structure definition that introduces a record type with one field requiring Fintype.card TrapRegime = 5. No tactics or lemmas are applied inside the declaration itself; the field is populated by the downstream definition opticalTrapCert via the trapRegime_count value.
why it matters
The structure supplies the cardinality certificate consumed by the downstream opticalTrapCert definition. It implements the five-regime enumeration stated in the module header for B15 depth analysis and aligns with the framework's use of configDim D = 5 for optical traps, separate from spatial dimension D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.