laws_of_logic_imply_dalembert_hypotheses
plain-language theorem explainer
A comparison operator obeying the four Aristotelian constraints plus scale invariance and non-triviality produces a derived cost function that meets every hypothesis of the d'Alembert inevitability theorem. Researchers formalizing the logical origins of the Recognition Composition Law would cite this result to connect Aristotelian structure to the functional-equation setting. The proof is a term-mode refinement that assembles five direct translation lemmas, one for each required analytic property.
Claim. Let $C : (0,∞) × (0,∞) → ℝ$ be a comparison operator. Suppose $C$ satisfies identity, non-contradiction, excluded middle, route independence, scale invariance, and non-triviality. Then the derived cost $F(x) := C(x,1)$ obeys $F(1)=0$, $F(x)=F(1/x)$, admits a symmetric quadratic polynomial $P$ such that $F(xy)+F(x/y)=P(F(x),F(y))$ for all positive $x,y$, is continuous on $(0,∞)$, and is non-trivial.
background
ComparisonOperator is the type of maps from pairs of positive reals to reals that assign a cost to comparing two quantities. SatisfiesLawsOfLogic packages the four Aristotelian constraints (identity, non-contradiction, excluded middle, route independence) together with scale invariance, which reduces the two-argument form to a one-argument derived cost, and non-triviality, which excludes the zero function. The derived cost is obtained by fixing the second argument at the multiplicative identity 1, yielding a function on positive ratios. This theorem translates those logical axioms into the exact hypotheses required by bilinear_family_forced in the d'Alembert inevitability module: normalized, symmetric, multiplicatively consistent via a symmetric quadratic polynomial, continuous on positives, and non-trivial.
proof idea
The proof is a term-mode refinement that constructs a five-tuple of the required properties. It applies identity_implies_normalized to the identity field, non_contradiction_and_scale_imply_reciprocal to the non-contradiction and scale_invariant fields, route_independence_implies_multiplicative_consistency to the route_independence field, excluded_middle_implies_continuous to the excluded_middle field, and passes the non_trivial field directly.
why it matters
This theorem supplies the missing translation step that lets the peer-reviewed bilinear_family_forced close the chain from logic to the Recognition Composition Law. It is invoked directly by the downstream results J_is_unique_cost_under_logic and RCL_is_unique_functional_form_of_logic. The module doc-comment identifies it as the core technical content of the precursor paper; once available, the existing machine-verified uniqueness theorems complete the passage from Aristotelian constraints to the canonical J-cost and the phi-ladder. In the broader framework it shows how the laws of logic force the functional equation whose solutions determine 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 3 of 3)
-
Frontier models scheme to disable oversight and exfiltrate weights
"Analysis of the models' chains-of-thought reveals that models explicitly reason about these deceptive strategies"
-
Multimodal LLMs barely beat random guessing on perception tasks
"these perception-demanding tasks cast significant challenges for current multimodal LLMs because they resist mediation through natural language"
-
Spotlighting cuts indirect prompt injection success to under 2%
"LLM is unable to distinguish which sections of prompt belong to various input sources"