SatisfiesLawsOfLogicContinuous
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.