Skip to content

docs: seed proof-debt.md per standards#203 schema (all 150 markers §(e) vendored)#82

Merged
hyperpolymath merged 1 commit into
mainfrom
claude/proof-debt-schema-202605
May 27, 2026
Merged

docs: seed proof-debt.md per standards#203 schema (all 150 markers §(e) vendored)#82
hyperpolymath merged 1 commit into
mainfrom
claude/proof-debt-schema-202605

Conversation

@hyperpolymath
Copy link
Copy Markdown
Owner

Summary

Seeds docs/proof-debt.md for hyperpolymath/maa-framework per the
trusted-base reduction policy schema landed via
hyperpolymath/standards#203 (canonical policy) +
hyperpolymath/standards#211 (scripts/check-trusted-base.sh CI gate).

Triage result

All 150 syntactic markers across 13 files live under the in-tree
absolute-zero/ subtree — a vendored copy of the sibling estate repo
hyperpolymath/absolute-zero. Canonical disposition is delegated
upstream.

Per the standards#203 guidance ("extend the schema; document the
extension at the top of the file as a repo-specific note"), this seed
introduces a new disposition:

  • §(e) VENDORED — estate-sibling: marker lives in an in-tree copy
    of another estate repository; close-out path is upstream.

§(a)/(b)/(c)/(d) are all empty because maa-framework itself
contains no proof-bearing source outside the vendored subtree.

Marker count by disposition

§ Count
(a) DISCHARGED 0
(b) BUDGETED 0
(c) NECESSARY AXIOM 0
(d) DEBT 0
(e) VENDORED — estate-sibling 150 (13 files)

Vendored-ratio

13/13 files vendored, 0/13 estate-owned-by-this-repo.

File-header inspection confirms estate-ownership (Author: Jonathan D. A. Jewell; Project: Absolute Zero) but canonical home is the
sibling repo hyperpolymath/absolute-zero. The two trees have
drifted (LambdaCNO.v differs); re-sync is a follow-up.

Owner-decision questions filed inline

  1. Should absolute-zero/ become a git submodule (so the canonical
    proof-debt.md is the single source of truth) instead of a
    vendored copy?
  2. What is the re-sync cadence until that decision lands?

The original audit prompt flagged maa-framework with the explicit
question "investigate whether vendored or original". This PR's answer:
fully vendored from a sibling estate repo, zero original
proof-bearing source in maa-framework itself
.

Notes on the audit count (134 vs 150)

The estate-wide audit reported "134 markers in 25 files" for
maa-framework. The wider regex used by check-trusted-base.sh
matches 150 hits across 13 files (a more inclusive pattern). One of
the 150 is a grep false positive (an Axiom.Extensionality.Propositional
module import in EchoBridgeCNO.agda). Net "load-bearing" count:
~149. The schema preserves the grep number for CI parity.

Test plan

  • CI green on this branch (governance, hypatia, antipattern checks).
  • bash scripts/check-trusted-base.sh . (once standards#211 has
    landed in maa-framework's governance bundle) accepts the
    enumerated paths.
  • Maintainer reviews the §(e) extension and the two owner-decision
    questions.

Refs hyperpolymath/standards#203 hyperpolymath/standards#211

🤖 Generated with Claude Code

Co-Authored-By: Claude Opus 4.7 (1M context) noreply@anthropic.com

…endored)

Add docs/proof-debt.md conforming to the trusted-base reduction policy
schema from hyperpolymath/standards#203 (canonical) + standards#211
(check-trusted-base.sh CI gate).

Triage result: all 150 syntactic markers (13 files) live under the
absolute-zero/ subtree, which is an in-tree copy of the sibling estate
repo hyperpolymath/absolute-zero. Canonical disposition is delegated
upstream.

