same_medium
Recognition Science maps the refractive index ratio r to a J-cost, which vanishes exactly at r = 1. Workers deriving Snell's law from the recognition functional equation cite this to anchor the no-bending baseline. The proof is a direct term application of the upstream Jcost unit lemma.
claim$J(1) = 0$, where $J(r)$ is the recognition cost for refractive index ratio $r$.
background
The Cost module defines the J-cost as $J(x) = (x-1)^2/(2x)$, which quantifies the recognition defect for scaling factor x. The OpticsSnellsLawFromRS module recasts Snell's law by associating refraction ratio $r = n_2/n_1$ with this J(r) cost. The module states that at r = 1 (same medium) J = 0 implies no bending, while r ≠ 1 yields J > 0 and bending. This rests on the upstream lemma Jcost_unit0, which proves the unit case by simplification of the Jcost definition.
proof idea
The declaration is a one-line term proof that directly invokes the lemma Jcost_unit0 from the Cost module.
why it matters in Recognition Science
This theorem supplies the same_medium_zero field in the opticsCert definition, which certifies that five canonical optical phenomena arise from configDim D = 5. It instantiates the J-uniqueness property at the fixed point r = 1, confirming zero cost for identical media as required by the forcing chain. The result closes the equal-media case without touching open questions in the optics derivation.
scope and limits
- Does not derive Snell's law for differing media.
- Does not compute explicit bending angles.
- Does not incorporate wavelength dependence.
- Does not prove the five-phenomena count.
Lean usage
example : Jcost 1 = 0 := same_mediumformal statement (Lean)
31theorem same_medium : Jcost 1 = 0 := Jcost_unit0
proof body
Term-mode proof.
32
33/-- Different media: J > 0 (bending occurs). -/