excluded_middle_implies_continuous
plain-language theorem explainer
If a comparison operator on positive reals satisfies excluded middle, its uncurried form is continuous on the positive quadrant and the derived cost function r ↦ C(r,1) is therefore continuous on (0,∞). Researchers tracing the Recognition Science derivation from Aristotelian logic to functional equations cite this translation lemma when establishing smoothness for the Aczél equation. The proof is a direct composition argument: the pair map r ↦ (r,1) is continuous, sends (0,∞) into the positive quadrant, and composes with the uncurried operator.
Claim. Let $C : (0,∞) × (0,∞) → ℝ$ be a comparison operator. If the uncurried map $(x,y) ↦ C(x,y)$ is continuous on the positive quadrant, then the derived cost function $r ↦ C(r,1)$ is continuous on $(0,∞)$.
background
ComparisonOperator is the type ℝ → ℝ → ℝ of maps sending pairs of positive quantities to a real cost. ExcludedMiddle C is the proposition that the uncurried form of C is continuous on the positive quadrant, expressing that every comparison returns a definite real value with continuous dependence on inputs. derivedCost C is the one-argument function obtained by fixing the second argument at the multiplicative identity 1, which is well-defined on positive ratios once scale invariance is imposed.
proof idea
The proof first shows the pair map s ↦ (s,1) is continuous on (0,∞) by continuous_id.prodMk continuous_const and restricts it to the open interval. It verifies that this map sends (0,∞) into the positive quadrant. Composition with the uncurried C, which is continuous on the quadrant by the ExcludedMiddle hypothesis, produces a continuous function on (0,∞). Function extensionality confirms the composition equals derivedCost C, so the result follows.
why it matters
This lemma is invoked inside laws_of_logic_imply_dalembert_hypotheses to obtain the normalized, symmetric, and continuous combiner needed for the d'Alembert inevitability theorem. It also supplies the continuous log-coordinate Aczél data used by log_aczel_data_of_laws. In the Recognition Science chain it closes the translation from the four Aristotelian constraints to the functional equation whose solutions force the phi-ladder, the eight-tick octave, and D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 1 of 1)
-
Softmax normalization creates attention sinks in language models
"After relaxing such dependence by replacing softmax attention with other attention operations, such as sigmoid attention without normalization, attention sinks do not emerge in LMs up to 1B parameters."