WIP Refactoring - #23

Draft

kencyke wants to merge 113 commits into

mainfrom

refactor-20260617

Commits on Jun 17, 2026

docs: update AGENTS.md
kencyke
committed
cd53fd0
feat(LocalNet): build AQFT net properties and organize by module

kencyke
and
claude
committed
072275e

Commits on Jun 21, 2026

feat(LocalNet): formalize the operator tensor decomposition of the net

kencyke
and
claude
committed
d4ea173
refactor(LocalNet): drop unused region-index factorisation equivalences

kencyke
and
claude
committed
f29a1f2
refactor(Matrix): remove unused rpow CFC-transport chain from Effros

kencyke
and
claude
committed
0350172
refactor(Matrix): remove unused matrixExp and helper lemmas

kencyke
and
claude
committed
ae10354
refactor(CStarAlgebra): remove unused State helper lemmas

kencyke
and
claude
committed
8684e11
refactor(ForMathlib): remove modules unused by the project

kencyke
and
claude
committed
a40c349
feat(cstar): add bundled *-representation layer

kencyke
and
claude
committed
ef252c0
refactor(gns): build GNS representation on CStarRep

kencyke
and
claude
committed
a2f569d
feat: add † notation for continuous linear map adjoint

kencyke
and
claude
committed
bbe2709
refactor: use ⟪·,·⟫/∘L notation in ForMathlib inner-product files

kencyke
and
claude
committed
54856dd
refactor(gns): state GNS construction with ⟪·,·⟫ and † notation

kencyke
and
claude
committed
3f3c2de
refactor(cstar): adopt ⟪·,·⟫ and † notation in representation layer

kencyke
and
claude
committed
2aeecea

Commits on Jun 24, 2026

refactor: replace bespoke matrixFunction/matrixLog with Mathlib cfc

kencyke
and
claude
committed
98c276c
refactor: regroup strong subadditivity modules

kencyke
and
claude
committed
110cd4c
refactor: replace bespoke entropyFun with Mathlib Real.negMulLog

kencyke
and
claude
committed
e84c675

Commits on Jun 25, 2026

refactor(localnet): split abstract LocalNet from SiteIndexSystem model

kencyke
and
claude
committed
d0281a7
refactor: propagate SiteIndexSystem rename to analysis and notation modules

kencyke
and
claude
committed
c410f5f
feat(formathlib): add completion functoriality for star-algebra equivalences

kencyke
and
claude
committed
97edbe3
feat(localnet): act on the quasi-local C*-algebra by covariant star-automorphisms

kencyke
and
claude
committed
e0e29c8
refactor(localnet): split net monolith into focused modules

kencyke
and
claude
committed
748e51d

Commits on Jun 26, 2026

refactor(localnet): unify net symmetry into covariance module

kencyke
and
claude
committed
1435ab8
refactor(localnet): separate abstract covariance, its action, and the concrete example

kencyke
and
claude
committed
bcd5829
refactor(localnet): split abstract net layer from concrete matrix model

kencyke
and
claude
committed
3656105
refactor(localnet): rename QuasiLocal module to QuasiLocalAlgebra

kencyke
and
claude
committed
6c96b28

Commits on Jun 28, 2026

refactor(localnet): replace matrix model with representation-free split net

kencyke
and
claude
committed
3f0f2b8
chore: remove incomplete modules
kencyke
committed
6fde6d2
refactor: remove QuantumSystem.Analysis.Channel.PartialTrace
kencyke
committed
3e23dd6
refactor(entropy): drop redundant 'product' qualifier from SSA/mutual-information names

kencyke
and
claude
committed
9ecd967
chore: remove junk file
kencyke
committed
512e352
feat: remove skills
kencyke
committed
c12df3f
build: npx skills@latest add mattpocock/skills
kencyke
committed
9e79362
feat: add ingest-paper skill

kencyke
and
claude
committed
a8201a0
feat: add grill-formalization skill

