pith. sign in
theorem

RCL_is_unique_functional_form_of_logic

proved
show as:
module
IndisputableMonolith.Foundation.LogicAsFunctionalEquation
domain
Foundation
line
309 · github
papers citing
9 papers (below)

plain-language theorem explainer

Any comparison operator on positive reals obeying the four Aristotelian constraints plus scale invariance and non-triviality forces its derived cost to satisfy multiplicative consistency through a bilinear combiner of the exact form P(u, v) = 2u + 2v + c uv. Researchers tracing the emergence of the Recognition Composition Law from logical primitives would cite this result when connecting Aristotelian structure to the d'Alembert setup. The proof is a direct term-mode extraction that first derives the full d'Alembert hypotheses from the logic law

Claim. Let $C$ be a comparison operator. If $C$ satisfies the laws of logic (identity, non-contradiction, excluded middle, scale invariance, route independence, and non-triviality), then there exist a function $P : ℝ → ℝ → ℝ$ and a constant $c ∈ ℝ$ such that the derived cost of $C$ satisfies multiplicative consistency with $P$ and $P(u, v) = 2u + 2v + c · uv$ for all real $u, v$.

background

The module formalizes logic as a functional equation. A ComparisonOperator is the type ℝ → ℝ → ℝ that assigns a real cost to any pair of positive quantities; the four Aristotelian constraints (identity, non-contradiction, excluded middle, route independence) together with scale invariance and non-triviality are packaged in the structure SatisfiesLawsOfLogic. The derived cost is obtained by fixing the second argument at the multiplicative identity, yielding a function on positive ratios. The local setting is the bridge from these logical axioms to the d'Alembert inevitability framework. The proof relies on the upstream theorem bilinear_family_forced, whose statement is: given a normalized symmetric cost F with multiplicative consistency via a symmetric quadratic polynomial P and non-triviality, the combiner P must be bilinear of the stated form.

proof idea

The proof is a term-mode extraction. It first applies laws_of_logic_imply_dalembert_hypotheses to C and the laws hypothesis to obtain normalization, consistency, polynomial form, symmetry, continuity, and non-triviality. It then feeds these directly into bilinear_family_forced, which returns the specific coefficients that fix P(u, v) = 2u + 2v + c uv together with the consistency property, and packages the pair (P, c) as the existential witness.

why it matters

This theorem shows that the Recognition Composition Law is the unique functional form compatible with the laws of logic under polynomial regularity. It supplies the logical justification for the RCL that is invoked by the downstream rcl_polynomial_closure_theorem on operative positive-ratio comparisons with finite pairwise polynomial closure. In the Recognition Science chain it supports the passage from T5 (J-uniqueness) through the RCL to the phi-ladder and the calibrated constants, citing the peer-reviewed d'Alembert Inevitability Theorem.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.