Loop-space geometry

The motivating question

Two loops can solve the same task and still be very different.

One loop might:

• ask the verifier again
• collect one more example
• and continue almost unchanged

Another loop might:

• change the witness basis
• collapse the task into ambiguity classes
• and then run a much smaller controller on what remains

That difference is the reason to talk about loop-space geometry.

The best current bounded results suggest that the strongest loops are usually not just:

• better prompts
• larger models
• or a bigger verifier budget

They are stronger because they reshape the remaining search problem.

Part I: the main axes of loop space

A neuro-symbolic loop can be factored into at least six axes.

• Witness language: what counts as an admissible failure, trace, or local certificate
• Stored state: what the loop keeps after collecting evidence
• Ambiguity quotient: which hidden targets still look the same after that state is stored
• Separator language: what extra questions, tests, or residual policies are allowed above the quotient
• Label basis: the coordinates in which the loop names outcomes
• Target artifact: what reusable symbolic object the loop is trying to compile

That factorization is useful because it separates changes that are often mixed together in informal descriptions.

The cleanest mental model is a sequence of compressions:

1. observe failures or witnesses
2. store them in a state
3. collapse the hidden family into ambiguity classes
4. run the smallest separator policy needed above that quotient
5. compile the surviving structure into a controller, question policy, or regime law

The point is not speed alone. A geometry-changing loop reshapes what remains to be searched.

Part II: the first big correction

The simplest story says:

• collect counterexamples
• repair the missing part
• ask a stakeholder when needed

The bounded results correct that story.

After saturated witness collection, the right object is not a bag of examples. It is an observation map:

O_W(M) = {S in W | S ⊆ M}

where:

• W is a witness library
• M is the hidden target, for example a missing requirement set

That moves the loop from example collection to quotient construction.

Two hidden targets are equivalent for the loop when they induce the same observation state:

M ~ M'  iff  O_W(M) = O_W(M')

A plain direct controller acts on the raw target family. A geometry-changing loop acts on this quotient first, then controls only the residue.

Part III: the requirements-discovery case study

The requirements case study is the clearest worked example.

Its core question is:

When a counterexample exposes a missing requirement, how much of the repair is already determined by witness structure, and how much still needs follow-up questions?

Three bounded corrections matter here.

1. Pure recovery is not only about singleton witnesses

The first step says direct recovery works when every missing requirement has a singleton witness. That is real, but it is not the whole story.

Even without singleton witnesses, pure recovery can still succeed if the full observation map is injective on the omission family.

So the real question is whether the stored state already separates the hidden targets, not only whether a singleton witness exists.

2. Scope matters sharply

On unrestricted omission families, singleton witnesses remain a global bottleneck.

On scoped families, especially pair-lobotomy families, oracle help becomes strictly stronger.

That means requirements discovery is not one monolithic task. The omission family changes the loop geometry.

3. Pair basis plus good separators is a real hybrid

Once the witness library contains all pairs:

• the residual ambiguity collapses to singleton uncertainty
• the remaining difficulty moves to separator language

Then the bounded ladder becomes:

• pair-subset queries, no help
• singleton-membership queries, linear depth
• block-intersection queries, logarithmic depth

That is the first clean example of a loop becoming stronger by changing geometry first and only then using a stronger residual controller.

Interactive labs

• Requirements Loop Geometry Lab
• Hybrid Loop Comparison Lab

Part IV: temporal labels are also part of loop space

Loop-space geometry is not only about witnesses and separators.

It also includes the label basis.

The temporal-label result shows a small but important result:

• raw monitor-cell labels are strictly finer than flat two-step trace labels on the full family
• after the right first coarse split, the richer temporal basis stops buying a finer partition

That means a stronger basis is not always the right global basis. Sometimes it is the right second-stage basis.

The easiest analogy is coordinates in geometry.

Polar coordinates can be the right language for one subproblem and the wrong language for another. Temporal labels behave the same way in this bounded loop setting.

Part V: graph-side compilers

The corrected graph line teaches a different lesson.

At first it looked like a large collection of unrelated graph families. After the corrected total-domination metric, the analysis compressed much more sharply.

The stable bounded survivors group into three families:

Multipartite family results:

• complete multipartite families on the corrected frontier
• repaired multipartite additivity
• a corrected small-domain single-block compiler
• a structurally explained point correction at (7, 9)

Low-edge family results:

