OpticalPhenomenon
plain-language theorem explainer
OpticalPhenomenon enumerates the five canonical optical effects as an inductive type with constructors for reflection, refraction, diffraction, interference and polarisation. A researcher deriving Snell's law from the J-cost functional in Recognition Science would cite this enumeration to fix the optical configuration dimension at five. The definition is a direct inductive introduction that automatically derives Fintype, enabling immediate cardinality verification in sibling theorems.
Claim. The set of optical phenomena is the finite set with elements reflection, refraction, diffraction, interference and polarisation, equipped with decidable equality.
background
In the Recognition Science treatment of optics the J-cost functional, drawn from the imported Cost module, measures deviation of a refractive ratio r from unity and vanishes exactly at r = 1. The module document states that same-medium propagation incurs zero J-cost while crossing media produces positive cost and consequent bending; five canonical phenomena are listed to match configDim D = 5. This inductive definition supplies the concrete enumeration required by the OpticsCert structure.
proof idea
The declaration is an inductive definition introducing five constructors and deriving the typeclass instances DecidableEq, Repr, BEq and Fintype automatically.
why it matters
This definition supplies the five_phenomena field of OpticsCert and the cardinality statement proved by opticalPhenomenonCount. It implements the module claim that five phenomena equal configDim D = 5, linking the J-cost mechanism for refraction to the broader RS framework where spatial dimension D = 3 is extended by optical degrees of freedom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.