Idris htSubst structure (b-erasure solved, 10/15) + AFFIRMATION & status docs#118
Merged
Conversation
…#108 preservation) The b-erasure blocker (ADR-003) is solved: the result type b is a genuine type index, so hvSubst and htSubst now both carry it as an ERASED implicit ({0 b} / auto-bound). This keeps the Var case's hvSubst call erasure-consistent (the earlier 'not accessible' came from passing an erased b to an unrestricted one). htSubst (the QTT substitution lemma, mirrors Coq ht_subst) lands structurally, all under %default total, build green 8/8: - 10/15 cases PROVED: Var (via hvSubst), Unit, Lam, With, Fst, Snd, Inl, Inr, MkEcho, Weaken - 5 usage-splitting cases as typed holes: App, Tensor, LetPair, Case, Let (each consumes usplit3/uaddSplitBoundary2 + substReassocAdd/Mult; next) Notes for the split cases: Let's clause matches THLet's quantity with _ (the term's q' forces it; two named patterns clash otherwise). Then substLemma0 / subst2Lemma / preservation close the #108 tail. Only ?todo_preservation + the 5 htSubst split holes remain.
…f prompt - AFFIRMATION.adoc (root, timestamped 2026-06-19): dated affirmation of my-lang's verified standing, following the hyperpolymath standards/RSR convention in spirit (the standards repo was not in session scope). Affirms the mechanised axiom-free core + the proofs->compiler coupling, and the honest open boundary (Idris preservation #108 not done). - docs/STATUS.adoc: the Must/Intend/Wish programme tables (normative must = my-lang itself), aligned to the contractile vocabulary. - docs/handoff/NEXT-SESSION.md: ready-to-paste prompt for the next Claude to close Idris preservation (the 5 htSubst split holes -> substLemma0/subst2Lemma -> preservation), with the b-erasure solution and Coq blueprint line refs.
hyperpolymath
marked this pull request as ready for review
June 19, 2026 22:39
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
2 participants
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.
Summary
Advances the Idris
preservationtrack (#108) and adds programme-status docs.Proof:
htSubststructure + theb-erasure breakthroughThe
b-erasure blocker that stalledhtSubstacross prior attempts is solved. The result typebis a genuine type index, sohvSubstandhtSubstnow both carry it as an erased implicit ({0 b}/ auto-bound) — which makes theVar-case cross-call erasure-consistent (an unrestrictedbgives "not accessible"). Plus the Let-clause quantity clash fixed (_forTHLet'sq).htSubst(the QTT substitution lemma, mirrors Coqht_subst) lands structurally,%default total, build green 8/8:?htSubst_app,?htSubst_tensor,?htSubst_letpair,?htSubst_case,?htSubst_let— each consumes the already-landedusplit3/uaddSplitBoundary2/substReassocAdd/substReassocMult. ThensubstLemma0/subst2Lemma→preservationcloses?todo_preservation.Docs
AFFIRMATION.adoc(root, timestamped2026-06-19T21:35:54Z) — dated affirmation of my-lang's verified standing, following the hyperpolymath standards/RSR convention in spirit (thestandardsrepo was not in session scope; flagged in-file to refine against the canonical template).docs/STATUS.adoc— the Must / Intend / Wish programme tables (normative must = my-lang itself), aligned to the contractile vocabulary.docs/handoff/NEXT-SESSION.md— ready-to-paste prompt to close Idrispreservation.Test plan
idris2 --build solo-core.ipkgexits 0 (8/8), only?todo_preservation+ the 5htSubstsplit holes open%default totalviolationRefs #108,
proofs/STATUS.md🤖 Generated with Claude Code
Generated by Claude Code