design(research-overhaul): the register + the foundations — lexicon, claim ladder, deskcheck papers, laws ledger, Lean ladder (draft) - #47
Open
ascalva wants to merge 2 commits into
Conversation
…e without inflating its claims Three mechanisms, one surfaced absence: a lexicon that teaches (alias and deepen, never replace — ids/commands/parsed strings frozen), a claim ladder that prices every label (agent ceiling: Proposition-with-checkable-proof; "Theorem" honest by absence), and the deskcheck evolved in place into an artifact-evaluation paper (same dc- lifecycle, board.py zero lines, book LaTeX factored not forked, PDFs to the exhaust lane never git). Plus the empty slot: the research Question, owner-only, surfaced not filled. Warrant: owner seed 2 in docs/brainstorms/mathematical-foundations.md (PR #42, sequenced first). Graduation licenses RR-1/2/3 on merge.
… Lean ladder — the overhaul's second note Structure-instantiation as the foundation (each component names the structure it models, states its hypotheses, imports theorems only under them; the implemented correspondences tabled as the working bridges). The laws ledger: docs/LAWS.md, seven mandatory columns, ~30 seed rows extracted from the real code (memberships first — resolved as coordinate-keyed relation with multiset projection, NOT the capsule's Boolean algebra; Boolean structure survives only in the support image, stronger readings demoted to Conjecture with a named falsifier). The Lean ladder L0-L4 adopted from issue #48: formal/ as a zero-coupling sibling, L1 statements with Plausible attacks and a sorry ratchet guarded against the axiom escape, L2 entry-gated discharge, L3/L4 parked. Float-epsilon as substance: three arithmetic tiers named and bound. Adversarially audited: 5 lenses (house rules, math-correctness vs code, regime/consumed-interfaces, feasibility x2), 6 must-fixes + ~25 should-fixes applied in revision — among them a fabricated code quotation replaced with the real text, the chi_s windowed-call counterexample recorded as a stated hypothesis, GAP-capped labels brought under the register's ceiling, anchor semantics fixed to symbol-at-HEAD with the repair model stated, and the SimpleGraph-vs-weighted Mathlib transfer priced honestly. Rides with: eight surgical edits to dn-research-register (its parked Lean row now points at the ladder; sect 1.3 names the real file) and the new track manifest docs/tracks/mathematical-foundations.md (owner adjudicates the coordinate at the merge). Warrant: owner seeds 1+3 (docs/brainstorms/mathematical-foundations.md, PR #42 + this session's directive); the Lean investigation is issue #48.
ascalva
changed the title
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.
What — an overhaul, two notes and a lane, one review
Per the owner's directive this PR now carries the full design treatment, ratified as a unit:
docs/design-notes/dn-research-register.md(draft,track: workflow) — the research register: the lexicon (docs/lexicon.md, alias-and-deepen, five-clause teaching contract), the claim ladder (agent ceiling: Proposition-with-checkable-inline-proof; "Theorem" honest by absence), the deskcheck evolved in place into an artifact-evaluation paper (carrier byte-compatible,board.pyzero lines, book LaTeX factored, PDFs via the exhaust lane), and the empty owner-only Question slot. Licenses RR-1/2/3 on merge.docs/design-notes/dn-mathematical-foundations.md(draft,track: mathematical-foundations— ⚑ manifest minted in this PR, owner adjudicates the coordinate at the merge) — the frame (structure-instantiation, the implemented bridges tabled), the laws ledger (docs/LAWS.md: seven mandatory columns, ~30 seed rows extracted from real code and audited line-by-line; memberships resolved as a coordinate-keyed relation with multiset projection — the capsule's "Boolean algebra" demoted to a named-falsifier Conjecture about the support image), the Lean ladder L0–L4 (from the Lean deep-dive: stress-test the proof-assistant park in dn-research-register — coverage, bridge, cost, and the agent-era premise #48 investigation:formal/zero-coupling sibling, Plausible attacks, sorry-ratchet with the axiom-escape guard, entry-gated L2 discharge), and float-ε as substance (three arithmetic tiers). Licenses MF-1..6 on merge.docs/tracks/mathematical-foundations.md— the new track manifest (scored-beliefs/erratum-relation precedent).Rulings PRESENTED to the reviewer (not resolved)
mathematical-foundationsis minted ⚑; rename or reject at the merge.[INFERENCE] → [ESTABLISHED]on the warrant of owner seed 3 (a chat directive quoted in the note). Merging ratifies the upgrade; strike the edit if the tag should stay humble.Sequencing
Merge #42 first (the warrant capsule); then this PR; the bp-152 store's own PR gates MF-1 whenever it lands.
Issues
Raised alongside: #43 (owner ruling), #44 (deskcheck README de-stale), #45 (dormant gate machinery, parked), #46 (ACM re-verification), #49 (χ_s windowed-law divergence — found by this PR's audit). Closes #48 — the Lean investigation's proposal is adopted wholesale by the foundations note; the issue's content is ratified into design by this merge.
Verification
Docs-only surface; all six CI verdicts green on the branch. Process: two ultracode treatments (11 agents each — 5 grounding readers, 1 drafter, adversarial audit, revision). The register note: 4 audit lenses, 4 must-fixes applied. The foundations note: 5 audit verdicts across two runs (a session-limit outage killed one run's reviser; the orchestrating session performed the revision inline), 6 must-fixes + ~25 should-fixes applied, including: a fabricated code quotation replaced with the real text (
conductance.py:159-160); the χ_s windowed-call counterexample recorded as a stated hypothesis (→ #49); χ_s demoted out of the exact tier (it is one float64 division); GAP-capped rows brought under the register's own ceiling (Conjecture until the falsifier lands); ledger anchor semantics fixed to symbol-at-HEAD with the repair model stated (the refactoring PR carries the row repair); the SimpleGraph-vs-weighted Mathlib transfer priced honestly (the one-line proofs are for binarized-support statements; the weighted reduction lemma is house work). Audits verified all ~34 seed-row anchors and falsifier pointers against HEAD + the staged store, all 8 register-edit old_strings unique, all table rows ≤190 chars; the orchestrating session re-verified the contested pins independently before landing.🤖 Generated with Claude Code
https://claude.ai/code/session_01HQcmECo4hNxNnQuRPxWo5K