marches

Working name — provisional. A march is a border region defined by its boundary law; renaming is a maintainer decision, not a technical one.

Claim (pinned at its actual level)

marches makes the inter-region discipline of a routed network the typed object: region-crossing well-formedness is a typing judgment on traces (Marches.Trace), and ill-typed crossings are unconstructible — they have no derivation — rather than detected and filtered.

Accepted by the Lean kernel through lake build (Lean 4, v4.35.0, no Mathlib; one dependency, tropical-types). This is Lean-leg evidence only; PROOF-STATUS.adoc gives the receipt and its scope:

• Every well-typed non-empty cross-region trace strictly worsens (trace_worsens, Marches/Compose.lean).

• A well-typed trace that returns to its start is empty — no well-typed routing loop exists, by construction (wt_cycles_are_empty).

• The ill-typed moves — crossing back from B, firing an A-label inside B — are underivable (no_back_cross, no_a_label_in_B).

• Single-region loop-freedom under strict inflation (no_return, Marches/Kernel.lean).

• The Gao–Rexford table never improves a route; strictness fails exactly at (fromCust, c); the valley dies at the type level (Marches/GaoRexford.lean, finite, by decide).

• DISAGREE — the classical smallest oscillator — both violates the discipline and demonstrably oscillates (Marches/BadGadget.lean; the #eval prints the period-2 orbit). The types reject exactly the policies that misbehave.

• A region crossing is a cut: in an acyclic region DAG every crossing in a well-typed trace leaves a cut and never re-enters it, and the composite restricted to a cut prefix is itself a discipline whose traces are exactly those ending in the prefix (Marches/Cut.lean).

What this is NOT

This is not a convergence proof for BGP or any deployed protocol. Mechanised routing algebras with full asynchronous convergence results already exist and are much deeper on that axis — see LIMITATIONS.adoc (agda-routing foremost). The residue claimed here is the typing-judgment framing: composition discipline as types, ill-typed states unconstructible, and the bridges into this estate’s attestation and graded machinery (see ROADMAP.adoc).

Status table

PROVEN in this table means the Lean kernel accepted the proof and it uses no axioms. PROVEN-WITH-AXIOMS means the kernel accepted it and it rests on the Lean built-in axioms named in the row. Under the estate proof policy marches is theory, so Agda is the source of truth and no theorem here is graded yet. PROOF-STATUS.adoc records each witness leg, the axiom census, the scope of the Lean receipt, and the plan for the Agda port.

Claim	Status	Discharged by
Well-typed non-empty traces strictly worsen	PROVEN	lake build → Compose.trace_worsens
Well-typed returning traces are empty	PROVEN	Compose.wt_cycles_are_empty
Ill-typed moves underivable	PROVEN	Compose.no_back_cross, Compose.no_a_label_in_B
Single-region loop-freedom	PROVEN	Kernel.no_return
GR table inflationary; strictness gap at (fromCust, c); valley → ⊥	PROVEN-WITH-AXIOMS (finite; propext)	GaoRexford.gr_inflationary, gr_not_strict, valley_dies
DISAGREE rejected by discipline ∧ oscillates	PROVEN + TESTED	BadGadget.disagree_not_inflationary, disagree_two_cycle, #eval orbit
GR crossings as typing judgment ≡ valley-freedom grammar ≡ non-⊥ table	PROVEN; PROVEN-WITH-AXIOMS (propext) for valley_free_iff_gwalk	GRTrace.gtrace_iff_valley_free, GRTrace.valley_free_iff_gwalk
GR ill-typed moves (valley, second peer hop, from-⊥) underivable	PROVEN	GRTrace.no_valley_step, no_peer_reexport_up, no_second_peer, no_step_from_bot
GR (node, signature) loop-freedom under acyclic hierarchy	PROVEN (conditional)	GRHierarchy.gr_loop_free — consumes Acyclic as an explicit hypothesis
Acyclic customer→provider hierarchy in real topologies	ASSUMED	named GRHierarchy.Acyclic; hypothesis of gr_loop_free, never proven here (as in Gao–Rexford 2001)
Within-region strictness load-bearing (falsifier F2)	PROVEN	Freewheel.f2_discharged — well-typed non-empty returning trace once hA is dropped
Any strictly inflationary path algebra is a Discipline	PROVEN	Reassembly.PathAlgebra.toDiscipline, toDiscipline_no_loop
A finite acyclic DAG of disciplines is itself a discipline (reassembly = closure under composition)	PROVEN	Reassembly.DiscSys.compose; composites nest via Reassembly.nestedComposed
n-region composite loop-freedom under an acyclic region DAG	PROVEN (conditional)	Reassembly.DiscSys.compose_no_loop — consumes Acyclic S.E
n-region ill-typed moves (foreign local label, DAG self-edge) underivable	PROVEN	Reassembly.DiscSys.no_foreign_local, no_self_cross
Acyclic region DAG in real deployments	ASSUMED	Marches.Acyclic — hypothesis of compose, the SAME notion as the GR hierarchy’s; never proven here
Every DAG edge crosses the principal cut of its source; an edge on a cycle crosses no cut	PROVEN (conditional)	Cut.edge_crosses_past — consumes Acyclic; Cut.path_back_crosses_no_cut
Every crossing in a well-typed trace crosses a cut that holds the trace’s start and not its end; a trace that leaves a cut never re-enters it	PROVEN (conditional)	Cut.DiscSys.trace_cross_crosses_cut, DiscSys.no_reentry; two-region Interface: trace_cross_crosses_cut, trace_stays_in_B
compose restricted to a cut prefix is a discipline; its traces are exactly the composite’s traces that end in the prefix	PROVEN (conditional)	Cut.DiscSys.composeCut, composeCut_trace_embed, composeCut_trace_reflect
TropicalNat as a (min,+) grade satisfies 𝟙 ⊗ x = x and x ⊕ x = x (the two laws K-CUT-LOSS uses); its better runs against its ⊕-induced order	PROVEN	Tropical.TropicalGrade.seq_unitl, alt_idem, better_reverses_altLe, altLe_one, s3_witness
In one tropical region the end signature of a run is the start ⊗ the grade its word carried, and a non-empty word carries a non-unit grade	PROVEN	Provenance.TropicalGrade.run_eq_seq_carried, carried_cons_ne_one, no_return_of_carried
A well-typed two-region trace that crosses is an A-word, the crossing, then a B-word; what crosses is the A-signature at the crossing, which B sees only through τ (its fibre is Interface.fibre)	PROVEN	Provenance.trace_cross_shape, Interface.carried, trace_cross_lands
In the region DAG, the grade reaching a point inside a cut, or a crossing out of ↓r, is accumulated by a trace of the cut prefix alone	PROVEN (conditional)	Provenance.DiscSys.carried_in_cut, carried_to_cross_in_past; conditional on Acyclic, as every compose theorem is
A collapsing crossing forgets the A-grade, and the fibre over the landing point still tells two such traces apart	PROVEN (finite)	Provenance.ProvenanceExhibit.zero_forgets, zero_fibre_distinguishes, collapse₀, collapse₁; id_carries for the identity crossing
marches' cuts and grade laws correspond to choreographic-types' K-CUT (proj-cut, cut-projectable, K-4), and its crossing fibre to echo-types' Echo and provenance theorems	ASSUMED (port-and-reprove)	docs/kcut-correspondence.adoc. A table of names, not a link. Names are checked at their pins by scripts/check-correspondence.sh. Falsifier F6 is open and has already withdrawn one proposed pairing.
Tropical estate integration: tropical-types' TropicalAdapterPath.lean builds inside this repo, unparaphrased, and its pathCost is marches' grade accumulation under the bottleneck grade	PROVEN-WITH-AXIOMS (propext, Quot.sound)	lake build with the lakefile.toml require; TropicalAdapter.pathCost_eq_accum, pathCost_append_via_accum, carried_floor, bottleneck_carries_unit
The bottleneck grade gives no loop-freedom: a non-empty path can carry the unit	PROVEN-WITH-AXIOMS (finite; propext)	TropicalAdapter.bottleneck_carries_unit
Protocol-level asynchronous convergence	OUT OF SCOPE	occupied by agda-routing — see LIMITATIONS.adoc

Anti-Goodhart clause: a status may only be upgraded by naming the transcribable artifact that discharges it. lake build output is the artifact for PROVEN rows. No fabricated identifiers.

Build

elan default leanprover/lean4:v4.35.0   # or let lake read lean-toolchain
lake build

No Mathlib; the one dependency is tropical-types, pinned in lakefile.toml. CI runs the same build.

scripts/check-correspondence.sh fetches the sibling proof repositories at their pinned commits (into _build/dependencies). It checks that every name docs/kcut-correspondence.adoc cites exists, and it needs network access.

Pins track latest, weekly, through reviewed PRs:

• actions-lock.yml relocks .github/workflows/actions.lock.

• track-lean.yml tries the newest stable Lean against the three gates.

• track-siblings.yml re-checks the correspondence against each sibling’s HEAD and re-pins when every name still exists.

A red result opens an issue instead of a PR.

Module map

• Marches/Basic.lean — path algebras, strict/non-strict inflation, run.

• Marches/Kernel.lean — single-region loop-freedom.

• Marches/Compose.lean — headline: typed crossing, stratified order, Step/Trace judgments, positive and negative theorems.

• Marches/Digraph.lean — RPath and Acyclic: the one explicit acyclicity hypothesis shared by the GR hierarchy and the region DAG.

• Marches/GaoRexford.lean — the commercial-relationship finite exhibit.

• Marches/GRTrace.lean — rung 1: GR relationships as typed crossings; the typing judgment is the valley-freedom grammar.

• Marches/GRHierarchy.lean — rung 1: the acyclicity hypothesis made explicit; conditional loop-freedom (gr_loop_free).

• Marches/BadGadget.lean — DISAGREE, the negative pincer.

• Marches/Freewheel.lean — rung 1: falsifier F2 discharged; strictness is load-bearing.

• Marches/Tropical.lean — (min,+) instance and its grade reading (the two K-4 laws, the S-3 order direction); seam for the estate’s tropical work.

• Marches/Reassembly.lean — rung 2 headline: Discipline, generic loop-freedom, PathAlgebra.toDiscipline, and DiscSys.compose — a finite acyclic DAG of disciplines is itself a discipline (reassembly as closure under composition).

• Marches/Cut.lean — rung 3: cuts of the region DAG; every crossing crosses a cut, traces never re-enter a cut they have left, and compose restricted to a cut prefix is a discipline (prefix-closure).

• Marches/Provenance.lean — rung 3e: what a trace carries. Words accumulate a grade (a monoid homomorphism); a tropical run ends at start ⊗ carried; a crossing trace is A-word, crossing, B-word, and carries the A-signature into the fibre of τ; in the DAG the grade reaching a cut or a crossing is accumulated inside the prefix.

• Marches/TropicalAdapter.lean — rung 3d: imports tropical-types' TropicalAdapterPath unparaphrased (a lake require); its min-max ⊗ is a marches Grade, and its pathCost is that grade’s accumulation.

Licence

Dual MIT + Palimpsest (per estate convention; see hyperpolymath/palimpsest-license). LICENSE text: TODO — copy from the licence repo; do not improvise it.