opticsCert
plain-language theorem explainer
The opticsCert definition assembles the OpticsCert structure confirming five optical phenomena together with the J-cost vanishing at unit ratio and positive for any other positive ratio. A physicist deriving Snell's law from the Recognition functional equation would cite this certificate. It is a direct record construction that assembles three sibling theorems on phenomenon count and J-cost evaluations.
Claim. The optics certificate asserts that the type of optical phenomena has cardinality five, that the J-cost vanishes at unit ratio, and that the J-cost is strictly positive for every positive ratio different from one: $Fintype.card(OpticalPhenomenon)=5$, $J(1)=0$, and $0<r, r≠1 ⇒ 0<J(r)$.
background
In the Recognition Science optics module the J-cost function encodes the energetic cost of a refraction ratio r = n₂/n₁ via the Recognition Composition Law, with J(r) = (r + r^{-1})/2 - 1. The OpticsCert structure packages three facts required for Snell's law: exactly five canonical phenomena (reflection, refraction, diffraction, interference, polarisation) counted as configDim D = 5, zero cost when media are identical, and positive cost otherwise. The module states that refraction ratio r ↔ J(r) cost, with J = 0 at r = 1 and J > 0 at r ≠ 1, yielding n₁ sin θ₁ = n₂ sin θ₂ without extra axioms.
proof idea
The definition constructs the OpticsCert record by assigning the five_phenomena field to opticalPhenomenonCount, the same_medium_zero field to same_medium, and the bending_positive field to different_media. No additional tactics or reductions are performed.
why it matters
This definition certifies the optical layer of Recognition Science and supplies the interface for deriving Snell's law from the J-uniqueness property (T5) and the Recognition Composition Law. It connects the five-phenomena count to the framework's configDim D = 5 while grounding the bending rule in the positivity of J for unequal media. No downstream theorems are yet attached, but the certificate closes the optics scaffolding for further wave derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.