pith. sign in
module module moderate

IndisputableMonolith.Physics.OpticsSnellsLawFromRS

show as:
view Lean formalization →

This module derives Snell's law for refraction from Recognition Science by classifying light paths as optical phenomena and separating same-medium from different-media cases. Physicists building RS foundations for classical optics would cite it when linking J-cost to ray bending. The module organizes the material through sibling definitions and predicates that rest on the imported Cost module, with no complex proofs required.

claimIn the same medium the cost satisfies $J=0$, implying no bending. Refraction between distinct media obeys the symmetric condition derived from the Recognition Composition Law, recovering Snell's law $n_1 sin i = n_2 sin r$.

background

The module imports IndisputableMonolith.Cost, which supplies the J-cost function $J(x)=(x+x^{-1})/2-1$ and the Recognition Composition Law $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$. It introduces OpticalPhenomenon as the type for light propagation behavior together with a count function and the predicates same_medium, different_media, and refraction_symmetric. The local setting applies the T5 J-uniqueness and T7 eight-tick octave to optics, with the supplied doc-comment stating that same medium yields J=0 and therefore no bending.

proof idea

This is a definition module, no proofs. It declares the OpticalPhenomenon type, the opticalPhenomenonCount function, the case predicates same_medium, different_media, refraction_symmetric, and the certification OpticsCert that packages the optical claims.

why it matters in Recognition Science

The module supplies the optics layer inside the Recognition Science framework, connecting the J-cost and RCL to classical refraction and preparing the ground for Snell's law as a cost-minimization consequence. It sits downstream of the Cost module and the T0-T8 forcing chain; no theorems yet list it among their dependencies.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (7)