OpticsCert
plain-language theorem explainer
OpticsCert packages the assertions that exactly five optical phenomena exist, that J-cost vanishes at refractive-index ratio one, and that J-cost is strictly positive for any other positive ratio. Physicists deriving Snell's law from the Recognition Science J-functional cite this structure to certify the optical sector. It is realized as a structure definition that directly records the three properties drawn from the OpticalPhenomenon enumeration and the Jcost function.
Claim. Let $O$ be the finite set consisting of reflection, refraction, diffraction, interference and polarisation. The structure asserts that $|O|=5$, that the J-cost of ratio $1$ equals zero, and that $Jcost(r)>0$ for every positive real $r$ with $r≠1$.
background
In the module deriving Snell's law from Recognition Science, the J-cost function supplies the energetic penalty attached to a refractive-index ratio $r=n_2/n_1$. The inductive type OpticalPhenomenon enumerates the five canonical phenomena (reflection, refraction, diffraction, interference, polarisation) and carries a Fintype instance. The module states that these five phenomena correspond to configDim $D=5$, that J-cost vanishes for equal media, and that it is positive for unequal media.
proof idea
The declaration is a structure definition whose three fields are stated directly: the cardinality equation on OpticalPhenomenon, the zero identity at unit ratio, and the universal positivity condition for unequal ratios. No lemmas or tactics are invoked; the structure simply collects the properties for subsequent instantiation.
why it matters
OpticsCert supplies the certified interface for the optical sector inside the Recognition Science derivation of Snell's law. It is instantiated by the downstream opticsCert definition, which populates the fields from opticalPhenomenonCount, same_medium and different_media. The five-phenomena count aligns with the framework landmark that configDim $D=5$ for the optical phenomena, closing the B14 optics depth.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.