mechanical_thermal_symmetric
plain-language theorem explainer
The declaration establishes that therapy J-cost remains unchanged when the intensity ratio is inverted. Acoustics modelers working on HIFU and LIPUS thresholds would cite it to confirm that mechanical and thermal regimes depend only on ratio magnitude, not direction. The proof is a direct one-line application of the J reciprocal invariance lemma.
Claim. For any nonzero real number $x$, the therapy J-cost satisfies $J(x) = J(1/x)$, where $J$ denotes the cost function applied to the intensity ratio.
background
The module develops the canonical-band argument for ultrasound therapy thresholds. therapyJCost is defined as the J function applied to the intensity ratio $r$. The J function obeys reciprocal symmetry, stated in CostAlgebra as the algebraic encoding of double-entry bookkeeping: every ratio and its reciprocal carry the same cost. The CanonicalJBand version relaxes the positivity hypothesis to mere nonzeroness via field simplification and ring normalization.
proof idea
The proof is a one-line wrapper that applies the J_reciprocal lemma from CanonicalJBand, instantiated directly on the nonzero hypothesis for $x$.
why it matters
The result supplies the algebraic symmetry required for the canonical-band identity in the B14 ultrasound model. It aligns with the module's description of mechanical-index ratios approximating phi squared across safe-to-ablative steps. The declaration closes one algebraic prerequisite for the empirical correspondence hypothesis noted in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.