kencyke
and
claude
committed
155895d
feat: add math-reviewer agent and math-review skill

kencyke
and
claude
committed
1660b4d
docs: fix relativeEntropy_channel_le docstring

kencyke
and
claude
committed
36d3695
docs: relax line-length guideline from 100 to 120 columns

kencyke
and
claude
committed
9ab7744
feat: export microcausality to quasi-local C*-algebra

kencyke
and
claude
committed
e726565
docs: align covariance docstrings with types and group-action boundary

kencyke
and
claude
committed
b0d94bc

Commits on Jun 29, 2026

feat: capture paper dependency DAG in ingest-paper INDEX.md

kencyke
and
claude
committed
c2b3d06
docs: require matching code to docs when docs overclaim

kencyke
and
claude
committed
29db0e7

Commits on Jul 19, 2026

feat: add type I factor structure theory and Hilbert tensor factors

kencyke
and
claude
committed
4ccce22
refactor: move image_centralizer to ForMathlib and document symmetrized commutant

kencyke
and
claude
committed
5b0eb76
refactor: derive hasSum_resolutionOfIdentity from coe_hilbertSumEquiv_apply

kencyke
and
claude
committed
9ba28c9
feat: strengthen spatial decomposition existentials to covering families of minimal projections

kencyke
and
claude
committed
4503fef
refactor: move Hilbert tensor factors to VonNeumannAlgebra.TensorFactor

kencyke
and
claude
committed
ebdb16e
feat: prove the tensor von Neumann algebras are factors

kencyke
and
claude
committed
08ed864
feat: add abelian projections and the general type I property

kencyke
and
claude
committed
4097ef7
feat: prove type I iff minimal projection for factors

kencyke
and
claude
committed
24bd242
refactor: keep ForMathlib modules importing only Mathlib

kencyke
and
claude
committed
a3b7bed
feat: add supporting API for the B(H) type I factor development

kencyke
and
claude
committed
f693644
refactor: remove unused theorems

kencyke
and
claude
committed
fa3e223
refactor: demote auxiliary theorems to lemma

kencyke
and
claude
committed
5a74a73
feat: add IsTypeIInfinite predicate for type I_∞ factors

kencyke
and
claude
committed
795b00e
chore: remove mattpocock/skills skills

kencyke
and
claude
committed
7bcd0c2

Commits on Jul 20, 2026

refactor: merge Lattice.lean into BoundedLinearOperators

kencyke
and
claude
committed
8033f2b
docs: reword grill/ingest skill descriptions

kencyke
and
claude
committed
c603918
refactor: move type I predicates and structure theorem into TypeI

kencyke
and
claude
committed
15a2df1
refactor: consolidate VonNeumannAlgebra modules

kencyke
and
claude
committed
22f1792
refactor: replace Top instance with named 𝓑(H) and a bridging star-isomorphism

kencyke
and
claude
committed
bc08cf2
refactor: make type-level 𝓑(H) an opt-in scoped notation

kencyke
and
claude
committed
fa6639a
docs: clarify LocalNet scope, Faithful split, and empty-region algebra

kencyke
and
claude
committed
97797d0
feat: add union-only smart constructor LocalNet.mk'

kencyke
and
claude
committed
b7c1098
refactor: drop algebraCongr_apply subsumed by algebraCongr_self

kencyke
and
claude
committed
53c1290
refactor: index local nets by a causal poset of regions

kencyke
and
claude
committed
20f7d4d
feat: add generated_mono for von Neumann algebras

kencyke
and
claude
committed
71e9c27
refactor: restate split tensor decomposition in inclusion form

kencyke
and
claude
committed
83bb16e
feat: add split inclusions of von Neumann algebras

kencyke
and
claude
committed
952e4d1
feat: add star and isotony lemmas for the dense local embedding

kencyke
and
claude
committed
b73ca0c
feat: add the split property of a local net

kencyke
and
claude
committed
8cdebb4

Commits on Aug 13, 2026

