pith. machine review for the scientific record. sign in
structure definition def or abbrev high

SatisfiesLawsOfLogicContinuous

show as:
view Lean formalization →

SatisfiesLawsOfLogicContinuous defines the continuous analogue of the laws of logic for a comparison operator C on positive reals. Researchers working on the d'Alembert functional equation and the Recognition Science Translation Theorem cite it to replace the polynomial route-independence hypothesis with a continuity requirement. The declaration is a structure definition that assembles six field predicates without any computational content.

claimLet $C : (0,∞) × (0,∞) → ℝ$ be a comparison operator. Then $C$ satisfies the continuous laws of logic when it obeys the identity law, the non-contradiction law, the excluded-middle law (continuity of $C$ on the positive quadrant), scale invariance, continuous route independence (existence of a continuous symmetric combiner $P$ such that the derived cost satisfies $F(xy) + F(x/y) = P(F(x), F(y))$ for $x,y > 0$), and non-triviality.

background

The module GeneralizedDAlembert carries out Move 3 of the Recognition Science program: discharge the polynomial regularity hypothesis on the route-independence combiner by replacing it with continuity. The classical Aczél–Kannappan theorem states that a continuous solution $H$ of the d'Alembert equation with $H(0)=1$ is either the constant 1, a hyperbolic cosine, or a trigonometric cosine; the module imports the corresponding classification from Cost.FunctionalEquation and uses it to weaken the original SatisfiesLawsOfLogic predicate. ComparisonOperator is the two-argument cost map ℝ → ℝ → ℝ whose derived one-argument cost $F$ is obtained by fixing the second argument at 1. ContinuousRouteIndependence asserts the existence of a continuous symmetric $P : ℝ → ℝ → ℝ$ such that $F(xy) + F(x/y) = P(F(x), F(y))$ on positive ratios.

proof idea

The declaration is a structure definition whose body consists of six field requirements. Each field is supplied by an upstream predicate: Identity, NonContradiction, ExcludedMiddle and ScaleInvariant come from LogicAsFunctionalEquation; ContinuousRouteIndependence is the local continuous-route predicate; NonTrivial is the standard non-degeneracy condition. No tactics or reductions are performed; the structure simply packages the conjunction.

why it matters in Recognition Science

SatisfiesLawsOfLogicContinuous is the direct parent of ContinuousCombinerAnalysisInputs and of the continuous-combiner bilinear classification theorems (continuous_combiner_bilinear, continuous_combiner_bilinear_classification). It supplies the hypothesis package that lets the Aczél–Kannappan classification replace the polynomial-degree-≤-2 restriction in the original Translation Theorem. The definition therefore sits at the interface between the functional-equation core (T5–T8 forcing chain) and the later smoothness-bootstrap results; the quartic-log obstruction recorded in the downstream inputs shows that continuity alone does not yet force bilinearity.

scope and limits

formal statement (Lean)

 121structure SatisfiesLawsOfLogicContinuous (C : ComparisonOperator) : Prop where
 122  identity            : Identity C
 123  non_contradiction   : NonContradiction C
 124  excluded_middle     : ExcludedMiddle C
 125  scale_invariant     : ScaleInvariant C
 126  route_independence  : ContinuousRouteIndependence C
 127  non_trivial         : NonTrivial C
 128
 129/-- Log-coordinate Aczél data extracted from a continuous-combiner Law of
 130Logic witness. -/

used by (14)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (16)

Lean names referenced from this declaration's body.