Per standards#203 guidance ("extend the schema; document the extension
at the top of the file as a repo-specific note"), this seed introduces
disposition §(e) VENDORED — estate-sibling, for markers whose
close-out path is in another estate repo. §(a)/(b)/(c)/(d) are all
empty because maa-framework itself contains no proof-bearing source
outside the vendored subtree.

Breakdown by file group:
  - absolute-zero/proofs/coq/     : 7 files,  91 markers
  - absolute-zero/proofs/lean4/   : 4 files,  54 markers
  - absolute-zero/proofs/agda/    : 1 file,    1 marker  (grep false positive)

Vendored-ratio: 13/13 files vendored, 0/13 estate-owned-by-this-repo.

PROOF-NEEDS.md's known gap (`y_not_cno` Admitted in
proofs/coq/lambda/LambdaCNO.v) is recorded as a §(e) entry deferred
to the sibling repo, consistent with the policy's "vendored markers go
in §(e)" rule.

Two owner-decision questions filed inline:
  1. Should absolute-zero/ become a git submodule rather than a
     vendored copy?
  2. Re-sync cadence until that decision lands.

Refs hyperpolymath/standards#203 hyperpolymath/standards#211

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@hyperpolymath hyperpolymath enabled auto-merge (squash) May 27, 2026 08:17
hyperpolymath added a commit to hyperpolymath/absolute-zero that referenced this pull request May 27, 2026
…vendored copy (#65)

## Summary

Upstreams 3 Agda files that exist only in maa-framework's vendored copy
of absolute-zero, but self-identify as absolute-zero artefacts.

- `proofs/agda/EchoBridgeScaffold.agda` — compile-safe interface (`Echo`
Σ-shape, `CNOModel`), intentionally independent of `CNO.agda`.
- `proofs/agda/EchoBridgeCNO.agda` — concrete instantiation from
`CNO.Program` / `CNO.eval` into the scaffold.
- `proofs/agda/README.adoc` — describes the directory.

## Why now

Discovered during proof-debt classification triage for maa-framework
(filed at hyperpolymath/maa-framework#82, with disposition analysis in
hyperpolymath/maa-framework#84). The maa-framework re-vendor
(hyperpolymath/maa-framework#83) currently uses `rsync --filter='P ...'`
to *preserve* these files across each sync — once they're upstream, that
filter becomes redundant.

The README.adoc literally titles itself "Agda Proofs (absolute-zero)"
and the scaffold header says "Echo/CNO Agda bridge scaffold", so the
canonical home is here.

## Trusted-base impact

The 3-file set has **zero postulates and zero axioms**.
`EchoBridgeCNO.agda` imports `Axiom.Extensionality.Propositional` to
obtain the `Extensionality` *type*, which is then accepted as an
explicit *module parameter* by downstream functions — not postulated.
Documented in `docs/proof-debt.md` under a new "False positives" section
to satisfy `check-trusted-base.sh`'s path-enumeration clause.

## Test plan
- [ ] `cd proofs/agda && agda EchoBridgeScaffold.agda` typechecks.
- [ ] `cd proofs/agda && agda EchoBridgeCNO.agda` typechecks (may need
`CNO.agda` build prerequisites).
- [ ] `bash scripts/check-trusted-base.sh .` passes (path-enumeration
covers the false positive).
- [ ] CI green.

## Companion
- hyperpolymath/maa-framework#82 — proof-debt schema PR (parallel).
- hyperpolymath/maa-framework#83 — re-vendor PR (parallel; this PR
removes its need for `rsync --filter='P ...'`).
- hyperpolymath/maa-framework#84 — fork-vs-vendor disposition issue
(open, owner-decision).
- hyperpolymath/standards#203 — trusted-base reduction policy.
- hyperpolymath/standards#211 — `check-trusted-base.sh`.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

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

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@hyperpolymath hyperpolymath merged commit 6f66f90 into main May 27, 2026
18 checks passed
@hyperpolymath hyperpolymath deleted the claude/proof-debt-schema-202605 branch May 27, 2026 11:15
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