ordinal(buchholz): Slice 3 prerequisites — NonBzero + strict-jump bridge + head-Ω lower bound by hyperpolymath · Pull Request #137 · hyperpolymath/echo-types

hyperpolymath · 2026-05-28T08:10:32Z

Summary

Lands three primitives the Slice 3 headline rank-mono-<ᵇ-+1-via-head-Ω will consume, plus an in-file design note pinning the remaining pinch.

New module Ordinal.Buchholz.RankPowSlice3:

NonBzero — left-spine non-bzero predicate (nz-bOmega / nz-bpsi / nz-bplus). Rules out the degenerate bplus bzero bzero chains that WfCNF technically allows but CNF normalisation excludes.
ω-rank-pow-succ-≤-via-<Ω — strict-jump bridge from μ <Ω ν to ω-rank-pow-succ μ ≤′ ω-rank-pow ν. Two cases: fin m <Ω fin n via ω^-mono-≤ (s≤s p); fin m <Ω ω via f-in-lim′ at branch suc m.
head-Ω-lower-bound — head-Ω LOWER bound under WfCNF + NonBzero. Dual of rank-pow-dominated-by-head-Ω (the upper). Structural recursion on the WfCNF carrier; bplus recurses on left summand and chains through ⊕-left-≤-sum.

Wired into proofs/agda/All.agda adjacent to RankPowDomination, pinned in Ordinal/Buchholz/Smoke.agda under its own using block.

What this does NOT close (documented in-file)

The Slice 3 HEADLINE itself requires a strict-jump on head-Ω x₁ <Ω head-Ω y₁ from x₁ <ᵇ y₁. The existing head-Ω-inv-bpsi gives only ≤Ω (via the <ᵇ-ψΩ≤ constructor), so the ψ-source bpsi sub-case bpsi ν α <ᵇ y₁ at ν = head-Ω y₁ does NOT close under head-Ω alone — the strict jump must come from α's rank (rank-adm / rank-lex combination, not head-Ω).

Two closure paths recorded in-file (route A = rank-lex combination, route B = refined inversion). Implementation is a follow-on slice.

Build invariant

Ordinal/Buchholz/Smoke.agda exits 0 under --safe --without-K, zero postulates.
RankPowSlice3.agda compiles standalone same flags.

Test plan

Buchholz Smoke green locally.
Full top-level All / Smoke via CI (local env has unrelated stdlib injectivity issue on EchoTotalCompletion etc.).
No postulates, no funext, no TERMINATING pragma.

PR #136 (session/doc-sweep-slice-2bplus-landed) introduced or touched 18 Echo*.agda modules without entries in echo-kernel-note.adoc, so scripts/kernel-guard.sh Check B (classification-drift lint) failed with exit 1 before Agda was even installed. Classifications (by in-repo import set): - EchoTotalCompletion: Tier 1 (only Echo + stdlib) — A ↔ Σ Echo encode/decode pair anchoring the F5 canonical-identity cohort - 17 others: Tier 2 (multi-hop) — split between the F5 canonical- identity / OFS cohort and the application/extension modules. F5 cohort: EchoOrthogonalFactorizationSystem, EchoImageFactorization, EchoNoSectionGeneric, EchoLossTaxonomy, EchoResidueTaxonomy, EchoDecorationStructure, EchoObservationalEquivalence, EchoOFSUnivF5, EchoOFSUnivF5Diag, EchoOFSUnivF5Iso, EchoCanonicalIdentitySuite. Application/extension: EchoEntropy, EchoLLEncoding, EchoProvenance, EchoSecurity, EchoProbabilisticSupport, EchoDifferential. Kernel-guard check A (funext-free certificate) continues to pass. Both checks PASS locally after this change. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…dge + head-Ω lower bound Lands three primitives the headline `rank-mono-<ᵇ-+1-via-head-Ω` (Slice 3 of the head-Ω route) will consume, and documents the remaining design pinch. New module `Ordinal.Buchholz.RankPowSlice3`: * `NonBzero` — left-spine non-bzero predicate (`nz-bOmega` / `nz-bpsi` / `nz-bplus`). Rules out the degenerate `bplus bzero bzero` chains that WfCNF technically allows but CNF normalisation excludes. Needed because `head-Ω bzero = fin 0` is a default whose `ω-rank-pow (fin 0) = ω^1 = ω` is NOT below `rank-pow bzero = oz` — the head-Ω lower bound fails for `bzero` and any spine that reduces to it. * `ω-rank-pow-succ-≤-via-<Ω : ∀ {μ ν} → μ <Ω ν → ω-rank-pow-succ μ ≤′ ω-rank-pow ν` — strict-jump bridge. Two cases: - `fin m <Ω fin n`: `ω-rank-pow-succ (fin m) = ω^(suc(suc m))` ≤′ `ω^(suc n) = ω-rank-pow (fin n)` via `ω^-mono-≤ (s≤s p)`. - `fin m <Ω ω`: pick branch `suc m` in the limit `ω-rank-pow ω = olim (λ k → ω^(suc k))` via `f-in-lim′`. - `ω <Ω _`: impossible (ω is top of OmegaIndex). Closes the gap between Slice 2-bplus's upper bound on the source's rank and the lower bound on the target's rank. * `head-Ω-lower-bound : ∀ {t} → WfCNF t → NonBzero t → ω-rank-pow (head-Ω t) ≤′ rank-pow t` — head-Ω LOWER bound. Dual of `rank-pow-dominated-by-head-Ω` (which is the corresponding upper). Structural recursion on the WfCNF carrier; `bOmega`/`bpsi` discharge `≤′-refl`, `bplus` recurses on the left summand's WfCNF with `NonBzero x` extracted from `nz-bplus nzx`, then chains through `⊕-left-≤-sum` for the bplus rank. Wired into `proofs/agda/All.agda` adjacent to `RankPowDomination`, pinned in `Ordinal/Buchholz/Smoke.agda` under its own `using` block with header comment per CLAUDE.md "Working rules". ## What this does NOT close (documented in-file) The Slice 3 HEADLINE `rank-mono-<ᵇ-+1-via-head-Ω` requires a STRICT-jump on `head-Ω x₁ <Ω head-Ω y₁` from `x₁ <ᵇ y₁`. The existing `head-Ω-inv-bpsi` only gives ≤Ω (via the `<ᵇ-ψΩ≤` constructor — bpsi can be `<ᵇ` an Ω at equal marker), so the ψ-source bpsi sub-case `bpsi ν α <ᵇ y₁` at `ν = head-Ω y₁` does NOT close under the head-Ω route alone. The strict jump there must come from α's rank — which lives in the rank-adm refinement, not the head-Ω route. Two closure paths under design (recorded in-file): (A) Combine the head-Ω route with rank-lex (`Ordinal.Buchholz. RankLex`) for the bpsi-source-at-equality sub-case. The rank-lex second component carries α-rank information that discharges the equality case via `<ᵇ-+ψ` / `<ᵇ-ψα`-style admissibility, mirroring the `<ᵇ-ψΩ≤` boundary closure. (B) Refine `head-Ω-inv-bpsi` to split on the source constructor: report `<Ω` (strict) for `<ᵇ-ψΩ` and `<ᵇ-ψ+`, `≤Ω` (non-strict) only for `<ᵇ-ψΩ≤`. Then chain the equality case through admissibility separately. Route (A) is cleaner — composes existing landed primitives rather than refining an inversion lemma. Implementation is a follow-on slice. ## Build invariant * `Ordinal/Buchholz/Smoke.agda` exits 0 under `--safe --without-K`, zero postulates. * `RankPowSlice3.agda` compiles standalone same flags. * Top-level `All.agda` / top-level `Smoke.agda` blocked locally by an unrelated stdlib injectivity issue affecting unrelated files (`EchoTotalCompletion.agda` shows the same env error); CI will validate the full chain. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

github-actions · 2026-05-28T08:11:25Z

🔍 Hypatia Security Scan

Findings: 68 issues detected

