OperativePositiveRatioComparison
An operative positive-ratio comparison is a continuous nontrivial comparison operator on positive reals obeying identity, reciprocal symmetry, and scale invariance. Researchers deriving the Recognition Composition Law via the direct counted-once route cite this structure to package the minimal Aristotelian constraints plus regularity. The declaration is a pure structure definition that bundles five independent properties with no proof steps.
claimA comparison operator $C: (0,∞)×(0,∞)→ℝ$ is an operative positive-ratio comparison when it satisfies $C(x,x)=0$ for all $x>0$, $C(x,y)=C(y,x)$ for all $x,y>0$, is continuous on the positive quadrant, obeys $C(λx,λy)=C(x,y)$ for every $λ>0$, and is non-trivial (the associated one-argument cost is nonzero for at least one positive ratio).
background
A comparison operator returns a real-valued cost for any ordered pair of positive reals. Identity requires zero cost on equal arguments. Reciprocal symmetry (non-contradiction) forces the cost to be unchanged under argument swap. Continuity (excluded middle) ensures the cost map is continuous on the positive domain. Scale invariance reduces the two-argument cost to a function of the ratio alone via the derived-cost construction. Non-triviality excludes the zero function by demanding at least one positive ratio with nonzero cost. The module isolates these five properties as the operative wrapper needed to state the direct algebraic derivation of the Recognition Composition Law under the finite pairwise polynomial closure hypothesis.
proof idea
The declaration is a structure definition that collects the five named properties into a single Prop. No lemmas are invoked and no tactics are executed; it serves as a type-level bundling construct for downstream theorems that assume an operative comparison.
why it matters in Recognition Science
This structure supplies the central hypothesis for the direct RCL proof path. It is consumed by operative_to_laws_of_logic to build the SatisfiesLawsOfLogic record, by rcl_direct_theorem to obtain the bi-affine coefficients, and by counted_once_combiner_forces_rcl to derive the full RCL family. Within the Recognition framework it isolates the precise regularity (continuity plus scale invariance) that lets the Aristotelian laws force the functional equation without the d'Alembert route. It touches the open question whether finite pairwise polynomial closure is the weakest regularity condition sufficient for the RCL.
scope and limits
- Does not include the finite pairwise polynomial closure hypothesis.
- Does not derive the Recognition Composition Law.
- Does not specify the explicit algebraic form of the derived cost.
- Does not address comparisons involving non-positive reals.
- Does not prove uniqueness of any comparison operator satisfying the properties.
formal statement (Lean)
24structure OperativePositiveRatioComparison (C : ComparisonOperator) : Prop where
25 identity : Identity C
26 non_contradiction : NonContradiction C
27 continuous : ExcludedMiddle C
28 scale_invariant : ScaleInvariant C
29 non_trivial : NonTrivial C
30
31/-- Finite pairwise polynomial closure is the polynomial route-independence
32condition from the Level-1 logic-as-functional-equation module. -/
used by (11)
-
mismatch_to_operative -
counted_once_combiner_forces_rcl -
operative_derived_cost_symmetric -
operative_descends_to_ratio -
operative_to_laws_of_logic -
rcl_direct_theorem -
rcl_polynomial_closure_theorem -
finite_logical_to_operative -
no_hidden_state_logic_forces_rcl -
no_hidden_state_comparison_forces_rcl -
truth_eval_to_operative