rcl_direct_theorem
The theorem establishes that any symmetric bi-affine combiner P consistent with the derived cost from an operative positive-ratio comparison must reduce to the form 2u + 2v + c0 uv. Researchers deriving the Recognition Composition Law from logic constraints would cite this for the counted-once subcase. The proof solves the system by substituting the identity element and a non-trivial ratio into the multiplicative consistency equation, then applies non-zero divisors to pin the linear coefficients.
claimLet $C$ be an operative positive-ratio comparison operator on positive reals. Let $P(u,v) = a + b u + c v + d u v$ be symmetric and satisfy multiplicative consistency with the derived cost $F(r) = C(r,1)$, i.e., $F(xy) + F(x/y) = P(F(x),F(y))$ for all positive $x,y$. Then there exists $c_0$ such that $P(u,v) = 2u + 2v + c_0 uv$ for all $u,v$.
background
A ComparisonOperator is a map from pairs of positive reals to reals that encodes the cost of comparing two quantities. The derivedCost function extracts the cost relative to the multiplicative identity by setting the second argument to 1, yielding a well-defined function on positive ratios under scale invariance. OperativePositiveRatioComparison packages the structural constraints: identity (cost zero when arguments match), non-contradiction, continuity, scale invariance, and non-triviality (existence of a ratio with non-zero cost). HasMultiplicativeConsistency states that the derived cost satisfies $F(xy) + F(x/y) = P(F(x),F(y))$ for the given combiner $P$. The module isolates the bi-affine counted-once subcase as a direct algebraic route to the Recognition Composition Law family, independent of the broader d'Alembert inevitability argument.
proof idea
The tactic proof first obtains a = 0 by evaluating consistency at (1,1) together with the identity property, which forces P(0,0) = 0. It then selects a non-trivial positive ratio x0 with t = derivedCost C x0 ≠ 0. Consistency at (x0,1) produces the linear relation t + t = a + b t; combined with a = 0 and mul_eq_zero this yields b = 2. Symmetry of P together with the same relation at swapped arguments forces c = 2. The remaining coefficient d is retained and the identity is verified by direct substitution and ring simplification.
why it matters in Recognition Science
This declaration supplies the algebraic core for the counted-once route to the Recognition Composition Law. It is invoked directly by counted_once_combiner_forces_rcl to conclude that the derived cost satisfies the RCL family. The result closes the strict bi-affine subcase inside the LogicAsFunctionalEquation module and supplies an independent verification path that does not rely on the full d'Alembert inevitability theorem. Within the Recognition Science chain it confirms that the eight-tick octave and phi-ladder structure can be recovered from the functional equation once the combiner is forced into the canonical form.
scope and limits
- Does not prove the general RCL without the bi-affine hypothesis on P.
- Does not construct or guarantee existence of an operative comparison operator C.
- Does not address non-counted-once or infinite pairwise cases.
- Does not derive the numerical value of the constant c0 from further physics input.
Lean usage
rcases hCount with ⟨P, ⟨a, b, c, d, hP⟩, hSym, hCons⟩; have h := rcl_direct_theorem C hOp P a b c d hP hSym hConsformal statement (Lean)
100theorem rcl_direct_theorem
101 (C : ComparisonOperator)
102 (hOp : OperativePositiveRatioComparison C)
103 (P : ℝ → ℝ → ℝ)
104 (a b c d : ℝ)
105 (hP : ∀ u v, P u v = a + b * u + c * v + d * u * v)
106 (hSym : ∀ u v, P u v = P v u)
107 (hCons : HasMultiplicativeConsistency (derivedCost C) P) :
108 ∃ c0 : ℝ, ∀ u v, P u v = 2 * u + 2 * v + c0 * u * v := by
proof body
Tactic-mode proof.
109 have hF1 : derivedCost C 1 = 0 := by
110 simpa [derivedCost] using hOp.identity 1 zero_lt_one
111 rcases hOp.non_trivial with ⟨x0, hx0_pos, hx0_ne⟩
112 let t := derivedCost C x0
113 have ht_ne : t ≠ 0 := hx0_ne
114
115 have hCons11 := hCons 1 1 zero_lt_one zero_lt_one
116 have hC11 : C 1 1 = 0 := hOp.identity 1 zero_lt_one
117 have ha_zero : a = 0 := by
118 have hp00 : P 0 0 = a := by
119 simpa using hP 0 0
120 have hzero : P 0 0 = 0 := by
121 have htmp : 0 = P 0 0 := by
122 simpa [derivedCost, hC11] using hCons11
123 exact htmp.symm
124 exact hp00 ▸ hzero
125
126 have hCons_x1 := hCons x0 1 hx0_pos zero_lt_one
127 have hb_two : b = 2 := by
128 have hmain : t + t = a + b * t := by
129 simpa [derivedCost, t, hC11, hP] using hCons_x1
130 have hprod : (2 - b) * t = 0 := by
131 nlinarith [hmain, ha_zero]
132 have hfactor : 2 - b = 0 := by
133 exact (mul_eq_zero.mp hprod).resolve_right ht_ne
134 linarith
135
136 have hc_two : c = 2 := by
137 have hsym_t0 : P 0 t = P t 0 := hSym 0 t
138 have hleft : P 0 t = c * t := by
139 simpa [ha_zero] using hP 0 t
140 have hright : P t 0 = b * t := by
141 simpa [ha_zero] using hP t 0
142 have hct : c * t = b * t := by
143 simpa [hleft, hright] using hsym_t0
144 have hct' : c * t = 2 * t := by
145 simpa [hb_two] using hct
146 have hprod : (c - 2) * t = 0 := by
147 nlinarith
148 have hfactor : c - 2 = 0 := by
149 exact (mul_eq_zero.mp hprod).resolve_right ht_ne
150 linarith
151
152 refine ⟨d, ?_⟩
153 intro u v
154 calc
155 P u v = a + b * u + c * v + d * u * v := hP u v
156 _ = 2 * u + 2 * v + d * u * v := by
157 rw [ha_zero, hb_two, hc_two]
158 ring
159
160end LogicAsFunctionalEquation
161end Foundation
162end IndisputableMonolith