Documentation Verification Report

Basic

📁 Source: PhysLean/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean

Statistics

Metric	Count
Definitions `DampedHarmonicOscillator`, `EquationOfMotion`, `IsCriticallyDamped`, `IsOverdamped`, `IsUnderdamped`, `discriminant`, `energy`, `energyDissipationRate`, `k`, `kineticEnergy`, `m`, `potentialEnergy`, `γ`, `ω₀`	14
Theorems `k_neq_zero`, `k_pos`, `m_neq_zero`, `m_pos`, `γ_nonneg`, `ω₀_pos`, `ω₀_sq`	7
Total	21

ClassicalMechanics

Definitions

Name	Category	Theorems
`DampedHarmonicOscillator` 📖	CompData	—

ClassicalMechanics.DampedHarmonicOscillator

Definitions

Name	Category	Theorems
`EquationOfMotion` 📖	MathDef	—
`IsCriticallyDamped` 📖	MathDef	—
`IsOverdamped` 📖	MathDef	—
`IsUnderdamped` 📖	MathDef	—
`discriminant` 📖	CompOp	—
`energy` 📖	CompOp	—
`energyDissipationRate` 📖	CompOp	—
`k` 📖	CompOp	2 math math: `k_pos`, `ω₀_sq`
`kineticEnergy` 📖	CompOp	—
`m` 📖	CompOp	2 math math: `m_pos`, `ω₀_sq`
`potentialEnergy` 📖	CompOp	—
`γ` 📖	CompOp	1 math math: `γ_nonneg`
`ω₀` 📖	CompOp	2 math math: `ω₀_pos`, `ω₀_sq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`k_neq_zero` 📖	—	—	—	—	`k_pos`
`k_pos` 📖	mathematical	—	`k`	—	—
`m_neq_zero` 📖	—	—	—	—	`m_pos`
`m_pos` 📖	mathematical	—	`m`	—	—
`γ_nonneg` 📖	mathematical	—	`γ`	—	—
`ω₀_pos` 📖	mathematical	—	`ω₀`	—	`k_pos` `m_pos`
`ω₀_sq` 📖	mathematical	—	`ω₀` `k` `m`	—	`ω₀.eq_1` `k_pos` `m_pos`

---

← Back to Index