theorem proved term proof

`P_symmetric_on_range`

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

formal statement (Lean)

  82theorem P_symmetric_on_range
  83    (F : ℝ → ℝ)
  84    (P : ℝ → ℝ → ℝ)
  85    (hSymm : ∀ x : ℝ, 0 < x → F x = F x⁻¹)
  86    (hCons : ∀ x y : ℝ, 0 < x → 0 < y → F (x * y) + F (x / y) = P (F x) (F y)) :
  87    ∀ u v : ℝ, (∃ x, 0 < x ∧ F x = u) → (∃ y, 0 < y ∧ F y = v) → P u v = P v u := by

proof body

Term-mode proof.

  88  intro u v ⟨x, hx, hFx⟩ ⟨y, hy, hFy⟩
  89  have h := P_symmetric_of_F_symmetric F P hSymm hCons x y hx hy
  90  rw [← hFx, ← hFy]
  91  exact h
  92
  93/-! ## Part 2: P(u, 0) = 2u from Normalization -/
  94
  95/-- If F(1) = 0 and the consistency equation holds, then P(u, 0) = 2u on the range of F. -/

depends on (12)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
Normalization in IndisputableMonolith.Foundation.CostAxioms decl_use
P_symmetric_of_F_symmetric in IndisputableMonolith.Foundation.DAlembert.FullUnconditional decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use
F in IndisputableMonolith.Physics.AnchorPolicy decl_use
F in IndisputableMonolith.Physics.LeptonGenerations.TauStepDerivation decl_use
F in IndisputableMonolith.Pipelines decl_use