Skip to content

proof(Path-3 prototype): same-left joint-bplus rank-mono extension#167

Merged
hyperpolymath merged 1 commit into
mainfrom
session/path-3-same-left-prototype
May 30, 2026
Merged

proof(Path-3 prototype): same-left joint-bplus rank-mono extension#167
hyperpolymath merged 1 commit into
mainfrom
session/path-3-same-left-prototype

Conversation

@hyperpolymath
Copy link
Copy Markdown
Owner

Summary

Mechanises the Path-3 alternative identified in PR #166's closing note: enrich the SOURCE RULE rather than the rank function. New module `Ordinal.Buchholz.RankMonoSameLeft` introduces a `<ᵇ⁰`-grounded same-left joint-bplus constructor and closes its rank-pow obligation in one line, bypassing the rank-lex-jb pivot's first-eq derivation entirely for the same-literal-left sub-case. Zero postulates, `--safe --without-K`, no funext.

The structural insight tested

PR #166's closing note flagged Path-3 as a possible reframing:

The source rule may need enrichment, not the rank function.
For a valid `<ᵇ-+1`-at-equal-head derivation under WfCNF, rank-mono soundness requires tail-rank-strict. Path-3 alternative: enrich the source side instead — promote `<ᵇ` to carry a `<ᵇ⁺-+2`-style same-left constructor with both head-eq and tail-strict premises baked in.

This PR mechanises that intuition concretely. Result: WORKS.

Headlines

Name Role
`<ᵇ⁺²` Extended relation: `<ᵇ⁺²-from-<ᵇ⁰` embeds 10 closed cases + `<ᵇ⁺²-same-left` adds the source-rule enrichment
`rank-pow-mono-<ᵇ⁺²` Two-case structural recursion: each case ONE LINE
`rank-pow-mono-same-left` Direct lemma showing the same-left case without routing through embedding

Path-3 vs rank-lex-jb (complementary, not subsuming)

