theorem
proved
tactic proof
inevitability_chain
show as:
view Lean formalization →
formal statement (Lean)
165theorem inevitability_chain
166 (h_defect : ∀ x : ℝ, x > 0 → (defect x = 0 ↔ x = 1))
167 (h_nothing : ∀ C : ℝ, ∃ ε > 0, ∀ x, 0 < x → x < ε → C < defect x)
168 (h_phi : ∃! x : ℝ, x > 0 ∧ x^2 = x + 1) :
169 ∀ (cost : ℝ → ℝ),
170 (cost 1 = 0) →
171 (∀ x, 0 < x → cost x = cost (1/x)) → -- Symmetry
172 (∀ x, 0 < x → cost x ≥ 0) → -- Non-negativity
173 (ContDiff ℝ 2 cost) → -- Smoothness
174 (deriv (deriv (fun t => cost (Real.exp t))) 0 = 1) → -- Calibration
175 (DAlembert.FourthGate.HasDAlembert cost) → -- d'Alembert structure
176 (∀ x, 0 < x → cost x = J x) := by
proof body
Tactic-mode proof.
177 intro cost hNorm hSymm hNonNeg hSmooth hCalib hDA
178 have hSymmInv : ∀ x, 0 < x → cost x = cost x⁻¹ := by
179 intro x hx
180 simpa [one_div] using hSymm x hx
181 -- The fourth gate already packages the required uniqueness step.
182 exact DAlembert.FourthGate.dAlembert_forces_Jcost
183 cost hNorm hSymmInv hSmooth hCalib hDA
184
185/-- NoFreeParameters holds: J is uniquely determined by the axiom bundle. -/