• exact low-edge and repaired-block optimizers
• a full-star-plus-low-edge family compiler

Cross-family results:

• a wider two-family overlap compiler on the checked high band

So loop space contains exact regime compilers, not only question policies, verifier front-ends, and witness languages.

Part VI: the low-edge concentration mechanism

The newest part of the graph line is the clearest “show what was achieved” story.

It no longer says only:

• a balanced star forest fits the checked frontier

It now has a mechanism.

Stage 1: starify components

Here “starify” means: turn each connected component into a star-shaped graph, one hub with several leaves, without changing the bounded objective being optimized.

On checked connected trees, every non-star class has an improving pendant-subtree move.

The analysis then compresses further:

• on checked trees with n in {8, 9}, the improving move can always be chosen so that the reattachment target is a maximum-degree hub
• and on the same checked domain, the moved subtree can be chosen with at most one internal fork
  • leaf-only moves fail
  • pure pendant-star moves fail

So the surviving move language is not “some local repair happens somewhere.” It is:

• move a pendant subtree with one internal fork toward a hub

Stage 2: balance star sizes

Once component shape is concentrated, the star-family product law can be optimized exactly by balancing component sizes.

That gives a second clean stage:

• smooth an uneven star profile into the balanced one

The composed result

The checked low-edge analysis is now a two-stage concentration process:

1. starify components
2. balance star sizes

The newer composition result tightens that from a teaching paraphrase into the checked mechanism itself. On the checked low-edge forest family, those are the two surviving stages.

The tree-side subproblem then tightened through several steps, each narrowing the surviving move language further.

First, on the checked tree domain, the whole monotone path to the star can stay inside the smaller move language, repeatedly moving pendant subtrees (a subtree hanging from one cut edge) with one internal fork into hubs.

Second, the path still survives if each step uses a smallest available hub-target move of that same form.

Third, there is an exact checked depth cutoff on that local controller. Depth 0 fails, depth 1 fails, and depth 2 is the smallest surviving bound on the checked tree domain. The terminal-cherry ladder family is the named witness: its smallest surviving hub-target move has branching depth exactly h, so the h = 2 case is the clean family-level reason depth 1 fails and depth 2 survives.

Finally, on the same checked domain, every move selected by that depth-2 controller falls into one finite rooted alphabet of five templates: leaf, cherry (a hub with two leaves), three-leaf star, broom-1 (a star with one extended arm), and broom-2 (a star with two extended arms). The full five-template set is the unique surviving controller subset on the checked domain.

The exceptional route also compressed

Most checked low-edge states follow that stable depth-2 controller directly.

One checked two-fan state does not:

• NTF(2, 8, 2) on n = 13

Earlier, that state looked like a named escape route through several intermediate families. That was already useful, but it still looked like a route table.

The newer collapse is cleaner. On the feeder side, the exact amount separates into:

• a Fibonacci growth term
• and a repeating period-4 correction

In symbols:

B(r, t) = A_r F_t + B_r F_{t + 1} + C_r cos(pi t / 2) + A_r sin(pi t / 2)

and the full deficit to the final star is:

Delta(r, t) = 2^(r + t + 5) - 1 - B(r, t)

So the exceptional route is no longer only a chain of checked moves. It now has a compact symbolic description:

• exponential target term
• minus Fibonacci-periodic feeder term

That is a much better fit for loop-space geometry. Once the right structural coordinates are found, the route becomes simple enough to compile.

Interactive lab

• Graph Regime Compiler Lab

Part VII: what these bounded results have already achieved

The stable bounded ladder that is now strong enough to teach runs through four main ideas.

1. Observation quotients
   • the loop should be analyzed through the state it stores, not only through the examples it sees
2. Witness-basis and separator ladders
   • pair bases, separator expressivity, and staged label choices are real loop axes
3. Exact regime compilers
   • some problems compress into exact piecewise families rather than into one monolithic controller
4. Concentration mechanisms
   • some strong loops work by reshaping the problem in stages before the final exact law is even applied

Together, these give the strongest bounded reason so far that useful neuro-symbolic loops exist beyond plain verifier-compilation.

Related tutorials

• Tutorial 27: Verifier-compiler loops
• Tutorial 30: Counterexample-guided requirements discovery
• Tutorial 31: Hybrid geometry-changing loops
• Tutorial 32: Temporal label functions and staged bases