Repository navigation
Phase 1.3: ⊕-mono-<-right not provable for naive _⊕_ at limit α #34
Description
Summary
The Echidna design search (docs/echidna-design-search-2026-04-28.adoc) lists ⊕-mono-<-right : ∀ α {β γ} → β <′ γ → α ⊕ β <′ α ⊕ γ as a Phase 1.3 deliverable, claiming it is "structural on α." Hand-tracing through the recursive _≤′_ definition (Ordinal.Brouwer.Phase13) shows the limit-α case is not provable for the naive left-recursive _⊕_ defined in Ordinal.Brouwer.Arithmetic.
Counterexample
Take α = ω = olim nat-to-ord, β = oz, γ = osuc oz.
By definitions:
ω ⊕ oz = olim (λ n → nat-to-ord n ⊕ oz) = olim nat-to-ord = ωω ⊕ osuc oz = olim (λ n → nat-to-ord n ⊕ osuc oz) = olim (λ n → nat-to-ord (suc n))
To prove ω ⊕ oz <′ ω ⊕ osuc oz we need osuc ω ≤′ olim (λ n → nat-to-ord (suc n)), which by the _≤′_ clause for osuc _ ≤′ olim _ requires a Σ k. osuc ω ≤′ nat-to-ord (suc k) = Σ k. ω ≤′ nat-to-ord k. But ω ≤′ nat-to-ord k = (m : ℕ) → nat-to-ord m ≤′ nat-to-ord k, which fails for m > k (osuc^(m−k) oz ≤′ oz = ⊥).
So no k works, and ω ⊕ oz ≮′ ω ⊕ osuc oz. The strict-mono-right lemma is false at this α.
Why this matters
RankBrouwer.agda's preamble closes the <ᵇʳᶠ-ψα and <ᵇʳᶠ-+2 cases of rank-mono via this lemma. Both can produce a limit α at the call site:
<ᵇʳᶠ-ψαwithν = ω:ω-rank ω = olim nat-to-ord(limit).<ᵇʳᶠ-+2:rank x ⊕ rank yis a limit when the left rank is.
So the unbudgeted wf-<ᵇʳᶠ chain (Subrelation.wellFounded rank-mono (InverseImage.wellFounded rank wf-<)) can not close as currently scoped.
Fix options
(A) Right-recursive _⊕_ — recurse on β instead of α:
α ⊕ oz = α
α ⊕ osuc β = osuc (α ⊕ β)
α ⊕ olim f = olim (λ n → α ⊕ f n)Trivially right-strict-mono by induction on γ. Smallest mathematical change. Need to recheck psi-rank/ω-rank consequences (currently shaped around left-recursion).
(B) Hessenberg / natural sum — commutative + bi-monotonic. The Arithmetic preamble explicitly deferred this ("more machinery than pays off for the rank we actually need"). Heavier but cleanest semantically.
(C) Reshape rank so rank x is never a limit — wrap bOmega rank in osuc (and propagate). Keeps _⊕_ as is. Smallest blast radius for _⊕_, but every downstream use of ω-rank ν now carries an extra osuc.
Recommendation
(A). Right-recursive _⊕_ is the smallest change that makes the lemma true as stated, doesn't touch the rank shape that the SA + swarm already converged on, and lines up with how _≤′_'s recursion already favours the right argument (≤-trans "induct on γ first" — same intuition). Would also make ⊕-mono-≤-right hold via the same induction.
Where this discovery sits
Found while planning the work in the 2026-05-01 session handoff (P3 — Phase 1.3 arithmetic side). The Echidna design doc is otherwise sound; this is a single-line claim that did not survive contact with the recursive _≤′_ definitions actually shipped in Phase13.agda. No _⊕_ proof was attempted in this session — blocked here.
Activity
hyperpolymath commentedon May 11, 2026
Resolved — fixable via option A. Full implementation plan below.
Counterexample confirmed
The hand-trace is correct. With left-recursive
_⊕_, computing the goalω ⊕ oz <′ ω ⊕ osuc oz(i.e.osuc ω ≤′ olim (λ n → nat-to-ord (suc n)))requires by the
osuc _ ≤′ olim _clause a witnessΣ k. ω ≤′ nat-to-ord k,i.e.
∀ m. nat-to-ord m ≤′ nat-to-ord k, which fails form = suc k.The lemma is genuinely false for the current definition.
Fix: right-recursive
_⊕_inArithmetic.agdaThe recursion direction now mirrors
_≤′_'s second-argument structure, so thethree cases of
β <′ γalign exactly with the three cases ofα ⊕ γ.Why
⊕-mono-<-rightis provable after the changeProve
⊕-mono-<-right : β <′ γ → α ⊕ β <′ α ⊕ γ(i.e.
osuc (α ⊕ β) ≤′ α ⊕ γ) by induction onγ:γ = oz: hypothesisosuc β ≤′ oz = ⊥, vacuous.γ = osuc γ': hypothesisβ ≤′ γ'; goalα ⊕ β ≤′ α ⊕ γ';discharged by companion
⊕-mono-≤-right.γ = olim g: hypothesisΣ n, osuc β ≤′ g n; goalosuc (α ⊕ β) ≤′ olim (λ n → α ⊕ g n);apply
≤′-limat the witnessn, reducing toosuc (α ⊕ β) ≤′ α ⊕ g n;closed by IH on
g n(structural subterm). ✓The same structural argument on
γ(with secondary induction onβ) gives⊕-mono-≤-right : β ≤′ γ → α ⊕ β ≤′ α ⊕ γ.Helper lemmas for
Phase13.agdaTwo helpers are needed, both straightforward:
≤′-weaken-osucis needed to thread theosucstep in⊕-left-≤-sum'sosuc γ'case;⊕-left-≤-sumis needed for theβ = ozbase case of⊕-mono-≤-right(goal isα ⊕ oz = α ≤′ α ⊕ γ).Collateral breakage in
Arithmetic.agda⊕-oz-left : ∀ β → oz ⊕ β ≡ βmust be removed:oz ⊕ osuc βnowreduces to
osuc (oz ⊕ β), notosuc β, so the identity is propositionalrather than definitional. Nothing in
RankBrouwer.agdaorPhase13.agdauses this equation.
The right-unit law
α ⊕ oz = αis now definitional — the identity thatactually matters for
rank-mono.psi-rankguarantee is unaffectedω-rank ν < psi-rank ν αrequiresω-rank ν ≤′ ω-rank ν ⊕ α, which isexactly
⊕-left-≤-sum. No change to thepsi-rankdefinition or shape.Closing chain
Once
⊕-mono-<-rightlands:<ᵇʳᶠ-ψα:rank (bpsi ν α) = osuc (ω-rank ν ⊕ rank α); descentα <ᵇʳᶠ βmaps to⊕-mono-<-righton the right argument. ✓<ᵇʳᶠ-+2:rank (bplus x y) = rank x ⊕ rank y; descenty <ᵇʳᶠ zmaps to
⊕-mono-<-rightwithα = rank x. ✓closes.
Not impossible. Recommend proceeding with option A.
hyperpolymath commentedon May 11, 2026
Resolved — fixable via option A. Full implementation plan below.
Counterexample confirmed
The hand-trace is correct. With left-recursive
_⊕_, computing the goalω ⊕ oz <′ ω ⊕ osuc oz(i.e.osuc ω ≤′ olim (λ n → nat-to-ord (suc n)))requires by the
osuc _ ≤′ olim _clause a witnessΣ k. ω ≤′ nat-to-ord k,i.e.
∀ m. nat-to-ord m ≤′ nat-to-ord k, which fails form = suc k.The lemma is genuinely false for the current definition.
Fix: right-recursive
_⊕_inArithmetic.agdaThe recursion direction now mirrors
_≤′_'s second-argument structure, so thethree cases of
β <′ γalign exactly with the three cases ofα ⊕ γ.Why
⊕-mono-<-rightis provable after the changeProve
⊕-mono-<-right : β <′ γ → α ⊕ β <′ α ⊕ γ(i.e.
osuc (α ⊕ β) ≤′ α ⊕ γ) by induction onγ:γ = oz: hypothesisosuc β ≤′ oz = ⊥, vacuous.γ = osuc γ': hypothesisβ ≤′ γ'; goalα ⊕ β ≤′ α ⊕ γ';discharged by companion
⊕-mono-≤-right.γ = olim g: hypothesisΣ n, osuc β ≤′ g n; goalosuc (α ⊕ β) ≤′ olim (λ n → α ⊕ g n);apply
≤′-limat the witnessn, reducing toosuc (α ⊕ β) ≤′ α ⊕ g n;closed by IH on
g n(structural subterm). ✓The same structural argument on
γ(with secondary induction onβ) gives⊕-mono-≤-right : β ≤′ γ → α ⊕ β ≤′ α ⊕ γ.Helper lemmas for
Phase13.agdaTwo helpers are needed, both straightforward:
≤′-weaken-osucis needed to thread theosucstep in⊕-left-≤-sum'sosuc γ'case;⊕-left-≤-sumis needed for theβ = ozbase case of⊕-mono-≤-right(goal isα ⊕ oz = α ≤′ α ⊕ γ).Collateral breakage in
Arithmetic.agda⊕-oz-left : ∀ β → oz ⊕ β ≡ βmust be removed:oz ⊕ osuc βnowreduces to
osuc (oz ⊕ β), notosuc β, so the identity is propositionalrather than definitional. Nothing in
RankBrouwer.agdaorPhase13.agdauses this equation.
The right-unit law
α ⊕ oz = αis now definitional — the identity thatactually matters for
rank-mono.psi-rankguarantee is unaffectedω-rank ν < psi-rank ν αrequiresω-rank ν ≤′ ω-rank ν ⊕ α, which isexactly
⊕-left-≤-sum. No change to thepsi-rankdefinition or shape.Closing chain
Once
⊕-mono-<-rightlands:<ᵇʳᶠ-ψα:rank (bpsi ν α) = osuc (ω-rank ν ⊕ rank α); descentα <ᵇʳᶠ βmaps to⊕-mono-<-righton the right argument. ✓<ᵇʳᶠ-+2:rank (bplus x y) = rank x ⊕ rank y; descenty <ᵇʳᶠ zmaps to
⊕-mono-<-rightwithα = rank x. ✓closes.
Not impossible. Recommend proceeding with option A.
fix: right-recursive _⊕_ + Phase 1.3 right-monotonicity lemmas (issue #…
fix: right-recursive _oplus_ + Phase 1.3 right-monotonicity (closes #34…
agda(arithmetic): Phase 1.3 ⊕-mono-<-right smoke pin + restore Brouwe…
ci: repin standards reusables to 75bd5994, record them in actions.lock (