Sub-case Path Closure
Same LITERAL left (`bplus x s` vs `bplus x t`) Path-3 (this PR) One-line via `rank-pow-bplus-right-mono`
Same head-Ω, different left syntax (`bpsi ν α` vs `bOmega ν`) rank-lex-jb (#147+#165+#166) Multi-step: leftmost-α + first-eq + `<lex-second`

The same-left case is UNREACHABLE in K-free `<ᵇ` (would require `<ᵇ-irrefl` violation via `<ᵇ-+1 (x <ᵇ x)`); reachable only in the extended `<ᵇ⁺` of `Ordinal.Buchholz.OrderExtended` via `<ᵇ⁺-+2`. This prototype narrows the tail premise to `<ᵇ⁰` to keep the closure inductively grounded.

The K-restriction does NOT bite at constructor formation (only at pattern-match elimination), so the same-binder `<ᵇ⁺²-same-left` constructor is fine under `--safe --without-K`.

Honest scope

  • Does NOT prove well-foundedness of `<ᵇ⁺²` — separate from rank-mono; would need a Brouwer-rank embedding (the rank function here provides the seed).
  • Does NOT subsume rank-lex-jb for the cross-head case — Path-3 and rank-lex-jb are complementary.
  • Does NOT extend the tail premise to `<ᵇ¹` — composes mechanically via `rank-pow-mono-<ᵇ¹` but kept out of the prototype for minimality.
  • Does NOT wrap in WfCNF endpoints (à la `<ᵇ⁻ⁿ` from Slice 4) — left for downstream consumers.

Implication confirmed

PR #166's #3 implication holds mechanically: enriching the source rule is structurally simpler than the rank-function enrichment for this scenario. The one-line closure here contrasts with the multi-PR rank-lex-jb assembly chain. This suggests the future bplus-chain rank-mono umbrella may want to be designed as a UNION of source-rule extensions (Path-3 style for cleanly-decomposable cases) rather than a single enriched rank function (rank-lex-jb style for cross-head cases).

Local verification

  • `agda -i proofs/agda proofs/agda/Ordinal/Buchholz/RankMonoSameLeft.agda` — clean.
  • `agda -i proofs/agda proofs/agda/Ordinal/Buchholz/Smoke.agda` — clean, exit 0.
  • `agda -i proofs/agda proofs/agda/Smoke.agda` — clean, exit 0.
  • `agda -i proofs/agda proofs/agda/All.agda` — clean, exit 0.
  • `bash tools/check-guardrails.sh proofs/agda` — 161 modules pass (one new).
  • `sh scripts/kernel-guard.sh` — PASS.

Five new names pinned in `Ordinal/Buchholz/Smoke.agda` under a new `RankMonoSameLeft` `using` block.

Test plan

  • Module typechecks under `--safe --without-K` with zero postulates.
  • Full suite + Smoke remain green with the new module wired in.
  • Foundation guardrail + kernel-guard pass with 161 modules.
  • CI: `check` + `cold-check` + governance lanes green.
  • Auto-merge on green.

🤖 Generated with Claude Code

Mechanises the Path-3 alternative identified in PR #166's closing
note: enrich the SOURCE RULE rather than the rank function.  New
module `Ordinal.Buchholz.RankMonoSameLeft` introduces a `<ᵇ⁰`-
grounded same-left joint-bplus constructor and closes its rank-pow
obligation in ONE LINE, bypassing the rank-lex-jb pivot's first-eq
derivation entirely for the same-literal-left sub-case.  Zero
postulates, `--safe --without-K`, no funext.

## The structural insight tested

PR #166's closing note flagged Path-3 as a possible reframing:

> The source rule may need enrichment, not the rank function.
> The K-free `_<ᵇ_`'s `<ᵇ-+1` constructor carries `x₁ <ᵇ y₁` as
> premise — nothing on `x₂ vs y₂`.  Yet for a valid `<ᵇ-+1`-at-
> equal-head derivation under WfCNF, rank-mono soundness
> *requires* tail-rank-strict.  Path-3 alternative: enrich the
> source side instead — promote `_<ᵇ_` to carry a `<ᵇ⁺-+2`-style
> same-left constructor with both head-eq and tail-strict premises
> baked in.

This PR mechanises that intuition concretely.  Result: WORKS.

## What the prototype contains

`data _<ᵇ⁺²_ : BT → BT → Set`:
  * `<ᵇ⁺²-from-<ᵇ⁰` — embed every `_<ᵇ⁰_` derivation (10
    inherited cases).
  * `<ᵇ⁺²-same-left` — **the source-rule enrichment**: when the
    left summand is LITERALLY equal on both sides and the right
    summand satisfies `<ᵇ⁰`, the bplus chain is in the relation.
    The K-restriction does NOT bite at constructor formation
    (only at pattern-match elimination), so this same-binder
    constructor is fine under `--safe --without-K`.

`rank-pow-mono-<ᵇ⁺²` — direct structural recursion.  The
inherited case forwards to `rank-pow-mono-<ᵇ⁰`; the same-left
case fires `rank-pow-bplus-right-mono` (= `⊕-mono-<-right`
specialised) on the tail's rank-pow strict witness.  ONE LINE
per case.

`rank-pow-mono-same-left` — convenience direct-rank-mono lemma
showing the same-left case without routing through the
embedding.  Demonstrates the one-line closure.

## Path-3 vs rank-lex-jb (complementary, not subsuming)

Path-3 covers a STRICTLY DIFFERENT sub-case than rank-lex-jb:

| Sub-case | Path | Closure |
|---|---|---|
| Same LITERAL left (`bplus x s` vs `bplus x t`) | Path-3 (this PR) | One-line `rank-pow-bplus-right-mono` |
| Same head-Ω, different left syntax (`bpsi ν α` vs `bOmega ν`) | rank-lex-jb (#147+#165+#166) | Multi-step: leftmost-α + first-eq + `<lex-second` |

Path-3's same-left is UNREACHABLE in K-free `_<ᵇ_` (would require
`<ᵇ-irrefl` violation via `<ᵇ-+1 (x <ᵇ x)`); reachable only in
the extended `_<ᵇ⁺_` of `Ordinal.Buchholz.OrderExtended` via
`<ᵇ⁺-+2`.  This prototype narrows the tail premise to `_<ᵇ⁰_`
to keep the closure inductively grounded.

## Honest scope (preserved in module preamble)

- Does NOT prove well-foundedness of `_<ᵇ⁺²_` — separate from
  rank-mono; would need a Brouwer-rank embedding (the rank
  function here provides the seed).
- Does NOT subsume rank-lex-jb for the cross-head case — Path-3
  and rank-lex-jb are complementary.
- Does NOT extend the tail premise to `_<ᵇ¹_` — composes
  mechanically via `rank-pow-mono-<ᵇ¹` but kept out of the
  prototype for minimality.
- Does NOT wrap in WfCNF endpoints (à la `_<ᵇ⁻ⁿ_` from
  Slice4) — left for downstream consumers.

## Implication confirmed

PR #166's #3 implication holds mechanically: enriching the
source rule is structurally simpler than the rank-function
enrichment for this scenario.  The one-line closure here
contrasts with the multi-PR rank-lex-jb assembly chain.  This
suggests the FUTURE bplus-chain rank-mono umbrella may want
to be designed as a UNION of source-rule extensions (Path-3
style for cleanly-decomposable cases) rather than a single
enriched rank function (rank-lex-jb style for cross-head
cases).

## Local verification

- `agda -i proofs/agda proofs/agda/Ordinal/Buchholz/RankMonoSameLeft.agda` — clean.
- `agda -i proofs/agda proofs/agda/Ordinal/Buchholz/Smoke.agda` — clean, exit 0.
- `agda -i proofs/agda proofs/agda/Smoke.agda` — clean, exit 0.
- `agda -i proofs/agda proofs/agda/All.agda` — clean, exit 0.
- `bash tools/check-guardrails.sh proofs/agda` — **161 modules** pass.
- `sh scripts/kernel-guard.sh` — PASS.

Five new names pinned in `Ordinal/Buchholz/Smoke.agda` under a
new `RankMonoSameLeft` `using` block.  Module wired into
`proofs/agda/All.agda` between `RankMonoUmbrellaSlice4` and
`RecursiveSurfaceOrder` (sibling extension to the Slice 4
narrowing).

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@hyperpolymath hyperpolymath enabled auto-merge (squash) May 30, 2026 14:32
@github-actions
Copy link
Copy Markdown

🔍 Hypatia Security Scan

Findings: 58 issues detected

Severity Count
🔴 Critical 17
🟠 High 22
🟡 Medium 19

⚠️ Action Required: Critical security issues found!

View findings
[
  {
    "reason": "No test directory or test files found",
    "type": "no_tests",
    "file": "/home/runner/work/echo-types/echo-types",
    "action": "flag",
    "rule_module": "honest_completion",
    "severity": "high",
    "deduction": 20
  },
  {
    "reason": "Issue in codeql.yml",
    "type": "missing_workflow",
    "file": "codeql.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in secret-scanner.yml",
    "type": "missing_workflow",
    "file": "secret-scanner.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Action rpolymath/standards/.github/workflows/governance-reusable.yml@main\n needs attention",
    "type": "unpinned_action",
    "file": "governance.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in agda.yml",
    "type": "unknown",
    "file": "agda.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in agda.yml",
    "type": "unknown",
    "file": "agda.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in governance.yml",
    "type": "unknown",
    "file": "governance.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in hypatia-scan.yml",
    "type": "unknown",
    "file": "hypatia-scan.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in mirror.yml",
    "type": "unknown",
    "file": "mirror.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in scorecard.yml",
    "type": "unknown",
    "file": "scorecard.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

@hyperpolymath hyperpolymath merged commit 390cebb into main May 30, 2026
12 of 13 checks passed
@hyperpolymath hyperpolymath deleted the session/path-3-same-left-prototype branch May 30, 2026 14:34
hyperpolymath added a commit that referenced this pull request May 30, 2026
…ns (#168)

## Summary

Realises the **architectural recommendation** from PR #167's closing
note: the future bplus-chain rank-mono umbrella shipped as a UNION OF
SOURCE-RULE EXTENSIONS rather than a single enriched rank function.
**Zero new proof obligations**; purely structural composition via Sum +
\`[_,_]\` mediator. \`--safe --without-K\`, no postulates, no funext.

## What the union umbrella ships

| Name | Type | Role |
|---|---|---|
| \`_<ᵇᵘ_\` | \`BT → BT → Set\` | Disjoint sum of \`_<ᵇ¹_\` (Slice 3)
and \`_<ᵇ⁺²_\` (Path-3) |
| \`rank-pow-mono-<ᵇᵘ\` | \`∀ {x y} → x <ᵇᵘ y → rank-pow x <′ rank-pow
y\` | Coproduct mediator via \`[_,_]\` — **ONE LINE** |
| \`<ᵇᵘ-from-<ᵇ¹\` / \`<ᵇᵘ-from-<ᵇ⁺²\` / \`<ᵇᵘ-from-<ᵇ⁰\` (+symmetric) |
embeddings | Convenience injections |

## The architectural design

PR #167's closing observation:

> The future bplus-chain rank-mono umbrella may want to be designed as a
UNION OF SOURCE-RULE EXTENSIONS (Path-3 style for cleanly-decomposable
cases) rather than a single enriched rank function (rank-lex-jb style
for cross-head cases).

This PR mechanises that recommendation. Each contributing extension
keeps its own proof obligation local; the union dispatches via case
analysis on which extension witnesses the relation. The mediator is \`[
rank-pow-mono-<ᵇ¹ , rank-pow-mono-<ᵇ⁺² ]\` — a single \`[_,_]\` over the
existing per-extension umbrellas.

## Why this architectural shape (three observations)

1. **Different sub-cases prefer different rank-mono machinery.**
Strict-head joint-bplus closes via head-Ω + \`ω-rank-pow-succ\`;
same-left closes via \`rank-pow-bplus-right-mono\`; cross-head
rank-equal closes at LEX-RANK via rank-lex-jb. No single rank function
dominates.

2. **Source-rule enrichment is structurally simpler than rank-function
enrichment** (Path-3 verdict, PR #167). The consumer-side first-eq
derivation that rank-lex-jb requires (PR #166 (c) trichotomy + first-eq)
gets bypassed entirely when the source rule carries the discriminator.

3. **Union of extensions scales.** Every new sub-case ships as its own
extension module with its own rank-mono theorem, then unions in
mechanically. No interference between extensions; closure is local.

## Extension recipe (for future contributors)

Documented in the module preamble. To add a new source-rule extension:

1. Define the relation + rank-pow-mono in its own module (use
\`RankMonoSameLeft\` as canonical template).
2. Re-export through \`Ordinal/Buchholz/Smoke.agda\` with its own
\`using\` block.
3. Update this module to extend \`_<ᵇᵘ_\` with the new disjunct and
extend \`rank-pow-mono-<ᵇᵘ\` with the new case via \`[_,_]\`.

Both edits mechanical; no new proof obligations.

## Honest scope (preserved in module preamble)

- Does NOT wrap with WfCNF endpoints (à la
\`RankMonoUmbrellaSlice4._<ᵇ⁻ⁿ_\`).
- Does NOT include rank-lex-jb discharge — cross-head rank-equal case
lives at LEX-RANK level, different rank-relation. Union is over
\`rank-pow <′\` discharges only.
- Does NOT prove well-foundedness of the union — orthogonal to
rank-mono.

## Slice 3+4 Route A arc summary (4 PRs total)

After this PR the session arc is closed:

| PR | Role |
|---|---|
| #165 | (b) \`<lex-first\` primitive + bpsi sub-case discharge |
| #166 | (c) trichotomy data type + first-eq derivation |
| #167 | Path-3 prototype (same-left source-rule extension) |
| **THIS PR** | **RankMonoUnion** (architectural realisation) |

The full bplus-chain rank-mono umbrella over all 13 \`_<ᵇ_\`
constructors is still gated on (i) tail-rank-equality discharge for the
bpsi-source-at-equal-head case AND (ii) the cross-head rank-equal case
via rank-lex-jb's structural research; **neither is closed by this PR**.
The architecture is now in place for those closures to plug in
mechanically.

## Local verification

- All four Agda lanes typecheck clean, exit 0.
- \`bash tools/check-guardrails.sh proofs/agda\` — **162 modules** pass.
- \`sh scripts/kernel-guard.sh\` — PASS.

Six new names pinned in \`Ordinal/Buchholz/Smoke.agda\`.

## Test plan

- [x] All Agda lanes typecheck under \`--safe --without-K\` with zero
postulates.
- [x] Foundation guardrail + kernel-guard pass with 162 modules.
- [ ] CI: \`check\` + \`cold-check\` + governance lanes green.
- [ ] Auto-merge on green.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
hyperpolymath added a commit that referenced this pull request May 30, 2026
## Summary

**Closes Gate 2 of the Slice 3+4 Route A session arc.** Derives
\`WellFounded _<ᵇᵘ_\` mechanically from \`rank-pow-mono-<ᵇᵘ\` (#168) and
the existing \`wf-<′\` via the standard Subrelation + InverseImage
transport pattern documented in \`Ordinal.Buchholz.RankBrouwer\`'s
preamble. **Zero new proof obligations**; purely structural. \`--safe
--without-K\`, no postulates, no funext.

## The rank-embedding recipe

```agda
wf-rank-pow-pullback : WellFounded (λ x y → rank-pow x <′ rank-pow y)
wf-rank-pow-pullback = On.wellFounded rank-pow wf-<′

wf-<ᵇᵘ : WellFounded _<ᵇᵘ_
wf-<ᵇᵘ = Subrelation.wellFounded rank-pow-mono-<ᵇᵘ wf-rank-pow-pullback
```

Two steps:

1. \`On.wellFounded\` (= \`InverseImage.wellFounded\`) lifts
well-foundedness of \`_<′_\` on \`Ord\` to the pullback \`_<′_ on
rank-pow\` on \`BT\`.
2. \`Subrelation.wellFounded\` transports well-foundedness from the
pullback to \`_<ᵇᵘ_\`, consuming \`rank-pow-mono-<ᵇᵘ\` as the witness
that \`_<ᵇᵘ_\` is a sub-relation of the pullback.

The pattern is documented at \`RankBrouwer.agda:55-56\`.

## Slice 3+4 Route A gate status after this PR

| Gate | Status |
|---|---|
| 1 — tail-rank-equality discharge (cross-head rank-equal case) | open
(structural blocker) |
| **2 — well-foundedness of \`_<ᵇᵘ_\`** | **CLOSED HERE** |
| 3 — Path-4 + further source-rule extensions | open (future-work,
mechanical) |

## What this does NOT do

- Does NOT prove well-foundedness of the WfCNF-narrowed \`_<ᵇᵘⁿ_\`
(#169) separately — follows by the same Subrelation transport from
\`wf-<ᵇᵘ\` via the canonical \`<ᵇᵘⁿ → <ᵇᵘ\` projection. Left for a thin
follow-on if specifically needed.
- Does NOT add a Brouwer-rank embedding stronger than \`rank-pow\` —
\`rank-pow\` is K-free + lands in \`Ord\` + already discharges the WF
transport.

## Local verification

- All four Agda lanes typecheck clean, exit 0.
- \`bash tools/check-guardrails.sh proofs/agda\` — 163 modules pass.
- \`sh scripts/kernel-guard.sh\` — PASS.

Two new names pinned in \`Ordinal/Buchholz/Smoke.agda\`:
\`wf-rank-pow-pullback\`, \`wf-<ᵇᵘ\`.

## Slice 3+4 Route A session arc (6 PRs)

| PR | Layer |
|---|---|
| #165 | rank-lex-jb (b) primitive |
| #166 | rank-lex-jb (c) trichotomy + first-eq |
| #167 | Path-3 same-left source-rule extension |
| #168 | RankMonoUnion architecture |
| #169 | WfCNF wrap of the union |
| **THIS PR** | **WF of the union (Gate 2 closure)** |

## Test plan

- [x] Module typechecks under \`--safe --without-K\` with zero
postulates.
- [x] Full suite + Smoke remain green with the new module wired in.
- [ ] CI: \`check\` + \`cold-check\` + governance lanes green.
- [ ] Auto-merge on green.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
hyperpolymath added a commit that referenced this pull request May 30, 2026
## Summary

**Stacked on #168.** Mirrors \`RankMonoUmbrellaSlice4._<ᵇ⁻ⁿ_\`'s
WfCNF-bundling pattern over \`RankMonoUnion._<ᵇᵘ_\` from #168. Provides
the canonical-form invariant downstream Buchholz consumers need
alongside the rank-relation. Zero new proof obligations; \`--safe
--without-K\`, no postulates, no funext.

## What ships

| Name | Type | Role |
|---|---|---|
| \`_<ᵇᵘⁿ_\` | record (WfCNF + WfCNF + \`_<ᵇᵘ_\`) | WfCNF-narrowed union
relation |
| \`mk<ᵇᵘⁿ\` | record constructor | Bundling combinator |
| \`<ᵇᵘⁿ-from-<ᵇ⁰\` / \`<ᵇᵘⁿ-from-<ᵇ¹\` / \`<ᵇᵘⁿ-from-<ᵇ⁺²\` |
embeddings | Constructor-level uplifts under WfCNF endpoints |
| \`rank-pow-mono-<ᵇᵘⁿ\` | rank-mono theorem | One-liner forwarding
through bundled \`<ᵇᵘ-d\` |

## Architectural payoff preserved

The "union of extensions" pattern from #168 extends through the WfCNF
wrap automatically. Future contributors adding a new source-rule
extension \`_<ᵇⁿ_\`:

1. Edit \`RankMonoUnion\` to extend \`_<ᵇᵘ_\` with the new disjunct +
\`rank-pow-mono-<ᵇᵘ\` with the new case.
2. **This module updates AUTOMATICALLY** — no edit needed.

Per-extension proof work + structural composition. No proof obligations
multiply across the WfCNF boundary either.

## Slice 3+4 Route A session arc (5 PRs)

| PR | Layer |
|---|---|
| #165 | rank-lex-jb (b) primitive |
| #166 | rank-lex-jb (c) trichotomy + first-eq |
| #167 | Path-3 prototype (same-left source-rule extension) |
| #168 | RankMonoUnion (architecture) |
| **THIS PR** | **WfCNF wrap of the union** |

## Local verification

- All four Agda lanes typecheck clean, exit 0.
- \`bash tools/check-guardrails.sh proofs/agda\` — **163 modules** pass.
- \`sh scripts/kernel-guard.sh\` — PASS.

Six new names pinned in \`Ordinal/Buchholz/Smoke.agda\`.

## Test plan

- [x] Module typechecks under \`--safe --without-K\` with zero
postulates.
- [x] Full suite + Smoke remain green with the new module wired in.
- [ ] CI: \`check\` + \`cold-check\` + governance lanes green.
- [ ] Auto-merge on green AFTER #168 merges (stacked).

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant