same_medium
plain-language theorem explainer
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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.