300theorem laws_polynomial_implies_continuous 301 (C : ComparisonOperator) (h : SatisfiesLawsOfLogic C) : 302 SatisfiesLawsOfLogicContinuous C where 303 identity := h.identity
proof body
Term-mode proof.
304 non_contradiction := h.non_contradiction 305 excluded_middle := h.excluded_middle 306 scale_invariant := h.scale_invariant 307 route_independence := polynomial_implies_continuous C h.route_independence 308 non_trivial := h.non_trivial 309 310/-! ## 4. Conditional bilinear assembly 311 312The remaining continuous-combiner work separates cleanly into two 313parts. The hard analysis must classify the log-coordinate cost 314`G(t) = F(exp t)`. Once that classification is available, the bilinear 315combiner is just algebra. 316 317This section proves the algebraic half. It is independent of the 318regularization and ψ-affine forcing arguments. 319-/ 320 321/-- Log-coordinate bilinear identity with coefficient `c`. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.