Constraint Resonance State Evolution
Constraint Resonance State Evolution
CRSE · Public Package 003
This package machine-checks a legacy CRSE stability statement against the existing native architecture. The audit does not assume the original statement is correct: where the original hypotheses are insufficient, explicit counterexamples are constructed and the missing conditions are isolated.
State Evolution
The theorem reuses CRSE's existing discrete state, legal-neighborhood, score, deterministic commitment, metric, and potential machinery without replacing native definitions. The discrete state is State = ZMod 12; the metric state is m = [c, τ, l, μ, φ].
The package adds a closed RecoveryCorridor, a StableBasin, deterministic and induced-metric evolution predicates, and assumption bundles used to state the repaired stability results.
Legacy Statement
A1 — Field legality. Forbidden edges are excluded by the native legal-neighborhood machinery.
A2 — Prototype alignment. Existence of a legal recovery edge that would decrease potential is not sufficient to guarantee descent, because existence does not imply selection.
A3 — Hysteresis lower bound. A strictly positive threshold is available, but by itself it does not bound switching.
Repaired Selection Bridge
The missing bridge is explicit: the recovery edge must be the unique maximizer of the native score over the legal neighborhood, and its score margin must clear the hysteresis gate. The package records this strengthened condition as DominantRecoveryEdge.
corridor_strict_descent then proves strict descent for the successor that native deterministic evolution actually selects whenever the state is outside the stable set and the metric lies in the recovery corridor but outside the stable basin.
Finite-Time Result
If the potential is nonnegative and decreases by at least a fixed ε > 0 at every step before entry, exists_basin_entry_time proves an entry time T satisfying:
Entry into the stated basin additionally requires compatibility between the basin thresholds and a potential sublevel. The package proves the exact sufficient threshold inequalities rather than identifying “small potential” with basin membership by assumption.
Conditional Stability
A1–A3 alone do not imply non-increasing potential after basin entry. The missing condition is native non-escalation on the committed stabilizing edge, reused from PrototypeAlignment.stab_reduces.
lyapunov_stability_in_basin gives the verified sublevel form: with threshold compatibility and non-increasing potential, sufficiently small potential-level perturbations remain in the stable basin. No stronger perturbation statement is claimed.
Formal Failure Modes
Selection failure. stallConfig satisfies the legacy legality, recovery-edge-existence and positive-hysteresis assumptions, yet equal candidate scores prevent the gate from opening; potential does not descend.
Basin escalation. switchConfig shows that positive hysteresis does not by itself prevent a committed edge from increasing potential inside the basin.
Switching. The same construction proves that a positive hysteresis lower bound alone does not bound switching; switching depends on the threshold relative to available score gaps.
No-runaway. Bounded turbulence, intensity and friction control only three of the five potential terms. Coherence and momentum can independently drive unbounded potential. Adding bounds on |1−c| and negative momentum yields an explicit finite cap.
Machine-Checked Results
Formal Artifact
The public source below is the verified module RequestProject/CRSEStabilityTheorem.lean, namespace ResonantEvolution.CRSEStability.
import RequestProject.DeterministicDecision
import RequestProject.Potential
open scoped BigOperators
open scoped Real
open scoped Classical
set_option maxHeartbeats 1000000
set_option relaxedAutoImplicit false
set_option autoImplicit false
/-!
# CRSE Stability Theorem v1 — corridor descent, basin entry and stability
This file is a purely downstream *formal verification* of the legacy
"Corridor Convergence and Stability" theorem package against the existing
Constrained Resonant State Evolution (CRSE) architecture. Nothing native is
changed: the atlas `State`, the circular distance `cdist`, the adjacency field
`Config.A`, the legal neighbourhood `legalNbhd`, the resonance kernel, the
native `score`, the hysteresis gate `committedState`, the deterministic
selector `DeterministicDecision.deterministicStepState`, and the coherence
potential `potential` of `RequestProject/Potential.lean` are all reused
verbatim.
## Source mapping
| legacy object | native interface |
| --- | --- |
| `s_t ∈ S = {s₀,…,s₁₁}` | `State = ZMod 12` |
| `N_r(s) = {u : (s→u) ∈ A, d(s,u) ≤ r}` | `legalNbhd` |
| `m = [c, τ, l, μ, φ]` | `Metric = Fin 5 → ℝ` with `coh, turb, intens, mom, fric` |
| `V(m) = a(1−c)² + b(τ−τ*)₊² + d(l−ℓ*)₊² + e(−μ)₊² + f(φ*−φ)₊²` | `potential` |
| recovery corridor `R = {τ ≤ τ_R, l ≤ l_R, φ ≥ φ_R}` | `RecoveryCorridor` (closed variant of the native `RecoveryRegion`) |
| stable basin `B = {c ≥ c_S, τ ≤ τ_S, l ≤ l_S}` | `StableBasin` |
| `argmax` + hysteresis commitment | `deterministicStepState` |
The only genuinely new *definitions* are the stable basin `B` and the closed
recovery corridor `R` (the native `RecoveryRegion` uses a strict friction
inequality `φ_R < φ`; `recoveryRegion_subset_recoveryCorridor` records that the
native region is contained in the closed corridor used by the legacy text), plus
the assumption bundles A2 / A2⁺ / A3 and the induced metric dynamics.
## Assumption audit (summary; details in `CRSEStabilityTheorem_Report.md`)
* **(1) Strict descent in the corridor is NOT implied by A1–A3.** A2 only
asserts the *existence* of a legal recovery edge; the score-and-hysteresis
rule may select a different successor — in particular it may refuse to move at
all. `stall_no_strict_descent` (with `stall_recoveryEdgeAvailable`,
`stall_hysteresis`, `stallConfig_valid`) is an explicit configuration
satisfying A1, A2 and A3 in which the committed successor leaves the potential
unchanged, so no `ε > 0` descent holds. The exact missing implication is a
*selection* hypothesis; `descent_of_dominant_recovery_edge` isolates the
minimal sufficient form (the recovery edge is the unique argmax and clears the
gate) and `corridor_strict_descent` is the resulting corridor theorem.
* **(2) Finite-time basin entry holds** once descent holds at every step before
the first basin entry: `exists_basin_entry_time`, with exactly the claimed
bound `T ≤ V(m₀)/ε`. Entry into the *stated* basin additionally needs the
threshold-compatibility condition `{V ≤ η} ⊆ B`
(`mem_stableBasin_of_potential_le`).
* **(3) Stability inside the basin is NOT implied by A1–A3**
(`basin_escalation_counterexample`); it requires a non-escalation hypothesis
on the committed edge, which is the native `PrototypeAlignment.stab_reduces`
(`basin_drift_nonpos_of_stabilizing`). Lyapunov stability then follows in the
sublevel form `lyapunov_stability_in_basin`.
* **Switching.** A3 alone does *not* bound switching:
`hysteresis_does_not_bound_switching` exhibits a configuration with
`Δ = Δmin > 0` whose deterministic trajectory switches at every single step.
* **(4) No-runaway corollary is false as stated**
(`bounded_inputs_do_not_bound_potential`, `momentum_runaway_under_bounded_inputs`):
bounded turbulence, bounded intensity and friction above the recovery
threshold leave the coherence and momentum terms of `V` unconstrained. With
the two missing bounds added, `potential_le_of_bounded_inputs` gives an
explicit finite cap.
## Nonclaims
No change to the native score, adjacency, hysteresis rule, latent smoothing,
potential, or deterministic tie policy. No claim that CRSE is gradient descent,
that every legal recovery edge is selected, or that the legacy statements (1),
(3) and the corollary are valid as written — they are refuted here by explicit
configurations.
-/
namespace ResonantEvolution.CRSEStability
open ResonantEvolution
open ResonantEvolution.DeterministicDecision
open ResonantEvolution.SmoothErgodicReductionPartB (zeroMetric driftConfig driftConfig_succ_legal
drift_score_succ drift_score_other drift_score_lt drift_best_unique)
/-! ## 1. Definitions -/
/-- The **stable basin** `B = {m : c ≥ c_S, τ ≤ τ_S, l ≤ l_S}`. -/
def StableBasin (cS τS lS : ℝ) : Set Metric :=
{m | cS ≤ coh m ∧ turb m ≤ τS ∧ intens m ≤ lS}
/-- The **recovery corridor** `R = {m : τ ≤ τ_R, l ≤ l_R, φ ≥ φ_R}`.
This is the closed variant of the native `RecoveryRegion`, matching the legacy
`φ ≥ φ_R`; the native region (with `φ_R < φ`) is contained in it. -/
def RecoveryCorridor (τR lR φR : ℝ) : Set Metric :=
{m | turb m ≤ τR ∧ intens m ≤ lR ∧ φR ≤ fric m}
/-- The native recovery region sits inside the closed legacy corridor. -/
theorem recoveryRegion_subset_recoveryCorridor (τR lR φR : ℝ) :
RecoveryRegion τR lR φR ⊆ RecoveryCorridor τR lR φR := by
rintro m ⟨hτ, hl, hφ⟩
exact ⟨hτ, hl, le_of_lt hφ⟩
/-- A discrete state trajectory follows the **native deterministic commitment rule**
`s_{t+1} = committedState (argmax J_t)`. -/
def IsDeterministicEvolution (C : Config) (z : ℕ → Metric) (s : ℕ → State) : Prop :=
∀ t, s (t + 1) = deterministicStepState C (s t) (z t)
/-- The metric trajectory is **induced by the committed edge**:
`m_{t+1} = upd (s_t → s_{t+1}) m_t`, where `upd` is the induced metric update of
the native `PrototypeAlignment` interface. -/
def InducedMetricEvolution (upd : State → State → Metric → Metric)
(s : ℕ → State) (m : ℕ → Metric) : Prop :=
∀ t, m (t + 1) = upd (s t) (s (t + 1)) (m t)
/-! ## 2. Assumptions A1–A3 -/
/-- **A1 — field legality.** Forbidden edges are excluded from the legal
neighbourhood. This is a property of the *native* `legalNbhd`, not an extra
hypothesis. -/
theorem not_mem_legalNbhd_of_forbidden (C : Config) (s u : State) (h : ¬ C.A s u) :
u ∉ legalNbhd C s := by
simp [legalNbhd, IsLegalNeighbor, h]
/-- **A1, consequence.** The deterministic successor is always a permitted edge. -/
theorem adjacent_deterministicStepState {C : Config} (hV : ValidField C) (s : State)
(z : Metric) : C.A s (deterministicStepState C s z) :=
((mem_legalNbhd_iff C s _).1 (deterministicStepState_mem_legalNbhd hV s z)).1
/-- **A2 — prototype alignment.** Outside the stable state set, for every metric in
the recovery corridor but outside the stable basin, the legal neighbourhood contains
*at least one* recovery edge whose induced next metric lowers the potential by `ε`.
This is an *existence* statement about the legal neighbourhood; it says nothing
about which edge the score-and-hysteresis rule actually selects. -/
structure RecoveryEdgeAvailable (C : Config) (P : PotParams)
(upd : State → State → Metric → Metric) (Sstable : Set State)
(R B : Set Metric) (ε : ℝ) : Prop where
/-- The descent margin is strictly positive. -/
eps_pos : 0 < ε
/-- Existence of a legal recovery edge. -/
edge : ∀ (s : State) (m : Metric), s ∉ Sstable → m ∈ R → m ∉ B →
∃ u ∈ legalNbhd C s, potential P (upd s u m) ≤ potential P m - ε
/-- **A3 — hysteresis lower bound.** `Δ_t ≥ Δ_min > 0`. -/
structure HysteresisLowerBound (C : Config) (Δmin : ℝ) : Prop where
/-- The lower bound is strictly positive. -/
pos : 0 < Δmin
/-- The native threshold dominates it. -/
le_threshold : Δmin ≤ C.Δ
/-! ## 3. Explicit witnesses: parameters, metrics and configurations -/
/-- Unit potential parameters: all weights `1`, all targets `0`. -/
def unitParams : PotParams where
a := 1
b := 1
d := 1
e := 1
f := 1
τstar := 0
ℓstar := 0
φstar := 0
theorem unitParams_pos : unitParams.Pos :=
⟨by norm_num [unitParams], by norm_num [unitParams], by norm_num [unitParams],
by norm_num [unitParams], by norm_num [unitParams]⟩
/-- A fully coherent metric: `c = 1`, all other coordinates `0`. Its potential is `0`. -/
def goodMetric : Metric := ![1, 0, 0, 0, 0]
/-- An incoherent metric: `c = -1`, all other coordinates `0`. Its potential is `4`. -/
def coldMetric : Metric := ![-1, 0, 0, 0, 0]
theorem potential_goodMetric : potential unitParams goodMetric = 0 := by
simp [potential, unitParams, goodMetric, cohDeficit, coh, turbDeficit, turb,
intensDeficit, intens, momDeficit, mom, fricDeficit, fric]
theorem potential_zeroMetric : potential unitParams zeroMetric = 1 := by
simp [potential, unitParams, zeroMetric, cohDeficit, coh, turbDeficit, turb,
intensDeficit, intens, momDeficit, mom, fricDeficit, fric]
theorem potential_coldMetric : potential unitParams coldMetric = 4 := by
simp [potential, unitParams, coldMetric, cohDeficit, coh, turbDeficit, turb,
intensDeficit, intens, momDeficit, mom, fricDeficit, fric]
norm_num
/-- The coherence term alone is a lower bound for the potential (unit weights). -/
theorem coh_term_le_potential (m : Metric) :
(cohDeficit m) ^ 2 ≤ potential unitParams m := by
have h : (0:ℝ) ≤ (turbDeficit unitParams m) ^ 2 + (intensDeficit unitParams m) ^ 2
+ (momDeficit m) ^ 2 + (fricDeficit unitParams m) ^ 2 := by positivity
simp only [potential, unitParams]
nlinarith
/-- The circular distance to the cyclic successor is `1`. -/
theorem cdist_succ_one (s : State) : cdist s (s + 1) = 1 := by
have h : s - (s + 1) = (-1 : State) := by ring
have h11 : ((-1 : State)).val = 11 := by decide
simp [cdist, h, h11]
/-- The cyclic successor is a different state. -/
theorem succ_ne_self (s : State) : s + 1 ≠ s := by
intro h
have h1 := cdist_succ_one s
rw [h, cdist_self] at h1
exact absurd h1 (by norm_num)
/-- **The stall configuration.** All prototypes coincide, so every legal candidate has
exactly the same score and the hysteresis gate (`Δ = 1 > 0`) never opens. -/
noncomputable def stallConfig : Config where
A := fun s u => cdist s u ≤ 1
proto := fun _ _ => fun _ => 0
W := fun _ => 1
ε := 1
lam := 0
ρ := 0
r := 1
Δ := 1
/-- **The switching configuration.** The native `driftConfig` benchmark with the
hysteresis threshold raised to the exact successor margin, so that A3 holds with
`Δ_min = Δ > 0`. -/
noncomputable def switchConfig : Config :=
{ driftConfig with Δ := Real.log 2 - Real.log (Real.exp (-5) + 1) }
/-- An induced metric update that repairs coherence off the basin and escalates inside
it; staying put leaves the metric unchanged. -/
noncomputable def escalateUpd : State → State → Metric → Metric := fun s u m =>
if u = s then m else if coh m < 0 then goodMetric else zeroMetric
/-! ## 4. Theorem (1): strict descent in the recovery corridor -/
/-- The stall configuration is a valid field. -/
theorem stallConfig_valid : ValidField stallConfig where
identity := fun s => by simp [stallConfig]
localContinuity := fun _ _ h => h
/-- In the stall configuration every candidate carries the same score. -/
theorem stall_score_const (s : State) (z : Metric) (u v : State) :
score stallConfig s z u = score stallConfig s z v := by
simp [score, stallConfig]
/-- **The stall configuration never commits.** The gate `Δ = 1` cannot be cleared by a
zero score gap, so the committed successor is always the current state. -/
theorem stall_step_eq_self (s : State) (z : Metric) :
deterministicStepState stallConfig s z = s := by
refine deterministicStepState_eq_self ?_
rw [stall_score_const s z (canonicalBest stallConfig s z) s]
norm_num [stallConfig]
/-- **A3 holds for the stall configuration** with `Δ_min = 1`. -/
theorem stall_hysteresis : HysteresisLowerBound stallConfig 1 where
pos := by norm_num
le_threshold := by norm_num [stallConfig]
/-- The successor edge is legal in the stall configuration. -/
theorem stall_succ_legal (s : State) : (s + 1) ∈ legalNbhd stallConfig s := by
simp only [mem_legalNbhd_iff]
exact ⟨by simp [stallConfig, cdist_succ_one], by simp [stallConfig, cdist_succ_one]⟩
/-- **A2 holds for the stall configuration.** Every corridor metric outside the basin
admits a legal recovery edge that clears the entire potential. -/
theorem stall_recoveryEdgeAvailable :
RecoveryEdgeAvailable stallConfig unitParams escalateUpd ∅
(RecoveryCorridor 0 0 0) (StableBasin 0 0 0) (1/2) where
eps_pos := by norm_num
edge := by
rintro s m - ⟨hτ, hl, -⟩ hB
have hcoh : coh m < 0 := by
by_contra hc
exact hB ⟨le_of_not_gt hc, hτ, hl⟩
refine ⟨s + 1, stall_succ_legal s, ?_⟩
have hupd : escalateUpd s (s + 1) m = goodMetric := by
simp [escalateUpd, succ_ne_self s, hcoh]
have hlow : (1:ℝ) < potential unitParams m := by
have h := coh_term_le_potential m
have hd : (1:ℝ) < cohDeficit m := by unfold cohDeficit; linarith
nlinarith
rw [hupd, potential_goodMetric]
linarith
/-- The witness metric lies in the corridor. -/
theorem coldMetric_mem_corridor : coldMetric ∈ RecoveryCorridor 0 0 0 := by
simp [RecoveryCorridor, coldMetric, turb, intens, fric]
/-- The witness metric lies outside the basin. -/
theorem coldMetric_not_mem_basin : coldMetric ∉ StableBasin 0 0 0 := by
simp [StableBasin, coldMetric, coh]
/-- **Counterexample to legacy claim (1).** In the stall configuration — which
satisfies A1 (`stallConfig_valid`), A2 (`stall_recoveryEdgeAvailable`) and A3
(`stall_hysteresis`) — the metric `coldMetric` lies in the corridor and outside the
basin, yet the potential of the *committed* successor does not decrease at all. Hence
A1–A3 do not imply the claimed `V(m_{t+1}) ≤ V(m_t) − ε` for any `ε > 0`. -/
theorem stall_no_strict_descent (s : State) (z : Metric) {ε : ℝ} (hε : 0 < ε) :
¬ potential unitParams
(escalateUpd s (deterministicStepState stallConfig s z) coldMetric)
≤ potential unitParams coldMetric - ε := by
rw [stall_step_eq_self s z]
have hupd : escalateUpd s s coldMetric = coldMetric := by simp [escalateUpd]
rw [hupd]
linarith
/-- **Assumption audit for legacy claim (1), packaged.** A1, A2 and A3 all hold for the
stall configuration at a corridor metric outside the basin, and yet the committed
successor produces no descent whatsoever. So A1–A3 are *insufficient* for claim (1);
the missing ingredient is a selection hypothesis. -/
theorem legacy_claim_one_insufficient :
ValidField stallConfig ∧
RecoveryEdgeAvailable stallConfig unitParams escalateUpd ∅
(RecoveryCorridor 0 0 0) (StableBasin 0 0 0) (1/2) ∧
HysteresisLowerBound stallConfig 1 ∧
coldMetric ∈ RecoveryCorridor 0 0 0 ∧ coldMetric ∉ StableBasin 0 0 0 ∧
∀ (s : State) (z : Metric),
¬ potential unitParams
(escalateUpd s (deterministicStepState stallConfig s z) coldMetric)
≤ potential unitParams coldMetric - 1/2 :=
⟨stallConfig_valid, stall_recoveryEdgeAvailable, stall_hysteresis,
coldMetric_mem_corridor, coldMetric_not_mem_basin,
fun s z => stall_no_strict_descent s z (by norm_num)⟩
/-- **Selection bridge.** If the recovery edge is the *unique* argmax of the native
score and clears the native hysteresis gate, then it *is* the committed successor, and
the claimed strict descent holds for the actually selected edge. -/
theorem descent_of_dominant_recovery_edge {C : Config} {P : PotParams}
{upd : State → State → Metric → Metric} {s u : State} {z m : Metric} {ε : ℝ}
(hu : IsBestCandidate C s z u)
(huniq : ∀ b, IsBestCandidate C s z b → b = u)
(hgate : C.Δ ≤ score C s z u - score C s z s)
(hdesc : potential P (upd s u m) ≤ potential P m - ε) :
potential P (upd s (deterministicStepState C s z) m) ≤ potential P m - ε := by
have hb : canonicalBest C s z = u := canonicalBest_eq_of_unique hu huniq
have hstep : deterministicStepState C s z = u := by
rw [deterministicStepState_eq_canonicalBest (by rw [hb]; exact hgate), hb]
rw [hstep]
exact hdesc
/-- **A2⁺ — dominant recovery edge.** The strengthening of A2 identified by the
selection audit: the recovery edge is the unique score maximiser and clears the gate. -/
structure DominantRecoveryEdge (C : Config) (P : PotParams)
(upd : State → State → Metric → Metric) (Sstable : Set State)
(R B : Set Metric) (ε : ℝ) : Prop where
/-- The descent margin is strictly positive. -/
eps_pos : 0 < ε
/-- Existence of a *dominant* legal recovery edge. -/
edge : ∀ (s : State) (z m : Metric), s ∉ Sstable → m ∈ R → m ∉ B →
∃ u, IsBestCandidate C s z u ∧ (∀ b, IsBestCandidate C s z b → b = u) ∧
C.Δ ≤ score C s z u - score C s z s ∧
potential P (upd s u m) ≤ potential P m - ε
/-- **Theorem (1), refined.** Along a native deterministic evolution with induced
metric dynamics, A2⁺ yields the claimed uniform strict descent in the corridor. -/
theorem corridor_strict_descent {C : Config} {P : PotParams}
{upd : State → State → Metric → Metric} {Sstable : Set State} {R B : Set Metric}
{ε : ℝ} (hA2 : DominantRecoveryEdge C P upd Sstable R B ε)
{z : ℕ → Metric} {s : ℕ → State} {m : ℕ → Metric}
(hs : IsDeterministicEvolution C z s) (hm : InducedMetricEvolution upd s m)
{t : ℕ} (hstate : s t ∉ Sstable) (hcorr : m t ∈ R) (hbasin : m t ∉ B) :
potential P (m (t + 1)) ≤ potential P (m t) - ε := by
obtain ⟨u, hu, huniq, hgate, hdesc⟩ := hA2.edge (s t) (z t) (m t) hstate hcorr hbasin
rw [hm t, hs t]
exact descent_of_dominant_recovery_edge hu huniq hgate hdesc
/-! ## 5. Theorem (2): finite-time basin entry -/
/-- Iterated strict descent: `n` consecutive `ε`-decreases lower the value by `n·ε`. -/
theorem descent_iterate {V : ℕ → ℝ} {ε : ℝ} :
∀ {n : ℕ}, (∀ k < n, V (k + 1) ≤ V k - ε) → V n ≤ V 0 - n * ε := by
intro n
induction n with
| zero => intro _; simp
| succ n ih =>
intro h
have h1 : V n ≤ V 0 - n * ε := ih fun k hk => h k (by omega)
have h2 : V (n + 1) ≤ V n - ε := h n (by omega)
push_cast
linarith
/-- **Theorem (2) — finite-time basin entry with the claimed bound.** If the potential
is nonnegative and strictly descends by `ε > 0` at every step before the first basin
entry, then the basin is entered at a time `T ≤ V(m₀)/ε`. -/
theorem exists_basin_entry_time {P : PotParams} (hP : P.Pos) {B : Set Metric}
{m : ℕ → Metric} {ε : ℝ} (hε : 0 < ε)
(hdesc : ∀ t, (∀ k < t, m k ∉ B) → m t ∉ B →
potential P (m (t + 1)) ≤ potential P (m t) - ε) :
∃ T, m T ∈ B ∧ (T : ℝ) ≤ potential P (m 0) / ε := by
classical
have hnn : ∀ t, 0 ≤ potential P (m t) := fun t =>
potential_nonneg hP.a.le hP.b.le hP.d.le hP.e.le hP.f.le _
have hex : ∃ T, m T ∈ B := by
by_contra hno
push_neg at hno
have hd : ∀ k, potential P (m (k + 1)) ≤ potential P (m k) - ε :=
fun k => hdesc k (fun j _ => hno j) (hno k)
obtain ⟨N, hN⟩ := exists_nat_gt (potential P (m 0) / ε)
have hiter := descent_iterate (V := fun k => potential P (m k)) (n := N)
(fun k _ => hd k)
have hNε : potential P (m 0) < N * ε := by
rw [div_lt_iff₀ hε] at hN; exact hN
have := hnn N
simp only at hiter
linarith
refine ⟨Nat.find hex, Nat.find_spec hex, ?_⟩
have hbefore : ∀ k < Nat.find hex, m k ∉ B := fun k hk => Nat.find_min hex hk
have hiter := descent_iterate (V := fun k => potential P (m k))
(n := Nat.find hex)
(fun k hk => hdesc k (fun j hj => hbefore j (by omega)) (hbefore k hk))
have h0 := hnn (Nat.find hex)
rw [le_div_iff₀ hε]
simp only at hiter
linarith
/-- **Sublevel ⊆ basin.** The threshold-compatibility condition that turns "the
potential becomes small" into "the metric is in the stated basin". -/
theorem mem_stableBasin_of_potential_le {P : PotParams} (hP : P.Pos) {cS τS lS η : ℝ}
(hc : cS ≤ 1 - Real.sqrt (η / P.a))
(hτ : P.τstar + Real.sqrt (η / P.b) ≤ τS)
(hl : P.ℓstar + Real.sqrt (η / P.d) ≤ lS)
{m : Metric} (hV : potential P m ≤ η) : m ∈ StableBasin cS τS lS := by
have hbound : ∀ (w : ℝ) (x : ℝ), 0 < w → w * x ^ 2 ≤ η → x ≤ Real.sqrt (η / w) := by
intro w x hw hx
have hsq : x ^ 2 ≤ η / w := by
rw [le_div_iff₀ hw]; linarith [hx]
calc x ≤ |x| := le_abs_self x
_ = Real.sqrt (x ^ 2) := (Real.sqrt_sq_eq_abs x).symm
_ ≤ Real.sqrt (η / w) := Real.sqrt_le_sqrt hsq
have hca : P.a * (cohDeficit m) ^ 2 ≤ η := by
have hrest : (0:ℝ) ≤ P.b * (turbDeficit P m) ^ 2 + P.d * (intensDeficit P m) ^ 2
+ P.e * (momDeficit m) ^ 2 + P.f * (fricDeficit P m) ^ 2 := by
have := hP.b.le; have := hP.d.le; have := hP.e.le; have := hP.f.le
positivity
simp only [potential] at hV
linarith
have hcb : P.b * (turbDeficit P m) ^ 2 ≤ η := by
have hrest : (0:ℝ) ≤ P.a * (cohDeficit m) ^ 2 + P.d * (intensDeficit P m) ^ 2
+ P.e * (momDeficit m) ^ 2 + P.f * (fricDeficit P m) ^ 2 := by
have := hP.a.le; have := hP.d.le; have := hP.e.le; have := hP.f.le
positivity
simp only [potential] at hV
linarith
have hcd : P.d * (intensDeficit P m) ^ 2 ≤ η := by
have hrest : (0:ℝ) ≤ P.a * (cohDeficit m) ^ 2 + P.b * (turbDeficit P m) ^ 2
+ P.e * (momDeficit m) ^ 2 + P.f * (fricDeficit P m) ^ 2 := by
have := hP.a.le; have := hP.b.le; have := hP.e.le; have := hP.f.le
positivity
simp only [potential] at hV
linarith
have h1 : cohDeficit m ≤ Real.sqrt (η / P.a) := hbound _ _ hP.a hca
have h2 : turbDeficit P m ≤ Real.sqrt (η / P.b) := hbound _ _ hP.b hcb
have h3 : intensDeficit P m ≤ Real.sqrt (η / P.d) := hbound _ _ hP.d hcd
refine ⟨?_, ?_, ?_⟩
· have : 1 - coh m ≤ Real.sqrt (η / P.a) := by simpa [cohDeficit] using h1
linarith
· have : turb m - P.τstar ≤ turbDeficit P m := le_max_right _ _
linarith
· have : intens m - P.ℓstar ≤ intensDeficit P m := le_max_right _ _
linarith
/-! ## 6. Theorem (3): stability inside the basin -/
/-- The switching configuration is a valid field. -/
theorem switchConfig_valid : ValidField switchConfig where
identity := fun s => by simp [switchConfig, driftConfig]
localContinuity := fun _ _ h => h
/-- Scores are inherited verbatim from the benchmark configuration. -/
theorem switch_score_eq (s u : State) (z : Metric) :
score switchConfig s z u = score driftConfig s z u := rfl
/-- Legal neighbourhoods are inherited verbatim from the benchmark configuration. -/
theorem switch_legalNbhd (s : State) : legalNbhd switchConfig s = legalNbhd driftConfig s := rfl
/-- Best candidates are inherited verbatim from the benchmark configuration. -/
theorem switch_isBestCandidate_iff (s b : State) (z : Metric) :
IsBestCandidate switchConfig s z b ↔ IsBestCandidate driftConfig s z b := Iff.rfl
/-- **A3 holds for the switching configuration**, with `Δ_min = Δ > 0`. -/
theorem switch_hysteresis :
HysteresisLowerBound switchConfig (Real.log 2 - Real.log (Real.exp (-5) + 1)) where
pos := by have := drift_score_lt; linarith
le_threshold := le_of_eq rfl
/-- The successor edge is the unique resonant maximiser of the switching configuration. -/
theorem switch_best_succ (s : State) :
IsBestCandidate switchConfig s zeroMetric (s + 1) := by
refine ⟨driftConfig_succ_legal s, ?_⟩
intro u _
by_cases hu : u = s + 1
· rw [hu]
· rw [switch_score_eq, switch_score_eq, drift_score_succ, drift_score_other hu]
exact le_of_lt drift_score_lt
/-- **The switching configuration commits at every step**: the committed successor is
the cyclic successor, which is never the current state. -/
theorem switch_step (s : State) :
deterministicStepState switchConfig s zeroMetric = s + 1 := by
have hbest := switch_best_succ s
have hb : canonicalBest switchConfig s zeroMetric = s + 1 :=
canonicalBest_eq_of_unique hbest (fun b hb => drift_best_unique hb)
have hgate : score switchConfig s zeroMetric (canonicalBest switchConfig s zeroMetric)
- score switchConfig s zeroMetric s ≥ switchConfig.Δ := by
rw [hb, switch_score_eq, switch_score_eq, drift_score_succ,
drift_score_other (Ne.symm (succ_ne_self s))]
exact le_of_eq rfl
rw [deterministicStepState_eq_canonicalBest hgate, hb]
/-- The fully coherent metric lies in the basin. -/
theorem goodMetric_mem_basin : goodMetric ∈ StableBasin 0 0 0 := by
simp [StableBasin, goodMetric, coh, turb, intens]
/-- **Counterexample to legacy claim (3).** The switching configuration satisfies A1
(`switchConfig_valid`) and A3 (`switch_hysteresis`), and its committed edge is the
cyclic successor; with the induced update `escalateUpd` the potential *increases*
strictly inside the basin. Hence A1–A3 do not imply `V(m_{t+1}) ≤ V(m_t)` in the
basin. -/
theorem basin_escalation_counterexample (s : State) :
goodMetric ∈ StableBasin 0 0 0 ∧
potential unitParams goodMetric
< potential unitParams
(escalateUpd s (deterministicStepState switchConfig s zeroMetric) goodMetric) := by
refine ⟨goodMetric_mem_basin, ?_⟩
rw [switch_step s]
have hupd : escalateUpd s (s + 1) goodMetric = zeroMetric := by
have hcoh : ¬ coh goodMetric < 0 := by simp [goodMetric, coh]
simp [escalateUpd, succ_ne_self s, hcoh]
rw [hupd, potential_goodMetric, potential_zeroMetric]
norm_num
/-- **Assumption audit for legacy claim (3), packaged.** A1 and A3 hold for the
switching configuration, whose committed edge nevertheless raises the potential inside
the basin: A1–A3 are insufficient for claim (3). -/
theorem legacy_claim_three_insufficient :
ValidField switchConfig ∧
HysteresisLowerBound switchConfig (Real.log 2 - Real.log (Real.exp (-5) + 1)) ∧
∀ s : State, goodMetric ∈ StableBasin 0 0 0 ∧
potential unitParams goodMetric
< potential unitParams
(escalateUpd s (deterministicStepState switchConfig s zeroMetric) goodMetric) :=
⟨switchConfig_valid, switch_hysteresis, basin_escalation_counterexample⟩
/-- **Theorem (3), refined.** Under the native prototype-alignment hypothesis
(the committed edge is stabilizing) the drift inside the basin is nonpositive. -/
theorem basin_drift_nonpos_of_stabilizing {C : Config} {P : PotParams}
{upd : State → State → Metric → Metric}
{Stabilizing Escalation : State → State → Prop}
(hAlign : PrototypeAlignment C P upd Stabilizing Escalation)
{s u : State} {m : Metric} (hstab : Stabilizing s u) :
potential P (upd s u m) ≤ potential P m :=
hAlign.stab_reduces s u m hstab
/-- A nonincreasing potential keeps every sublevel set forward invariant. -/
theorem potential_le_of_nonincreasing {P : PotParams} {m : ℕ → Metric} {η : ℝ}
(hstep : ∀ t, potential P (m (t + 1)) ≤ potential P (m t))
(h0 : potential P (m 0) ≤ η) : ∀ t, potential P (m t) ≤ η := by
intro t
induction t with
| zero => exact h0
| succ n ih => exact le_trans (hstep n) ih
/-- **Lyapunov stability inside the basin.** If the initial potential is below a level
`η` compatible with the basin thresholds and the potential never increases, the whole
trajectory stays in the basin. -/
theorem lyapunov_stability_in_basin {P : PotParams} (hP : P.Pos) {cS τS lS η : ℝ}
(hc : cS ≤ 1 - Real.sqrt (η / P.a))
(hτ : P.τstar + Real.sqrt (η / P.b) ≤ τS)
(hl : P.ℓstar + Real.sqrt (η / P.d) ≤ lS)
{m : ℕ → Metric} (h0 : potential P (m 0) ≤ η)
(hstep : ∀ t, potential P (m (t + 1)) ≤ potential P (m t)) :
∀ t, m t ∈ StableBasin cS τS lS := fun t =>
mem_stableBasin_of_potential_le hP hc hτ hl (potential_le_of_nonincreasing hstep h0 t)
/-! ## 7. The switching claim -/
/-- **A3 does not bound switching.** `switchConfig` satisfies A1 and A3 with
`Δ_min = Δ > 0`, yet every deterministic trajectory driven by the constant latent
`zeroMetric` changes state at *every* step. -/
theorem hysteresis_does_not_bound_switching {s : ℕ → State}
(hs : IsDeterministicEvolution switchConfig (fun _ => zeroMetric) s) :
∀ t, s (t + 1) ≠ s t := by
intro t
rw [hs t, switch_step]
exact succ_ne_self (s t)
/-! ## 8. Corollary: no runaway under bounded inputs -/
/-- **Refuting the corollary as stated (coherence).** Bounded turbulence, bounded
intensity and friction above the recovery threshold leave the potential unbounded: the
coherence term is not controlled by the listed assumptions. -/
theorem bounded_inputs_do_not_bound_potential (M : ℝ) :
∃ m : Metric, m ∈ RecoveryCorridor 0 0 0 ∧ M < potential unitParams m := by
refine ⟨![-(|M| + 2), 0, 0, 0, 0], ⟨by simp [turb], by simp [intens],
by simp [fric]⟩, ?_⟩
have habs : M ≤ |M| := le_abs_self M
have hpos : (0:ℝ) ≤ |M| := abs_nonneg M
simp [potential, unitParams, cohDeficit, coh, turbDeficit, turb, intensDeficit,
intens, momDeficit, mom, fricDeficit, fric]
nlinarith
/-- **Refuting the corollary as stated (momentum).** Even with perfect coherence and
the same bounded inputs, the momentum term escapes. -/
theorem momentum_runaway_under_bounded_inputs (M : ℝ) :
∃ m : Metric, m ∈ RecoveryCorridor 0 0 0 ∧ coh m = 1 ∧ M < potential unitParams m := by
refine ⟨![1, 0, 0, -(|M| + 2), 0], ⟨by simp [turb], by simp [intens],
by simp [fric]⟩, by simp [coh], ?_⟩
have habs : M ≤ |M| := le_abs_self M
have hpos : (0:ℝ) ≤ |M| := abs_nonneg M
have hmax : max (0:ℝ) (|M| + 2) = |M| + 2 := max_eq_right (by positivity)
simp [potential, unitParams, cohDeficit, coh, turbDeficit, turb, intensDeficit,
intens, momDeficit, mom, fricDeficit, fric]
rw [hmax]
nlinarith
/-- **Corollary, refined.** With the two missing bounds (coherence and momentum) the
potential admits an explicit finite cap. -/
theorem potential_le_of_bounded_inputs {P : PotParams} (hP : P.Pos) {m : Metric}
{Kc τB lB μB φR : ℝ} (hKc : |1 - coh m| ≤ Kc) (hμB : 0 ≤ μB)
(hτ : turb m ≤ τB) (hl : intens m ≤ lB) (hμ : -μB ≤ mom m) (hφ : φR ≤ fric m) :
potential P m ≤ P.a * Kc ^ 2 + P.b * (max 0 (τB - P.τstar)) ^ 2
+ P.d * (max 0 (lB - P.ℓstar)) ^ 2 + P.e * μB ^ 2
+ P.f * (max 0 (P.φstar - φR)) ^ 2 := by
have hsq : ∀ x y : ℝ, 0 ≤ x → x ≤ y → x ^ 2 ≤ y ^ 2 := by
intro x y hx hxy; nlinarith
have hc : (cohDeficit m) ^ 2 ≤ Kc ^ 2 := by
have h1 : |cohDeficit m| ≤ Kc := by simpa [cohDeficit] using hKc
have h2 : (cohDeficit m) ^ 2 = |cohDeficit m| ^ 2 := (sq_abs _).symm
rw [h2]
exact hsq _ _ (abs_nonneg _) h1
have hb : (turbDeficit P m) ^ 2 ≤ (max 0 (τB - P.τstar)) ^ 2 :=
hsq _ _ (le_max_left _ _) (max_le_max le_rfl (by linarith))
have hd : (intensDeficit P m) ^ 2 ≤ (max 0 (lB - P.ℓstar)) ^ 2 :=
hsq _ _ (le_max_left _ _) (max_le_max le_rfl (by linarith))
have he : (momDeficit m) ^ 2 ≤ μB ^ 2 := by
refine hsq _ _ (le_max_left _ _) ?_
exact max_le hμB (by linarith)
have hf : (fricDeficit P m) ^ 2 ≤ (max 0 (P.φstar - φR)) ^ 2 :=
hsq _ _ (le_max_left _ _) (max_le_max le_rfl (by linarith))
simp only [potential]
have ha' := hP.a.le
have hb' := hP.b.le
have hd' := hP.d.le
have he' := hP.e.le
have hf' := hP.f.le
nlinarith [mul_le_mul_of_nonneg_left hc ha', mul_le_mul_of_nonneg_left hb hb',
mul_le_mul_of_nonneg_left hd hd', mul_le_mul_of_nonneg_left he he',
mul_le_mul_of_nonneg_left hf hf']
/-! ## 9. Axiom audit -/
#print axioms corridor_strict_descent
#print axioms descent_of_dominant_recovery_edge
#print axioms exists_basin_entry_time
#print axioms mem_stableBasin_of_potential_le
#print axioms lyapunov_stability_in_basin
#print axioms stall_no_strict_descent
#print axioms stall_recoveryEdgeAvailable
#print axioms legacy_claim_one_insufficient
#print axioms legacy_claim_three_insufficient
#print axioms basin_escalation_counterexample
#print axioms hysteresis_does_not_bound_switching
#print axioms bounded_inputs_do_not_bound_potential
#print axioms momentum_runaway_under_bounded_inputs
#print axioms potential_le_of_bounded_inputs
end ResonantEvolution.CRSEStability
Verification
Both the direct module compile and whole-project build succeed. The module contains no sorry/admit, no new axioms, no implemented_by, no native_decide, and no unsafe/partial declarations. Representative #print axioms checks report only propext, Classical.choice, and Quot.sound.
Claim Boundary
This package does not modify the native score, adjacency, hysteresis rule, latent smoothing, potential definition, or deterministic tie policy.
It does not claim that CRSE is gradient descent, that every legal recovery edge is selected, that positive hysteresis alone bounds switching, or that the legacy stability statement and no-runaway corollary were valid as originally written.
The counterexample configurations certify insufficiency of the stated hypotheses; they are not claims about any particular deployed parameterization.