6. Taming spurious behaviors

In this lesson: why the honest answer is sometimes a mess, where the mess comes from, and how to soundly clean it up.

The promise, revisited

Lesson 1 warned that the library's output can contain spurious behaviors — extra paths no real system follows. Now we meet them head-on, because the frictionless spring is where they famously appear.

In Lesson 5 the practical profile kept landmark discovery off and produced one clean cycle. Select textbook QSIM discovery explicitly and watch what happens:

import qrlib as qr
# ... spring model `m`, `initial` as in Lesson 5 ...

result = qr.qsim(
    m,
    initial,
    config=qr.SimConfig.classic(max_states=22),
)
print(result.status)          # SimStatus.TRUNCATED  — it didn't finish!
print(len(result.behaviors()))

The spring's spurious branching

That sprawling tree is a genuine problem. The real frictionless spring has one behavior — a steady oscillation. Where did all these come from?

Where the mess comes from: landmark discovery

Landmark discovery is a powerful feature: when a variable goes steady at a value that has no name yet — like the exact height of the spring's first peak — the library invents a landmark for it (x*0, x*1, …) so it can reason about later peaks relative to it.

But here's the rub. When the spring reaches its second peak, is that peak higher than, equal to, or lower than the first? Pure qualitative reasoning can't tell — all three are consistent with "a spring swings back and forth." So it branches three ways. And again at the next peak. And the next. The result is the explosion above: spurious growing and shrinking oscillations that no real frictionless spring exhibits, plus unbounded invention of new landmarks (which is why we had to cap it with max_states).

This is the coverage guarantee being scrupulously honest: it will not rule out the growing oscillation, because nothing in the bare qualitative model forbids it. To rule it out, we must add knowledge.

Cleaning up soundly: the energy argument

The knowledge we're missing is energy conservation. A frictionless spring keeps the same energy, so it must return to the same amplitude every swing — it cannot spontaneously grow or shrink. That single physical fact collapses the whole mess.

The library ships this as a ready-made filter, EnergyFilter:

tamed = qr.qsim(
    m,
    initial,
    config=qr.SimConfig.classic(
        successor_filters=(qr.EnergyFilter(),),
    ),
)
print(tamed.status)              # SimStatus.COMPLETE
print(len(tamed.behaviors()))    # 1

The spring, tamed to its true cycle

One behavior — the true oscillation. The EnergyFilter enforces that turning points don't drift: once the first peak is discovered, later peaks must match it. Growing and shrinking swings are pruned as inconsistent with conservation.

EnergyFilter has two modes:

EnergyFilter() — conserved (the default): amplitude is pinned, as for the frictionless spring.
EnergyFilter(trend="nonincreasing") — dissipative: amplitude may shrink but never grow, as for a spring with friction.

A filter can only remove behaviors, never invent them. That preserves the coverage guarantee only when the filter's physical premise is true of every system represented by the model. EnergyFilter() is sound for a genuinely conservative spring; applying it to a driven spring could remove a real growing-amplitude behavior and therefore invalidate coverage. Treat a filter like any other model constraint: it is trusted knowledge, not a heuristic.

Strict decrease inside one qualitative interval

EnergyFilter(trend="nonincreasing") rules out amplitude growth, but it does not assert that an explicit Lyapunov scalar makes strict progress. A numeric scalar may decrease while staying in the same open magnitude interval, so a plain qualitative state can appear to repeat. Use LyapunovCertificate for that proof pattern:

certificate = qr.LyapunovCertificate(
    "V",
    minimum="0",
    equilibrium={"angle": "0", "velocity": "0"},
    strict_when=(("velocity", "!=", "0"),),
)
strict_config = qr.SimConfig(successor_filters=(certificate,))
# result = qr.qsim(model_with_V, initial, config=strict_config)
# assert result.stats["lyapunov_cycles_filtered"] > 0

Here the model contains the scalar V and its qualitative derivative. The certificate requires V to be nonincreasing, requires V.dir == DEC whenever velocity != 0, and requires V to reach its 0 landmark exactly at the declared equilibrium. A proposed recurrence is rejected if the condition was active somewhere around the cycle; isolated turning points with velocity == 0 may still have a zero derivative.

If strict_when is omitted, strict decrease is required at every state outside the equilibrium. Conditions are conjunctions of landmark predicates using ==, !=, <, >, <=, or >=. This is a trusted analytic certificate, not something inferred from the QDE. It is path-dependent, so use tree-mode QSIM rather than envisionment=True.

A second source of clutter: chatter

Sometimes a variable's direction wobbles meaninglessly — increasing, decreasing, steady, back again — without anything observable depending on it. This is called chatter, and it multiplies behaviors just like discovery does. The practical profile detects chattering variables automatically and abstracts their direction away:

result = qr.qsim(m, initial)  # SimConfig.practical()

To combine chatter abstraction with classic landmark discovery, request both controls explicitly:

config = qr.SimConfig(
    discover_landmarks=True,
    dynamic_chatter=True,
)

Unlike the energy filter, dynamic chatter does not assert new physics. It detects direction distinctions that the active constraint structure cannot observe, merges successors that differ only in those directions, and records the merged direction as Qdir.IGN. Variables named in temporal direction properties or phase-plane filters remain tracked.

The takeaway

The practical profile starts with a sound abstraction that avoids the two largest sources of accidental growth. Select SimConfig.classic() when the extra landmark distinctions are the question being studied, then add trusted knowledge such as energy or phase arguments to prune classic QSIM's spurious branches.

Exercises

Run the spring three ways: SimConfig.practical(); SimConfig.classic(max_states=22); and the classic profile with EnergyFilter(). Record the status and behavior count of each. Which distinctions does each profile preserve?
Explain why EnergyFilter preserves coverage for a conservative spring but may break it when applied to a driven spring.
A ball bouncing on the floor loses a little height each bounce. Which EnergyFilter trend — conserved or nonincreasing — matches it?

Next: 7. The soundness guarantee →