chore: npm audit fix
kencyke
committed
d9ab94f

Commits on Aug 14, 2026

chore: remove unriped skills
kencyke
committed
7ea5d75
chore: remove package.json
kencyke
committed
f7669f9
chore: migrate commit message linting to commitizen

kencyke
and
claude
committed
0aff811
feat: add evidence tiers, refutation pass and ledger to math-review

kencyke
and
claude
committed
519a6bd
docs: gloss the tensor-bar shorthand in TensorFactor

kencyke
and
claude
committed
ca91d56
refactor: name the proper-containment hypothesis in the split lemma

kencyke
and
claude
committed
8f1472e
feat: add lint-fix skill and move the lint rules into it

kencyke
and
claude
committed
5445e7f
docs: add plan-mode response guidance to AGENTS.md

kencyke
and
claude
committed
9fed209
feat: add math-extract skill for pre-Lean literature extraction

kencyke
and
claude
committed
d33e61b
feat: give math-extract's checks the commands they were measured with

kencyke
and
claude
committed
71dca2c
chore: remove the dead pdf-to-knowledge PostToolUse hook

kencyke
and
claude
committed
5445ce6
feat: add the MinerU rung to math-extract ingestion

kencyke
and
claude
committed
3bc8415
build: pass the host GPU to the devcontainer and persist mineru caches

kencyke
and
claude
committed
c7fa2aa
feat: wire backend and effort selection into math-extract ingestion

kencyke
and
claude
committed
31c624a
fix: inject six into the mineru tool venv

kencyke
and
claude
committed
f7fce65
build: install mineru from a dependency group and pin torch to cu128

kencyke
and
claude
committed
8f7464f
fix: chown both cache volumes and split the devcontainer create steps

kencyke
and
claude
committed
6568ed2
feat: hand extraction notes to math-review and to object design

kencyke
and
claude
committed
4d8a21b

Commits on Aug 15, 2026

feat: render source macros in a note preamble instead of editing quotes

kencyke
and
claude
committed
4ec09ec
docs: update GPU verification notes for uv sync and cu128 pin

kencyke
and
claude
committed
c52db89
docs: remove GPU verification notes

kencyke
and
claude
committed
eb7caa6
docs: add proof route and nonvacuity check to math-extract

kencyke
and
claude
committed
351f5dd
feat(ForMathlib): add supporting lemmas for Hilbert space, rank-one operators, commutants

kencyke
and
claude
committed
4d59f7f
feat: prove the type I factor structure theorem and spatial tensor factorization

kencyke
and
claude
committed
f66a2ff
feat: add split inclusion of von Neumann algebras

kencyke
and
claude
committed
74da9e1
feat: add causal index sets for local nets

kencyke
and
claude
committed
bb05693
feat: derive the split property from proper containment

kencyke
and
claude
committed
a130a0a
feat: add witnesses for the local-net interfaces

kencyke
and
claude
committed
9bc1131
docs: add extraction notes for causal index set and split inclusion

kencyke
and
claude
committed
57af85c
docs: record math-review ledger entries for LocalNet/VonNeumannAlgebra

kencyke
and
claude
committed
2e21b4b

Commits on Aug 16, 2026

feat: state the Gelfand-Naimark theorem and its separable refinement

kencyke
and
claude
committed
a2fa4f5
docs: add extraction note for the separable faithful representation

kencyke
and
claude
committed
89f28ce
docs: record the math-review ledger entry for GelfandNaimark

kencyke
and
claude
committed
9b1810d
feat: state the bicommutant theorem as a three-way TFAE and derive its corollaries

kencyke
and
claude
committed
71a5efb
docs: add extraction note for the von Neumann bicommutant theorem

kencyke
and
claude
committed
dd26be4
docs: add the 'do not bridge what should be unified' principle to AGENTS.md

kencyke
and
claude
committed
ae20f4a
chore: wrap lines over 120 columns

kencyke
and
claude
committed
2d7f460