opticalPhenomenonCount
plain-language theorem explainer
Exactly five optical phenomena are enumerated in the Recognition Science treatment of optics. A physicist deriving refraction from the J-cost functional would reference this cardinality to fix the configuration dimension at five. The proof reduces to a decision procedure that counts the constructors in the finite inductive enumeration of the phenomena.
Claim. The set consisting of reflection, refraction, diffraction, interference, and polarisation has five elements.
background
The module derives Snell's law from the Recognition Science J-cost, where the refraction ratio corresponds to a positive J-value between different media and zero within the same medium. Optical phenomena are introduced via an inductive type that enumerates five cases: reflection, refraction, diffraction, interference, and polarisation. This enumeration supplies the count used to certify the optics section, consistent with the framework's assignment of five phenomena to the spatial configuration dimension.
proof idea
The proof invokes the decide tactic on the Fintype instance derived from the inductive type. This tactic evaluates the cardinality by direct enumeration of the five constructors, returning the equality to five.
why it matters
The result populates the five_phenomena component of the OpticsCert structure, which also records zero J-cost for equal media and positive cost for bending. It thereby completes the optics certification in the module, linking the five phenomena to the Recognition Science claim that configDim equals five without introducing axioms or sorry placeholders.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.