pith. machine review for the scientific record. sign in
theorem proved term proof

hyperbolic_not_flat

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 120theorem hyperbolic_not_flat : ¬ SatisfiesFlatODE Gcosh := Gcosh_not_flat

proof body

Term-mode proof.

 121
 122/-! ## The Bridge: Connecting the Gates -/
 123
 124/-- **Key Hypothesis**: Interaction + Structural Axioms forces the hyperbolic ODE.
 125
 126    This is the central bridge connecting the gates. It says:
 127    If F has interaction, symmetry, normalization, smoothness, and consistency,
 128    then the log-lift G satisfies G'' = G + 1.
 129
 130    This is NOT yet fully proved from first principles, but is strongly motivated by:
 131    1. The counterexample (no interaction) ⟹ flat ODE
 132    2. J (has interaction) ⟹ hyperbolic ODE
 133    3. Entanglement forces a specific functional form
 134
 135    We state it as an explicit hypothesis to make the logical structure clear.
 136-/

depends on (22)

Lean names referenced from this declaration's body.