different_media
plain-language theorem explainer
The theorem establishes that the J-cost is strictly positive for any positive real refraction ratio r different from one. Researchers deriving Snell's law within Recognition Science would cite it to confirm bending occurs precisely between distinct media. The proof is a direct one-line application of the general positivity lemma for the J-cost.
Claim. For every positive real number $r$ with $r ≠ 1$, the associated cost satisfies $0 < J(r)$, where $J(r)$ is the cost function for the refraction ratio $r = n_2/n_1$.
background
The module OpticsSnellsLawFromRS derives Snell's law from Recognition Science by mapping the refraction ratio $r = n_2/n_1$ to the J-cost. At $r = 1$ (identical media) the cost is zero and no bending occurs; at $r ≠ 1$ the cost is positive and refraction follows. The upstream lemma Jcost_pos_of_ne_one states that J(x) > 0 for x > 0 and x ≠ 1, proved by rewriting the cost as a square over a positive denominator.
proof idea
The proof is a one-line wrapper that applies the lemma Jcost_pos_of_ne_one to the given hypotheses on r.
why it matters
This supplies the bending_positive component of the opticsCert definition, which certifies that the five optical phenomena arise from the Recognition Science cost structure. It fills the B14 Optics Depth step showing that different media produce positive J-cost and therefore refraction, consistent with the Recognition Composition Law. The result touches the extension from geometric optics to full wave phenomena.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.