// SPDX-License-Identifier: MPL-2.0
// SPDX-License-Identifier: CC-BY-SA-4.0

= marches
:toc: macro

*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.

Machine-checked, in this repository, by `lake build` (Lean 4, v4.35.0,
no dependencies):

* 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

[cols="3,1,2"]
|===
|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 (finite)
|`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
|`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
|`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 (finite)
|`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

[source,shell]
----
elan default leanprover/lean4:v4.35.0   # or let lake read lean-toolchain
lake build
----

Zero dependencies; no mathlib. 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.