constZero_scaleInvariant
plain-language theorem explainer
Constant zero satisfies scale invariance, so its cost remains unchanged when both arguments are scaled by the same positive factor. Foundation workers cite this when showing that distinguishability is equivalent to the non-triviality condition inside SatisfiesLawsOfLogic. The proof is a direct one-line term verification that reduces both sides to zero by reflexivity after introducing the scaling parameters.
Claim. The constant-zero comparison operator defined by $C(x,y):=0$ satisfies scale invariance: $C(λx,λy)=C(x,y)$ for all $x,y,λ>0$.
background
Scale invariance is the property that the cost of a comparison depends only on the ratio of the two quantities. The constant-zero operator is the function that returns zero for every pair of positive reals. In the NonTrivialityFromDistinguishability module this property is checked to support the equivalence between distinguishability and the non_trivial field of SatisfiesLawsOfLogic. Upstream, ScaleInvariant is defined as ∀ x y lam : ℝ, 0 < x → 0 < y → 0 < lam → C (lam * x) (lam * y) = C x y, which encodes the d'Alembert route-independence form required by the four Aristotelian laws.
proof idea
The proof is a one-line term-mode wrapper. It introduces the six variables (two quantities, the scale factor, and three positivity hypotheses) and concludes by reflexivity, since both sides of the required equality are identically zero under the constant-zero definition.
why it matters
This result confirms that the trivial operator meets the structural scale-invariance requirement used in the equivalence between distinguishability and non-triviality. It therefore participates in the module's replacement of the non_trivial posit by the more Aristotelian distinguishability condition. No downstream uses are recorded yet, and the declaration touches no open scaffolding questions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.