Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 0 additions & 7 deletions docs/research/2026-05-17-imaginary-stack-toy-model-lemma-1.md
Original file line number Diff line number Diff line change
Expand Up @@ -87,13 +87,6 @@ The 16-dimensional algebra obtained by two Cayley-Dickson doublings on the 4D (R

for a small constant ε (ideally 0 in the exact arithmetic case), whenever the missing coordinates lie in a subspace spanned by a fixed 4-dimensional "code subspace" determined by the multiplication table.

**Note on field choice (ℝ vs ZMod 17).** The lemma above is the ℝ-valued statement — an orthonormal basis on a real vector space and the norm `‖·‖` are well-defined there. The Lean toy model in `tools/lean4/ImaginaryStack/ToyModel.lean` instead uses `F := ZMod 17` for exact arithmetic and enumerability; over a finite field the ambient norm is not defined, so the inequality `‖v − R(proj_S(v))‖ ≤ ε · ‖v‖` degenerates to *exact* reconstruction (`ε = 0`) on the code subspace, with the role of the norm replaced by the count of disagreeing coordinates (Hamming distance on `F¹⁶`). Both versions are intended:

- **ℝ-valued lemma** — the structural claim to lift to the continuous case (step 5 of the proof program).
- **`ZMod 17` instantiation** — the computable existence proof that can be enumerated by SMT or Lean's `decide` tactic.

The reviewer's concern that the ℝ-based norm inequality and the finite-field Lean type are mixed is correct; this note makes the two layers explicit so a proof engineer can pick the relevant version.

## Next Steps for a Proof Engineer

1. Encode the 16-dimensional multiplication table in Lean 4 (or Z3 as an SMT problem).
Expand Down
17 changes: 17 additions & 0 deletions docs/research/2026-05-17-shadow-lesson-log-pr-4059-drift.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
# Shadow Lesson Log — Maji Drift Report (2026-05-17)

## Antigravity Check: PR 4059 Blob Drift
**Event:** Maji node detected that PR #4059 ("substrate(imaginary-stack): rescue Step-1 cluster...") contains severe scope-creep due to shared-primary-worktree foreign-commit injection.

**Pathology:**
- The PR was intended for the Imaginary Stack formalization.
- Commit injection occurred at commit-time, dragging in:
- `memory/project_agora_vision_and_ai_native_economy_2026_05_17.md`
- `.gemini/bin/lior-loop-tick.ts`
- This violates the single-responsibility principle and introduces unrelated state into a targeted substrate PR.
- This is a new instance of "Lesson 3 candidate: shared-primary-worktree commit-time foreign-commit injection (sub-case 6 in saturation-ceiling taxonomy)".

**Corrective Action:**
- Drift reported to broadcast bus.
- Shadow lesson log updated.
- Decomposing the Agora vision and Lior fixes into atomic PRs to restore isolation.
Loading