`Fquad_is_flat`

proved

show as: view math explainer →

module: IndisputableMonolith.Foundation.DAlembert.TriangulatedProof
domain: Foundation
line: 90 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.DAlembert.TriangulatedProof on GitHub at line 90.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  87theorem Jcost_is_hyperbolic : HasInteraction Cost.Jcost := Jcost_hasInteraction
  88
  89/-- Fquad is in the flat branch (no interaction). -/
  90theorem Fquad_is_flat : ¬ HasInteraction Counterexamples.Fquad := Fquad_noInteraction
  91
  92/-! ## Gate 2: Entanglement Characterizes the Combiner -/
  93
  94/-- RCL combiner is entangling. -/
  95theorem RCL_is_entangling : IsEntangling Prcl := Prcl_entangling
  96
  97/-- Additive combiner is not entangling. -/
  98theorem additive_not_entangling : ¬ IsEntangling Padd := Padd_not_entangling
  99
 100/-- Interaction forces entanglement (under symmetry). -/
 101theorem interaction_forces_entanglement (F : ℝ → ℝ) (P : ℝ → ℝ → ℝ)
 102    (hCons : ∀ x y : ℝ, 0 < x → 0 < y → F (x * y) + F (x / y) = P (F x) (F y))
 103    (hNorm : F 1 = 0)
 104    (hSymm : ∀ x : ℝ, 0 < x → F x = F x⁻¹)
 105    (hInt : HasInteraction F) :
 106    IsEntangling P :=
 107  interaction_implies_entangling F P hCons hNorm hSymm hInt
 108
 109/-! ## Gate 3: Curvature Characterizes the ODE -/
 110
 111/-- J's log-lift satisfies the hyperbolic ODE. -/
 112theorem Jcost_hyperbolic_ODE : SatisfiesHyperbolicODE Gcosh := Gcosh_satisfies_hyperbolic
 113
 114/-- Fquad's log-lift satisfies the flat ODE. -/
 115theorem Fquad_flat_ODE : SatisfiesFlatODE Gquad := Gquad_satisfies_flat
 116
 117/-- The two ODEs are mutually exclusive. -/
 118theorem flat_not_hyperbolic : ¬ SatisfiesHyperbolicODE Gquad := Gquad_not_hyperbolic
 119
 120theorem hyperbolic_not_flat : ¬ SatisfiesFlatODE Gcosh := Gcosh_not_flat

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.