-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathMain.lean
More file actions
212 lines (160 loc) · 9.23 KB
/
Main.lean
File metadata and controls
212 lines (160 loc) · 9.23 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
import SGC.Spectral.Envelope
import SGC.Spectral.Defs
import SGC.Renormalization.Lumpability
import SGC.Renormalization.Approximate
import SGC.Thermodynamics.DoobMeyer
import SGC.Variational.LeastAction
import SGC.Information.Equivalence
import SGC.Observables.ValidityHorizon
import SGC.Observables.TopologicalPersistence
import SGC.Observables.EnergyUnification
import Mathlib.LinearAlgebra.Matrix.Notation
open Matrix SGC Real SGC.Spectral SGC.Approximate
/-!
# Sanity Checks for SGC Library
This file serves two purposes:
1. **Axiom Transparency**: `#print axioms` reveals exactly what each theorem depends on
2. **Non-Vacuity**: Concrete instantiations prove our structures are satisfiable
These checks protect against "hallucinated proofs" where definitions are vacuously
true or proofs smuggle in hidden assumptions.
-/
section AxiomAudit
/-! ## Axiom Audit
The following commands print the axioms used by key theorems.
Expected: `propext`, `Quot.sound`, `Classical.choice` (standard Lean/Mathlib axioms)
plus any explicitly declared axioms from `SGC.Bridge.Discretization`.
Red flag: If `sorry` appears, the proof is incomplete.
-/
-- Spectral Pillar (Core Stability Result)
#print axioms SGC.Spectral.spectral_stability_bound
-- Renormalization Pillar (Dirichlet Gap - algebraic)
#print axioms dirichlet_gap_non_decrease
-- Effective Theory (Approximate Lumpability)
-- trajectory_closure_bound: THE CORE VICTORY - valid for ALL generators
#print axioms SGC.Approximate.trajectory_closure_bound
#print axioms SGC.Approximate.NCD_uniform_error_bound
-- spectral_stability_reversible: Only valid for reversible (self-adjoint) generators
#print axioms SGC.Approximate.spectral_stability_reversible
-- Thermodynamics Pillar
#print axioms doob_decomposition
-- Variational Pillar
#print axioms variational_drift_optimality
-- Topology Pillar (Blanket Structure)
#print axioms SGC.blanket_orthogonality
-- Information Bridge (v2 Extension)
#print axioms SGC.information_geometry_equivalence
-- Observables Pillar (NEW January 2026)
-- Spectral Bridge: Connects abstract spectral gap to measurable autocorrelation
#print axioms SGC.Observables.autocorrelation_decay_from_sector
-- Zero Emergence Theorem (REVERSIBLE ONLY): Defect=0 ⟹ Constant Curvature
#print axioms SGC.Observables.zero_defect_implies_constant_curvature
-- Topological Persistence: Markov blanket ⟹ positive survival time
#print axioms SGC.Observables.expected_persistence_time_pos
#print axioms SGC.Observables.persistence_cost_ratio_constant
-- Energy Unification Triangle
#print axioms SGC.Observables.energy_unification_triangle
end AxiomAudit
section ConcreteInstantiation
/-! ## Concrete Instantiation (Definition Non-Vacuity)
These examples prove our **definitions** are satisfiable — they can be instantiated
with real data. If definitions like `Matrix` or `Setoid` were vacuously true
(e.g., required `False`), these would fail to compile.
**Note**: Applying theorems like `gap_non_decrease` to these examples would require
constructing complex hypotheses (`IsStronglyLumpable`, `Nonempty` sets, etc.).
The `#print axioms` audit above is the ground truth for theorem verification.
-/
/-- A simple 2-state Markov chain (coin flip dynamics). -/
def twoStateGenerator : Matrix (Fin 2) (Fin 2) ℝ :=
![![-1, 1], ![1, -1]]
/-- Uniform distribution on 2 states. -/
noncomputable def uniformDist2 : Fin 2 → ℝ := fun _ => 1/2
/-- The trivial partition: each state in its own block. -/
def trivialPartition2 : Setoid (Fin 2) := ⟨Eq, ⟨Eq.refl, Eq.symm, Eq.trans⟩⟩
/-- The coarse partition: all states in one block. -/
def coarsePartition2 : Setoid (Fin 2) := ⟨fun _ _ => True, ⟨fun _ => trivial, fun _ => trivial, fun _ _ => trivial⟩⟩
end ConcreteInstantiation
section ComputationalPropertyTests
/-! ## Computational Property Tests
These tests verify mathematical properties **numerically**, not just type-theoretically.
Unlike the axiom audit (which verifies logical dependencies), these tests compute
actual values and assert correctness.
**Key distinction:**
- Axiom audit: "Does this theorem depend only on standard axioms?"
- Property test: "Does this concrete example satisfy the mathematical definition?"
**Why this matters:** A vacuous definition could type-check but fail numerical tests.
These tests use `Rat` (exact rationals) for reproducible arithmetic.
**Test Design:**
- **Positive tests**: Valid examples that MUST pass
- **Negative tests**: Invalid examples that MUST fail (proves tests have teeth)
-/
open Matrix
/-- A 2-state symmetric Markov generator (coin-flip dynamics).
L = [[-1, 1], [1, -1]] with uniform stationary distribution. -/
def testGenerator : Matrix (Fin 2) (Fin 2) Rat :=
!![(-1 : Rat), 1; 1, -1]
/-- Uniform stationary distribution on 2 states. -/
def testStationary : Fin 2 → Rat := fun _ => 1/2
/-- A BAD "generator" (identity matrix) - row sums are NOT zero.
This MUST fail the generator property test. -/
def badGenerator : Matrix (Fin 2) (Fin 2) Rat :=
!![(1 : Rat), 0; 0, 1]
/-- A WRONG stationary distribution for testGenerator.
This MUST fail the stationarity test. -/
def wrongStationary : Fin 2 → Rat := fun i => if i = 0 then 1 else 0
/-! ### Property Checkers -/
/-- Check that all row sums equal zero (Markov generator property).
A matrix L is a generator iff Σⱼ L_ij = 0 for all i. -/
def checkRowSumsZero (L : Matrix (Fin 2) (Fin 2) Rat) : Bool :=
(L 0 0 + L 0 1 == 0) && (L 1 0 + L 1 1 == 0)
/-- Check πL = 0 (stationary distribution property).
π is stationary for L iff Σᵢ π_i L_ij = 0 for all j. -/
def checkStationary (pi : Fin 2 → Rat) (L : Matrix (Fin 2) (Fin 2) Rat) : Bool :=
let col0 := pi 0 * L 0 0 + pi 1 * L 1 0
let col1 := pi 0 * L 0 1 + pi 1 * L 1 1
(col0 == 0) && (col1 == 0)
/-- Check π is a valid probability distribution (positive, normalized). -/
def checkProbabilityDist (pi : Fin 2 → Rat) : Bool :=
(pi 0 > 0) && (pi 1 > 0) && (pi 0 + pi 1 == 1)
/-- Check detailed balance: π_i L_ij = π_j L_ji (reversibility). -/
def checkDetailedBalance (pi : Fin 2 → Rat) (L : Matrix (Fin 2) (Fin 2) Rat) : Bool :=
pi 0 * L 0 1 == pi 1 * L 1 0
/-! ### Execute Tests -/
-- Positive tests (all should return true)
#eval checkRowSumsZero testGenerator -- Expected: true
#eval checkStationary testStationary testGenerator -- Expected: true
#eval checkProbabilityDist testStationary -- Expected: true
#eval checkDetailedBalance testStationary testGenerator -- Expected: true
-- Negative tests (all should return false - PROVES TESTS HAVE TEETH)
#eval checkRowSumsZero badGenerator -- Expected: false (row sums = 1, not 0)
#eval checkStationary wrongStationary testGenerator -- Expected: false (not stationary)
/-- Run all property tests and report results. -/
def runPropertyTests : IO Unit := do
IO.println "┌─────────────────────────────────────────────────────────┐"
IO.println "│ COMPUTATIONAL PROPERTY TESTS │"
IO.println "├─────────────────────────────────────────────────────────┤"
-- Positive tests
let t1 := checkRowSumsZero testGenerator
let t2 := checkStationary testStationary testGenerator
let t3 := checkProbabilityDist testStationary
let t4 := checkDetailedBalance testStationary testGenerator
IO.println s!"│ Generator row sums = 0: {if t1 then "✓ PASS" else "✗ FAIL"} │"
IO.println s!"│ πL = 0 (stationarity): {if t2 then "✓ PASS" else "✗ FAIL"} │"
IO.println s!"│ π valid probability dist: {if t3 then "✓ PASS" else "✗ FAIL"} │"
IO.println s!"│ Detailed balance (πᵢLᵢⱼ=πⱼLⱼᵢ): {if t4 then "✓ PASS" else "✗ FAIL"} │"
-- Negative tests (these SHOULD fail)
let n1 := checkRowSumsZero badGenerator
let n2 := checkStationary wrongStationary testGenerator
IO.println "├─────────────────────────────────────────────────────────┤"
IO.println "│ NEGATIVE TESTS (must fail to prove tests have teeth) │"
IO.println s!"│ Bad generator rejected: {if !n1 then "✓ PASS" else "✗ FAIL"} │"
IO.println s!"│ Wrong stationary rejected: {if !n2 then "✓ PASS" else "✗ FAIL"} │"
let allPass := t1 && t2 && t3 && t4 && !n1 && !n2
IO.println "├─────────────────────────────────────────────────────────┤"
IO.println s!"│ ALL PROPERTY TESTS: {if allPass then "✓ PASS" else "✗ FAIL"} │"
IO.println "└─────────────────────────────────────────────────────────┘"
#eval runPropertyTests
end ComputationalPropertyTests
/-! ## Success Message
This runs during elaboration, so interpreter users see it.
-/
#eval IO.println "✓ SGC sanity checks passed. All structures are non-vacuous."