theorem proved term proof

`phiScale_neg`

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

formal statement (Lean)

  81theorem phiScale_neg (n : ℤ) (x : ℝ) :
  82    phiScale (-n) (phiScale n x) = x := by

proof body

Term-mode proof.

  83  rw [phiScale_add, neg_add_cancel, phiScale_zero]
  84
  85/-! ## The φ-Ladder Hypothesis Class -/
  86
  87/-- A value is on the φ-ladder if it equals X₀ · φⁿ for some base X₀ and integer n. -/

depends on (14)

Lean names referenced from this declaration's body.

Hypothesis in IndisputableMonolith.ClassicalBridge.Fluids.CPM2D decl_use
A in IndisputableMonolith.Foundation.IntegrationGap decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
A in IndisputableMonolith.Masses.Anchor decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
A in IndisputableMonolith.Modal.Actualization decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use
value in IndisputableMonolith.QFT.SpinStatistics decl_use
phiScale in IndisputableMonolith.RRF.Hypotheses.PhiLadder decl_use
phiScale_add in IndisputableMonolith.RRF.Hypotheses.PhiLadder decl_use
phiScale_zero in IndisputableMonolith.RRF.Hypotheses.PhiLadder decl_use