Pith. sign in
module module high

IndisputableMonolith.Physics.OpticsSnellsLawFromRS

show as:
view Lean formalization →

The module OpticsSnellsLawFromRS connects the J-cost from Recognition Science to classical refraction by defining optical phenomena and the case of same-medium propagation. Researchers deriving classical optics laws from the unified forcing chain would cite it. The module consists of definitions for OpticalPhenomenon along with predicates for same-medium, different-media, and symmetric refraction cases.

claimThe module defines the optical phenomenon predicate with same-medium case satisfying $J=0$ (no bending), different-media case, refraction_symmetric, and the certification OpticsCert.

background

The module imports the Cost module, which supplies the J function obeying the Recognition Composition Law. In the Recognition Science setting, J measures scale-recognition cost with the explicit form $J(x)=(x+x^{-1})/2-1$, and the same-medium predicate is the zero-cost instance. The module applies this to light propagation, introducing OpticalPhenomenon as the basic structure for refraction events in media distinguished by their J values.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

This module supplies the optical definitions that support derivation of Snell's law inside the Recognition framework. It draws on J-uniqueness from the forcing chain (T5) and the Recognition Composition Law to set up the same-medium and different-media cases. No downstream theorems are recorded as using the module.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (7)