ratioCost_zero_iff
plain-language theorem explainer
The equivalence shows that the ratio-derived cost between two frequency ratios vanishes exactly when the ratios are identical. Researchers formalizing strict logic realizations in physical domains cite this to confirm the cost function detects equality. The argument unfolds the piecewise definition and splits cases on whether the arguments coincide.
Claim. For frequency ratios $a, b > 0$, the cost function defined by $C(a,b) := 0$ if $a = b$ and $1$ otherwise satisfies $C(a,b) = 0$ if and only if $a = b$.
background
The Rich Domain Cost Theorems module supplies concrete proofs for cost functions across five domains (Music, Biology, Narrative, Ethics, Metaphysical) that realize strict logic with excluded-middle, composition, and invariance laws. FrequencyRatio is the subtype of positive reals. The ratioCost function returns the natural number 0 on equality and 1 otherwise. This rests on the general ratioCost from PositiveRatioForcing, which extracts a scale-invariant comparison factor via a ComparisonOperator applied to the ratio and unity.
proof idea
Unfold the definition of ratioCost from the Music module to expose the if-then-else expression. Perform case analysis on whether a equals b. Simplify both sides of the biconditional in each branch to obtain the equivalence.
why it matters
This supplies the music_cost_zero_iff component of the richDomainCostsCert_holds certificate that verifies all five domain costs. It completes the verification that zero cost coincides with identity, supporting the required composition and invariance laws for strict realizations. The result sits inside the broader forcing-chain development but does not directly invoke T5 J-uniqueness or the RCL.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.