Reframe/retraction 2026 05 18#110
Merged
Merged
Conversation
Adversarial three-reviewer review + a codebase pressure-test found no
in-repo defense for five central claims; two were contradicted by the
repo's own Gate-2 audit. This commit corrects the PROSE downward to
what the Agda actually establishes. No proof is weakened — Agda is
unchanged except for line-comment retraction banners; full build
(All.agda then Smoke.agda) still exits 0 under --safe --without-K.
Retracted -> replaced:
- "graded comonad" -> loss-graded reindexing modality
(thin-poset action; no nested D_r D_s)
- "terminal-cone universal
property" -> funext-relative pointwise mediator
- "two independent models /
model-independence" -> carrier-parametricity, fixed grade poset
- "conservativity metatheorem
discharged by the build" -> postulate-free build = evidence, not proof
- "funext quarantined" -> no funext anywhere; pointwise mediator
IS the real funext boundary
- docs/retractions.adoc: created (canonical log roadmap-gates.adoc
referenced but never existed); entry R-2026-05-18.
- docs/echo-types/earn-back-plan.adoc: created; Pillar F gated program
to convert retractions back into theorems (F1 make-or-break).
- paper/conservativity/types-abstract/establishment-plan: reframed;
"submission-ready" status withdrawn from the abstract.
- Smoke.agda + 7 modules: top retraction banners (comments only).
- ECHO-CNO-BRIDGE.adoc: scope note (its distinct, valid "model
independence" is NOT retracted; disambiguated, not over-applied).
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
The .envrc declared `use flake` but no flake.nix existed, so direnv failed. Add a devShell pinned to nixpkgs nixos-24.11: - rustc 1.82.0 + cabal-install 3.12.1.0 (exact .tool-versions match), agda 2.7.0.1, ghc 9.6.6, just 1.38.0 - Agda libraries: standard-library (nixpkgs, reproducible) + absolute-zero (local ~/dev/repos checkout; no usable upstream pkg), wired via a generated AGDA_DIR/libraries in the shellHook - .gitignore: ignore the generated .agda/ dir Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.