⚜ PRINCIPIA ORTHOGONA · Book XXI · ch 1 ← contents
Book XXI · chapter 1 · rung 21

What “the Same System” Means

Similarity is the standard test for “one map in different coordinates”, and it has a decision procedure. The corpus claimed identity across domains for two years without running it.
SourceSpiral.lean
report spiral.axioms.txt
Checked10 theorems, no sorryAx
nothing outside [propext, Classical.choice, Quot.sound]
Toolchainlean 4.33.0-rc1 · Mathlib v4.33.0-rc1
the repository pins v4.32.0; see the audit log
A computation over eleven rows is evidence about eleven rows, and it depends on the table having been parsed correctly. This chapter holds the theorem the computation was an instance of.

1 · The discriminant does all the classifying

Strogatz classifies a planar linear system by two numbers: the trace τ and the determinant Δ. Writing the system in the real normal form for eigenvalues μ ± iω — rotation by ω, scaled by μ — gives τ = 2μ and Δ = μ² + ω², and so

discriminant : τ² − 4Δ = −4ω²

That is negative with no further hypothesis available. The system spirals as soon as ω ≠ 0 (is_spiral), and it is a sink exactly when μ < 0 (is_sink_iff). So “spiral sink” is the entire shared description, and it is very weak: eleven damped oscillators picked at random would satisfy it.

2 · Similarity cannot move the invariants

Conjugating by an invertible matrix leaves the trace alone (trace_of_conj) and the determinant alone (det_of_conj). Since τ and Δ are 2μ and μ² + ω², the pair (μ, ω²) belongs to the system and not to the chart.

similar_forces_same_invariants : P⁻¹ · spiral μ ω · P = spiral μ′ ω′ → μ = μ′ ∧ ω² = ω′²
The form used against the table different_mu_not_similar — if the two μ differ, there is no invertible matrix at all taking one system to the other. Not approximately. Not up to anything.

The corpus's own closest pair is instantiated directly, so nothing is left resting on arithmetic:

immune_is_not_market : μ = −0.44 against −0.67 — no such P exists

Across the eleven bridge rows carrying both μ and ω that is 0 similar pairs out of 55, and 0 again when the clock is allowed to rescale.

One direction only, and deliberately Different invariants forbid similarity. The converse — same invariants imply similarity — needs rational canonical form and is not proved here. It would only be wanted to show that two rows are the same, and none are.

3 · What the eleven do share, and why it carries nothing

Every planar linear spiral sink is topologically conjugate to every other. That is true of all eleven, and it is true of any eleven damped oscillators, so it distinguishes nothing. The claim was true at the level where it says nothing and false at every level where it would say something.

4 · The citation

Strogatz, Nonlinear Dynamics and Chaos (2018), sha256 e4c3681c…, 532 pp. §5.2 “Classification of Linear Systems”, printed pp. 129–138; the discriminant on pp. 132, 135, 138; the classification diagram at Figure 5.2.8, p. 138. spiral-pages-verify.py opens the file and finds them, and refuses outright on a sha mismatch — because every page number above then describes a copy the reader does not have.

A phrase withdrawn A first draft called §5.2 “the trace–determinant plane”. It is not in this printing. Strogatz gives the diagram without naming the plane, and common usage is not a quotation.
Proved · kernel-checked
det_of_conj book21/Spiral.lean:98
different_mu_not_similar book21/Spiral.lean:130
discriminant book21/Spiral.lean:75
immune_is_not_market book21/Spiral.lean:142
is_sink_iff book21/Spiral.lean:85
is_spiral book21/Spiral.lean:79
similar_forces_same_invariants book21/Spiral.lean:111
trace_of_conj book21/Spiral.lean:92 Each name above is declared in this repository at the line shown and appears in an axiom report with no sorryAx. A clean axiom report is not a reading of the statement: per R20, a theorem can assume its conclusion and still report clean. Follow the link before citing one as evidence.