laws_polynomial_implies_continuous
plain-language theorem explainer
Any comparison operator satisfying the Laws of Logic under polynomial route independence also satisfies the continuous Laws of Logic. Researchers extending the Translation Theorem cite it to drop the degree-≤2 hypothesis in favor of continuity of the combiner. The proof is a term-mode structure constructor that copies five axioms verbatim and applies the sibling polynomial-implies-continuous lemma only to the route-independence field.
Claim. Let $C$ be a comparison operator. If $C$ satisfies the Laws of Logic, then $C$ satisfies the continuous Laws of Logic, in which the route-independence axiom is the continuous version rather than the polynomial version.
background
The GeneralizedDAlembert module carries out Move 3: it discharges the polynomial-degree restriction on the route-independence combiner that appears in the Translation Theorem. The key external tool is the Aczél–Kannappan classification, which states that a continuous $H:ℝ→ℝ$ with $H(0)=1$ obeying the d'Alembert equation is either the constant 1, a hyperbolic cosine, or a trigonometric cosine. This classification is proved inside the framework by reduction to the existing dAlembert_classification lemma.
proof idea
The proof is a direct term-mode construction of the SatisfiesLawsOfLogicContinuous structure. It assigns the identity, non-contradiction, excluded-middle, scale-invariance and non-trivial fields by copying the corresponding fields of the input witness h. The sole non-trivial step replaces the route-independence field by an application of the sibling lemma polynomial_implies_continuous to the polynomial route-independence component of h.
why it matters
The declaration shows that every polynomial-case Laws of Logic witness is already a continuous-case witness, so the continuous version strictly subsumes the polynomial version. It is invoked inside the downstream theorem laws_continuous_subsumes_polynomial and completes the algebraic half of the continuous-combiner assembly described in the module doc. The framework still needs separate ContinuousCombinerAnalysisInputs to reach the bilinear conclusion; the quartic-log counterexample remains an obstruction to dropping all regularity hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.