Severity	Count
🔴 Critical	16
🟠 High	33
🟡 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 secret-scanner.yml",
    "type": "missing_workflow",
    "file": "secret-scanner.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "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"
  },
  {
    "reason": "Agda postulate assumes without proof -- potential soundness hole (1 occurrences, CWE-704)",
    "type": "agda_postulate",
    "file": "/home/runner/work/echo-types/echo-types/tutorial/provenance_debugging/ProvenanceDebugging.agda",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  },
  {
    "reason": "Agda postulate assumes without proof -- potential soundness hole (1 occurrences, CWE-704)",
    "type": "agda_postulate",
    "file": "/home/runner/work/echo-types/echo-types/tutorial/epistemic_erasure/EpistemicErasure.agda",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

github-actions · 2026-05-28T08:23:59Z

🔍 Hypatia Security Scan

Findings: 69 issues detected

Severity	Count
🔴 Critical	16
🟠 High	33
🟡 Medium	20

⚠️ 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 secret-scanner.yml",
    "type": "missing_workflow",
    "file": "secret-scanner.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "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"
  },
  {
    "reason": "Agda postulate assumes without proof -- potential soundness hole (1 occurrences, CWE-704)",
    "type": "agda_postulate",
    "file": "/home/runner/work/echo-types/echo-types/tutorial/epistemic_erasure/EpistemicErasure.agda",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  },
  {
    "reason": "Agda postulate assumes without proof -- potential soundness hole (1 occurrences, CWE-704)",
    "type": "agda_postulate",
    "file": "/home/runner/work/echo-types/echo-types/tutorial/region_exit_audit/RegionExitAudit.agda",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

…ADME) (#144) ## Summary Surgical narrative refresh across the five canonical doc surfaces (CHANGELOG.md, EXPLAINME.adoc, docs/echo-types/MAP.adoc, README.md, readme.adoc) to catch up with the six PRs that landed 2026-05-28: #136 (kernel-guard fix), #137 (Slice 3 prerequisites), #138 (EchoImageFactorizationProp), #139 (ResidueTaxonomy Search + Epistemic), #140 (banner kit), #141 (Slice 3 headline). ## Changes per file - **CHANGELOG.md** (+78 lines) — new \`### Added (2026-05-28)\` + \`### Fixed (2026-05-28)\` blocks covering all six PRs with honest framing (Slice 3 headline closure described as "under a strict-head premise"; bpsi=bpsi-at-equal-markers caller-burden sub-case explicitly NOT closed). - **EXPLAINME.adoc** (+4 lines) — status-snapshot bullets for Slice 3, canonical identity layer extensions, and CI / foundational hygiene; new \`docs/echo-types/echo-kernel-note.adoc\` entry in "Where to look first". - **docs/echo-types/MAP.adoc** (+14 / -9 net) — new (epi, mono) bullet adjacent to image factorisation; ResidueForm instance count 4 → 6 with Search + Epistemic named; Buchholz proofs list gains RankPowSlice3 + RankPowSlice3Headline with strict-head-premise framing. - **README.md** (+2 / -2) — Tier 1 + Tier 2 mermaid node labels updated for ImageFactorizationProp + Search/Epistemic. - **readme.adoc** (+2 / -1) — Tier 1 + Tier 2 list mirror updated. ## Verification - \`scripts/kernel-guard.sh\` PASS (both Check A funext-free + Check B classification-drift). - No Agda code touched; docs-only refresh. ## Honesty constraints preserved - Slice 3 headline framed as closed *under a strict-head premise*, not unconditionally. - bpsi=bpsi-at-equal-markers caller-burden sub-case explicitly named as NOT closed (rank-adm / rank-lex remaining work). - PR #136 framed as "infrastructure honesty, not a proof-content advance". - 11/13 per-constructor rank-mono count unchanged. ## Test plan - [x] kernel-guard.sh PASS locally - [ ] CI green on this PR - [ ] Admin-merge once green or budget permits 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

hyperpolymath and others added 2 commits May 28, 2026 09:00

hyperpolymath enabled auto-merge May 28, 2026 08:10

Merge branch 'main' into session/slice-3-helpers-and-design-note

7c030ad

hyperpolymath merged commit ec2b274 into main May 28, 2026
13 checks passed

hyperpolymath deleted the session/slice-3-helpers-and-design-note branch May 28, 2026 08:24

hyperpolymath mentioned this pull request May 28, 2026

docs: post-PR-136 narrative refresh (CHANGELOG + EXPLAINME + MAP + README) #144

Merged

3 tasks

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

ordinal(buchholz): Slice 3 prerequisites — NonBzero + strict-jump bridge + head-Ω lower bound#137

ordinal(buchholz): Slice 3 prerequisites — NonBzero + strict-jump bridge + head-Ω lower bound#137
hyperpolymath merged 3 commits into
mainfrom
session/slice-3-helpers-and-design-note

hyperpolymath commented May 28, 2026

Uh oh!

github-actions Bot commented May 28, 2026

Uh oh!

github-actions Bot commented May 28, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

hyperpolymath commented May 28, 2026

Summary

What this does NOT close (documented in-file)

Build invariant

Test plan

Uh oh!

github-actions Bot commented May 28, 2026

🔍 Hypatia Security Scan

Uh oh!

github-actions Bot commented May 28, 2026

🔍 Hypatia Security Scan

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant