# Puncture graphs and loop generation

The kernel now checks the statement that **every based loop in the finite
puncture graph merely has a finite signed-word representation**. It also checks
that loop invariants preserving concatenation are determined by generator
values, that every additive period is the winding-weighted sum of its local
values, and that winding numbers do not classify all loops.

These are theorems about a constructed **homotopy type**. The comparison with
continuous paths in a punctured complex domain has not been proved. Neither
the free-group normal-form theorem nor the residue theorem is asserted here.

## The type and its paths

```text
def Bouquet(A : U0) = Suspension(Unit or A);
def PunctureGraph(n : Nat) = Bouquet(Fin(n));
```

The suspension has two points, `bouquet_base` and `bouquet_tip`, a distinguished
spoke from the `Unit` label, and another edge for each label in `A`. The
generator for `a : A` goes along its edge and returns along the inverse of the
distinguished spoke. There are therefore n labelled generating loops in
`PunctureGraph(n)`.

`bouquet_map` sends these generators to any supplied family of loops in another
small type. `bouquet_map_generator` proves its computation on each generator.
The graph, generators, maps, and computation theorem require no axioms; they
use the existing higher-inductive suspension kernel rules.

The underlying set of complex numbers minus a finite set is **not** being
identified with this higher type. Its continuous paths would first have to be
related to these identity paths by a geometric comparison theorem. In
particular, removing points from a set type does not create identity loops.

## The generation theorem

[bouquet_generation.cubist](../web/proofs/bouquet_generation.cubist) proves:

```text
theorem every_puncture_loop_generated(
  n : Nat, p : bouquet_base(Fin(n)) = bouquet_base(Fin(n))) :
  Mere(exists word : Word(Fin(n)),
    eval_word(Fin(n), PunctureGraph(n), bouquet_base(Fin(n)),
      puncture_loop(n), word) = p)
```

`Word(A)` is a natural length together with a finite snoc list of signed
letters. A positive letter traverses its generator; a negative letter traverses
the inverse. `word_backtrack_cancels` proves that appending a letter followed by
its reverse preserves the evaluated loop.

The statement quantifies over the **actual identity loop space** of the
suspension. It does not define loops to be words and then assert that they are
words. It neither assumes generation nor introduces a free-group axiom.

The proof proceeds as follows:

1. Construct an auxiliary family on the suspension, with the existing loop
   space as its fiber at each pole. Each labelled edge acts on the fiber by
   appending a generator, using its checked half-adjoint equivalence.
2. Define the proposition that a fiber element has a word representation.
   Appending generators or inverse generators preserves this proposition.
3. Use proposition extensionality and suspension induction to extend this
   predicate over the family.
4. Transport the proof that the constant loop is represented along any loop.
5. Decode transport back to the original loop and obtain its mere word
   representation.

`bouquet_connected` separately proves mere existence of a connector from the
base to every point. `bouquet_path_generated` handles paths with arbitrary
endpoints when connectors to those endpoints are supplied: close the path to a
based loop, represent that loop, and reopen it. No simultaneous selection of
connectors is made.

The conclusion is truncated. This proof does not select a word, compute a
canonical reduced word, prove uniqueness of reduced words, or prove that the
loop space is a set. Those stronger statements require further proofs.

## Loop invariants and the eventual residue argument

[bouquet_invariants.cubist](../web/proofs/bouquet_invariants.cubist) proves
`bouquet_maps_determined_by_generators`. Suppose `h` and `k` map loops into a
set `G`, preserve the constant loop and concatenation, and agree on each
positive generator. If the target operation has right cancellation, then
`h(p) = k(p)` for every loop `p`.

Right cancellation determines inverse-generator values; induction on word
length determines word values; the generation theorem extends the result to
all loops. Elimination of mere word existence is valid because the equality
being proved is a proposition (`G` is a set).

The target can live in `U1`, which accommodates complex numbers built from
our intended proposition-valued Dedekind reals. The supporting
`small_mere_eliminate` lemma uses the existing universe-lowering truncation
signature, as explained in [the real-number foundation notes](reals.md).

[puncture_periods.cubist](../web/proofs/puncture_periods.cubist) now proves the
explicit formula for every based loop `p`:

```text
period(p) = sum over i : Fin(n) of
  integer_multiple(values(i), puncture_winding(n, i, p))
```

Here `G` is any set in `U1` with abelian-group addition, `period` preserves
the constant loop and concatenation, and `values(i)` is its value on generator
`i`. Signed integer multiples and finite sums are constructed by recursion;
their additivity and the single-supported-term sum are proved without axioms.
The winding sum is then proved additive and equal to `values(i)` on generator
`i`. The existing generation theorem extends that equality to all paths. No
representative word is selected, and no uniqueness of words is needed.

[complex_periods.cubist](../web/proofs/complex_periods.cubist) specializes this
result to complex addition, with local values `normalization * residues(i)`.
The normalization is a parameter: its eventual value `2*pi*i` has not been
constructed. This is the homotopy reduction of the residue formula, not yet
the analytic residue theorem. Applying it to integration still requires
constructing the integral, proving that it descends to these homotopy paths
and respects concatenation, relating analytic contours to the graph, and
calculating the local generator integrals. These facts are not axioms.

The development uses homotopy types and their identity paths wherever they
describe the relevant deformation information. In particular, the period
domain here is the actual based loop space of the puncture homotopy type,
rather than a replacement definition of loops as words or winding vectors.
Geometric and analytic constructions must supply and justify the comparison
with this type. The same approach guides the circle obstruction for algebraic
closure and the puncture topology needed later for Picard.

The [limit and descent development](analysis_limits.md) now proves a way to
construct the required period. `homotopy_limit_period` starts with Cauchy
approximations on representatives, not functions already invariant under
homotopy at every finite stage. It descends their limits to actual identity
loops and proves the period laws from vanishing homotopy, constant-loop, and
concatenation errors. Geometric coverage and these analytic estimates are
still explicit proof obligations; no representative is selected from mere
existence.

[Finite contour sums](contour_sums.md) provide the next analytic ingredient:
checked composition, telescoping, and exact refinement-error identities.
They remain sampling data on representatives. In particular, a checked
nonzero coarse backtracking sum illustrates why homotopy invariance must be
proved for the limit before applying the period formula.

## Winding and a checked counterexample

[puncture_winding.cubist](../web/proofs/puncture_winding.cubist) maps the selected
generator to our existing `S1` loop and the other generators to the constant
loop. Applying the existing circle winding map gives an integer. The source
proves that the selected generator has winding +1, its reverse has winding -1,
and other generators have winding zero. Winding is additive under concatenation.
It follows that generators are nontrivial and distinct.

[puncture_noncommutative.cubist](../web/proofs/puncture_noncommutative.cubist)
constructs two generators `a`, `b` and their commutator `a b a⁻¹ b⁻¹`. It proves:

- The generators do not commute.
- The commutator is not the constant loop.
- Its winding is zero around **every** one of the two labelled punctures.

Nontriviality is witnessed by a local system with three states. Generator `a`
acts by swapping states 0 and 1, and generator `b` swaps 0 and 2. Transport
around the commutator sends state 0 to state 2. The constant loop fixes state 0,
and the two states are provably distinct. This uses explicit finite permutations,
not a postulated free-group classification.

[puncture_period_examples.cubist](../web/proofs/puncture_period_examples.cubist)
now also proves that every additive period vanishes on this noncontractible
commutator. More generally, equal winding vectors imply equal additive
periods, and zero winding implies zero period. These statements do not assert
equality of paths: an additive measurement retains less information than the
full homotopy type. Reversing a generator negates its period.

## Assumptions and modules

No kernel rules or new axiom declarations were added. The generation proof uses
the single univalence axiom, function extensionality,
and propositional truncation (constructor, introduction, propositionhood, and
elimination). It uses neither excluded middle nor choice. The noncommutativity
witness only needs univalence; its zero-winding
proof additionally uses function extensionality.

| Module | Purpose |
| --- | --- |
| `path_actions` | Path append equivalences, functoriality, and closing/reopening paths |
| `loop_words` | Signed words, evaluation, backtrack cancellation, and folds |
| `puncture_graph` | Labelled bouquet, generators, and generator maps |
| `bouquet_cover` | Auxiliary loop-space family and decoding |
| `bouquet_generation` | Generation of all loops and paths with connectors |
| `bouquet_invariants` | Determination of invariants by generator values |
| `bouquet_actions` | Local systems from families of equivalences |
| `puncture_winding` | Integer winding around each label |
| `puncture_noncommutative` | Nontrivial commutator with zero winding vector |
| `integer_multiples` | Axiom-free signed multiples in abelian groups |
| `finite_sums` | Axiom-free finite sum laws and single-supported-term sums |
| `puncture_periods` | Every additive period is its winding-weighted local sum |
| `complex_periods` | Specialization to complex-valued periods and local contributions |
| `puncture_period_examples` | Zero period of a noncontractible loop; reversal changes sign |

Open `proof.html?proof=puncture_periods`, `proof.html?proof=complex_periods`, or
`proof.html?proof=puncture_noncommutative` in the web source explorer. Each proof
is checked from source, and its axiom dependencies can be inspected individually.

The next geometric milestone is a constructive comparison with a plane or disk
with a finite, labelled, pairwise separated collection of points removed.
Continuity, path gluing, controlled deformations, and their comparison with the
graph remain mathematical proof obligations. A general shape modality is not
part of the current kernel and is not assumed here.