WIP Refactoring - #23
Draft
kencyke wants to merge 113 commits into
Draft
Conversation
Build the AQFT local-net layer on the isotony embedding: functoriality, locality (disjoint regions commute), the quasi-local C*-algebra (C*-inductive limit) and covariance (symmetry action). Relax `LocalNet.sites` to an arbitrary (possibly infinite) type so the quasi-local algebra is a genuine inductive limit. Generalize the C*-inductive-limit construction into `ForMathlib` (`DirectLimit` *-algebra and C*-norm, `Completion` C*-algebra), and organize `LocalNet/` by net property: Basic / Isotony / Locality / QuasiLocal / Covariance. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Promote the index bijection `combineIdx` to a genuine tensor factorisation of
operators on Hilbert spaces. Add to ForMathlib the Euclidean-space tensor
isometry (`EuclideanSpace.tensorEquiv`), the `End ⊗ End ≃ End(⊗)` algebra
equivalence (`endTensorEndAlgEquiv`), and an explicit-subspace partial trace
`LinearMap.partialTrace (e : ℋ ≃ₗ A ⊗ B)` with its ampliation `LinearMap.ampliate`
and module ("pull-out") law `Tr_B((A⊗1)·ρ) = A·Tr_B(ρ)`.
On the net, identify the local matrix algebra with operators on the region
Hilbert space (`opEquiv`), build the operator tensor decomposition `tensorEquiv`,
and prove that isotony is the ampliation (`opEquiv_includeAlgebra`) and the
marginal `restrict` is the partial trace tracing out the complementary region
(`opEquiv_restrict`), with the traced-out subspace named by `regionBipartition`.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Remove the empty/insert/univ recursive split, the left-associated triple factorisation, the complement-decomposition suite, and the singleton helper from LocalNet/Basic.lean. Only regionIdxCongr, regionIdxPairEquiv and regionIdxTripleEquiv are actually consumed by the net properties; the rest was speculative scaffolding with no call sites. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
The leftMulMatrix_rpow / rightMulMatrix_rpow lemmas and the entire star-algebra homomorphism + continuity + cfc apparatus built to prove them were unused. Removing the rpow lemmas orphaned the whole chain (leftMulStarAlgHom, rightMulConjTransposeStarAlgHom, *_cfc, rightMulMatrix_posSemidef) plus several leaf helpers (leftMul_apply, *_pow, *_conjTranspose, signMatrix_*, kronecker_npow, leftRightMatrixPerspective and its Hermiticity lemma). All removals verified dead by build. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
matrixExp and its only consumer matrixExp_trace were unused, as were matrixLog_trace, matrixLog_isHermitian, matrixFunction_neg_id, matrixFunction_sub_const and matrixSqrt_conjTranspose_mul_self_posSemidef. matrixLog itself is kept (consumed by the entropy modules). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Drop star_mul_self_eq_normSq, kernel_degenerate_right, real_eval_nonneg_of_nonneg, real_eval_le_of_le, star_mul_self_ne_zero_of_ne_zero and norm_star_mul_self_eq_sq, none of which had call sites. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Adjoint, l2Space, ContinuousFunctionalCalculus.Abs (operator absolute value), ContinuousFunctionalCalculus.PartialIsometry and SpecialFunctions.Pow.Real are imported only by the aggregate root and consumed by no module. The polar- decomposition pair (Abs + PartialIsometry) in particular was unwired scaffolding. Drop the files and their aggregate imports (~802 lines). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Introduce a lightweight scoped postfix `T†` for `ContinuousLinearMap.adjoint T` in `ForMathlib/Analysis/InnerProductSpace/AdjointNotation.lean`, the standard operator-algebra symbol for the Hilbert-space adjoint. The notation lives in the opt-in `Adjoint` scope and the module imports only Mathlib, keeping it a valid ForMathlib upstream candidate. Regenerate the `QuantumSystem` aggregate. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Spell the Hilbert-space inner product as `⟪·,·⟫_ℂ` and operator composition as `∘L` in `HilbertSpace`, `InvariantSubspace`, and `DiagonalAmplification`, matching Mathlib idiom. `InvariantSubspace` gains a file-local `†` postfix for the adjoint so its proofs read like its existing comments. No imports beyond Mathlib are added, preserving ForMathlib purity. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Rewrite the GNS construction's inner products as `⟪·,·⟫_ℂ` and the representation adjoint as `†` throughout statements and proofs, so the defining identities (`inner_ξω_eq`, `state_recovery`, `πω_star`) read as in the operator-algebra literature and match their docstrings. Two calc steps lifting the inner product across the quotient/completion coercion keep the explicit `@inner` form (no type anchor for the notation's instance metavariable) with an explanatory comment; the explicit `@norm` on the quotient is likewise retained. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Spell the adjoint as `†` and inner products as `⟪·,·⟫_ℂ` across the `CStarRep` representation layer (unitary equivalence, conjugation, irreducibility, hom, direct sums) and the WOT double-commutant development, so intertwiner and adjoint identities read as in the source texts. Comments and docstrings using `U⋆`/`(·)*` for the adjoint are unified to `†`. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Eliminate the custom spectral functional calculus `matrixFunction` (and the `matrixLog` defined on top of it), expressing all matrix functional calculus directly through Mathlib's continuous functional calculus `cfc` / `CFC.rpow`: - Löwner/Jensen convexity definitions and the Order/Effros/LiebConcavity operator-convexity proofs (rpow integral representation, compression). - von Neumann / relative entropy, Kronecker log-tensor identity, SSA. - `matrixSqrt` / `matrixInvSqrt` redefined via `CFC.rpow`. - New standalone cfc helpers: `cfc_spectral_eq`, `trace_cfc`, `trace_mul_cfc`, `cfc_isHermitian`, `mul_cfc_isHermitian`, `cfc_add_const_eq`, `cfc_inv_add_const`, `cfc_resolvent`, `cfc_compression_of_commuting`. - Delete `matrixFunction` and all `matrixFunction_*` lemmas. The `matrixLog → cfc` migration is inseparable from the `matrixFunction` removal (matrixLog was defined via matrixFunction), so the coupled entropy-module reorganization it required is bundled here as well (MutualInfoProduct, SSAProduct, StrongSubadditivityEval, partial-trace bridges, region-index equivalences). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Rename the two strong-subadditivity files into a self-describing family so the two settings of the same theorem are clear at a glance, and drop the removed lean-eval layer: - SSA.lean -> StrongSubadditivityLocalNet.lean - SSAProduct.lean -> StrongSubadditivityProduct.lean - remove StrongSubadditivityEval.lean (and its aggregate import) The LocalNet theorem gains a symmetric setting suffix (vonNeumannEntropy_SSA -> vonNeumannEntropy_SSA_localNet), matching the existing _product suffix, and each module docstring now cross-references its companion. Aggregate regenerated via scripts/mk_all.lean. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
entropyFun (= -x log x, guarded at x ≤ 0) duplicated Mathlib's Real.negMulLog, which the file already bridged. Drop entropyFun, entropyFun_nonneg, entropyFun_eq_negMulLog_of_nonneg and the entropyFun-sum form vonNeumannEntropy_eq_sum; route everything through vonNeumannEntropy_eq_negMulLog_sum (now proved directly from trace_mul_cfc) and the Mathlib lemma Real.negMulLog_nonneg. Also list the previously-undocumented fundamental results in the Main Results sections: von Neumann entropy eigenvalue-sum / nonneg / le_log_dim, and relative entropy Klein nonneg / faithfulness. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Reify the Haag-Kastler net as a first-class abstract structure `LocalNet` (Net.lean): the region assignment with isotony embeddings, functoriality and locality, on which the directed system, the quasi-local algebra, the C-star completion for faithful nets, and the covariance symmetry group are built once and for all. The former concrete carrier (sites + finite local dimensions) is renamed `SiteIndexSystem` and becomes one instance via `SiteIndexSystem.toLocalNet`; its quasi-local algebra and cocone are now thin wrappers over the abstract net. Covariance is lifted to the abstract net: `LocalNet.Symmetry` forms a `Group` under composition with a monoid-homomorphic action `quasiLocalRelabel` on the local observables. Locality and faithfulness docstrings were refined (microcausality; injective inclusions as the standard non-degeneracy condition). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…odules Mechanical rename of the generating-data structure (former `LocalNet`, now `SiteIndexSystem`) across the entropy, partial-trace, channel and notation modules that consume it, with minor accompanying docstring touch-ups. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…alences Add `UniformSpace.Completion.mapStarAlgEquiv`: a uniformly continuous `*`-algebra equivalence whose inverse is also uniformly continuous extends, by continuity on the dense image, to a `*`-algebra equivalence of the completions. Mirrors Mathlib's `mapRingHom`/`coe_mapRingHom` for ring homs. This is the supporting infrastructure for extending the AQFT covariance action to the quasi-local C*-algebra. Candidate for upstreaming. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…utomorphisms Each covariance isomorphism `β` is a `*`-isomorphism, so the action `quasiLocalRelabel` is C-linear and `*`-preserving. Package this as a `*`-algebra automorphism `quasiLocalRelabelStarEquiv : 𝔄_loc ≃⋆ₐ[C] 𝔄_loc` and a group homomorphism `quasiLocalRelabelStarHom` into its `*`-automorphism group. For a faithful net the action is isometric, so it extends along the completion to `quasiLocalCStarRelabel : 𝔄 ≃⋆ₐ[C] 𝔄` and a group homomorphism `quasiLocalCStarRelabelHom` — the genuine AQFT covariant automorphic action on the quasi-local C*-algebra. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Break the monolithic LocalNet/Net.lean into single-concern files: Net keeps only the abstract net axioms (structure, Faithful, algebraCongr); QuasiLocal gains the abstract quasi-local algebra section; Covariance holds the symmetry covariance action; and the new Symmetry module carries the abstract symmetry group (structure + Group instance), leaving Covariance for the action layer. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Merge LocalNet/Symmetry.lean into Covariance.lean and rename the abstract `Symmetry` structure and group to `Covariance`, aligning the terminology with the AQFT covariance axiom β(𝔄(Λ)) = 𝔄(σΛ). Rename the derived declarations accordingly (quasiLocalRelabel → quasiLocalCovariance, relabelAlgebra → localCovariance, relabelRegionIdx → regionIdxEquiv, toLocalNetSymmetry → toLocalNetCovariance, quasiLocalCStarRelabel → quasiLocalCStarCovarianceEquiv), drop the obsolete Symmetry import from the aggregate root, and refresh the module docs. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
… concrete example Split the covariance material across three files by abstraction level: - Covariance.lean: abstract `LocalNet.Covariance` data and group structure only (now depends on Net alone). - QuasiLocal.lean: hosts the abstract covariance action on the quasi-local algebra and its C*-completion. - LatticeCovariance.lean (new): the concrete `SiteIndexSystem.Covariance` of the generated matrix net, together with its inherited action. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Separate the abstract Haag–Kastler net layer (namespace LocalNet) from the finite-dimensional matrix model (namespace SiteIndexSystem), which were mixed across files and names. - Abstract layer stays at LocalNet/ top level: Net (bundled structure), Covariance, and QuasiLocal (inductive limit, C*-completion, covariance action only). QuasiLocal no longer transitively pulls in Channel or the matrix norm. - Concrete matrix model moves under LocalNet/MatrixModel/: Basic -> SiteIndexSystem, Isotony, Locality, TensorDecomposition, LatticeCovariance -> Covariance, and a new Net carrying toLocalNet plus the quasi-local wrappers split out of QuasiLocal. - Update the two downstream importers (PartialTrace, PartialTraceOperator) and regenerate the QuantumSystem aggregate. Pure reorganization: no proof or statement changes; lake build is green. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…it net Remove the MatrixModel/SiteIndexSystem layer and the matrix partial-trace bridge, and build the quantum-information stack directly on the abstract split net: - drop QuantumSystem/Algebra/LocalNet/MatrixModel/* and the old Analysis/Matrix partial-trace files plus StrongSubadditivityLocalNet - add abstract Split tensor decomposition (Algebra/LocalNet/TensorDecomposition) - add the representation-free Split* entropy stack: SplitTrace, SplitEntropy, SplitRelativeEntropy, SplitTransport, SplitSSA - merge TensorCommutant into ForMathlib/LinearAlgebra/Trace so ForMathlib imports only Mathlib Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…-information names Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
A PDF now converts through MinerU's CPU pipeline, but only when the call passes --allow-mineru, with --pages to convert a range instead of a whole book. Without the flag a PDF exits 5 and states what the conversion would cost; with it but without mineru on PATH it exits 5 and says how to install it. The script never installs anything itself. -b pipeline is passed unconditionally: MinerU 3.x defaults to a GPU backend and this machine has none. The install line is mineru[pipeline], not mineru[all], which pulls vllm and lmdeploy. Converted text is model inference, so the JSON summary carries verbatim: false and a caveat naming the tier consequence -- quotes from a converted cache are (b) with mineru-unchecked until compared against the page image. Everything downstream is unchanged: the converter's Markdown is flattened into source.flat.txt like every other rung, so the quote check works on it too. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
runArgs --gpus all hands the host GPU to the container; Docker Desktop bundles the NVIDIA runtime, so no host-side toolkit work is needed. The setting takes effect on the next rebuild, and a rebuild wipes the running session, so the post-rebuild verification procedure lives in .devcontainer/gpu-verification.md where it survives: nvidia-smi, the torch CUDA probe, a timed reconversion, the hybrid-engine trial with its OOM fallback, and the failure triage table. Two named volumes keep rebuilds cheap: hf-models holds MinerU's downloaded models and uv-cache holds the wheel cache (torch alone is ~2GB). The converter itself installs in onCreateCommand as a uv tool -- deliberately not a pyproject.toml dependency, since its hard pins and few hundred packages have no business in the venv the commit hooks run from. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
ingest.py grows --backend {auto,pipeline,hybrid-engine,vlm-engine} and
--effort {medium,high}. auto resolves to pipeline even on GPU: torch picks up
CUDA on its own, so pipeline gets the speedup with no configuration, while the
VLM backends stay opt-in -- 8GB of VRAM is their minimum and it is shared with
the Windows desktop, so they can OOM where pipeline cannot. --effort is
forwarded only to the VLM backends, which are the only ones that take it. The
JSON summary now names the backend used.
Measured end-to-end on a five-page PDF with the CPU pipeline: 2m52s including
the first-run model download, formulas out as LaTeX, and the quote check
behaves on the converted text -- a real sentence matches source.flat.txt, a
fabricated one does not. Same run surfaced a fidelity example now recorded in
ingestion.md: Knuth's small-caps byline came out as D<sub>on</sub>
K<sub>nu</sub>th, which is exactly why converted quotes stay tier (b).
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
mineru 3.4.5's pipeline imports six without declaring it, so every conversion died with "No module named 'six'" (measured on the first end-to-end run). uv tool install --with six is the workaround; the verification doc carries the same warning so a rebuild without it is diagnosed in one look. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The converter moves from `uv tool install` into the `mineru` dependency group (in `default-groups`), so a plain `uv sync` provides it and the version is locked; ingest.py therefore looks in the project venv before PATH, because `uv run` with PEP 723 metadata does not put that venv on PATH. torch and torchvision are pinned to the cu128 index. The default PyPI wheel is built for CUDA 13 and needs driver 580+; this host runs 573.22 (CUDA 12.8), where it failed to initialise CUDA and silently ran on CPU. cu128 stops at torch 2.11, hence the `<2.12` cap. Both changes land together because they share one lockfile update. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The `hf-models` volume is created root-owned by Docker, so MinerU died at model download with "[Errno 13] Permission denied: '/home/vscode/.cache/huggingface/hub'" (measured) — `onCreateCommand` chowned only the uv cache. It now chowns both and does nothing else; fetching the Lean cache, syncing the venv and installing the hooks move to `postCreateCommand`, which is where they belong now that the converter is a locked dependency rather than a `uv tool` install. `containerEnv` pins the model origin. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
A note produced by `/math-extract` is now read twice after it is written: `/math-review` resolves the note for the file under review, has the reviewer cite its `(D#)` / `(X#)` / degeneracy lines by id, converts note tiers into review tiers, and maintains the `Implemented as` back-link; AGENTS.md *Think before coding* points at `docs/math/README.md` before a new object is designed. note-format.md states what the adopted general form must contain so those readers have something to check against. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
A verbatim quote carries its source's own LaTeX macros, which every KaTeX or MathJax renderer rejects. Transcribing the definitions into a per-note $$ block keeps the quoted bytes intact — they are what the quote check verifies, and a shared macro table would silently render one source's quote in another's notation. Also records the mineru hybrid-engine backend flags and their VRAM failure mode in the ingestion ladder; neither backend raises the evidence tier. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
…perators, commutants Small additions upstream candidates needed by the von Neumann algebra type I structure theorem and tensor factorization work: helpers on CStarAlgebra Hilbert space, rank-one operators, and von Neumann algebra commutants. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ctorization Extends VonNeumannAlgebra.Basic with supporting lemmas, adds the spatial tensor decomposition and tensor-factor commutant theorems, and uses them to prove the type I structure theorem (every type I factor is spatially isomorphic to the bounded operators on some Hilbert space) together with abelian/minimal-projection comparison results. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
IsSplitInclusion (an interpolating type I factor), monotonicity/sandwich/self constructors, and the spatial tensor decomposition of a split inclusion and its commutant (exists_tensor_decomposition). Also adds a minimal negative witness, the diagonal algebra on EuclideanSpace ℂ (Fin 2), whose identity inclusion is not split. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
CausalOrthogonality/OrthogonalHat/CausalIndexSet formalize the abstract causal-disjointness axioms (symmetry, heredity, every region has a ⊥-partner) without assuming directedness. LocalNet and its Faithful/ Covariance classes, and the quasi-local C*-algebra construction, are restated over an arbitrary CausalIndexSet instead of a fixed geometric model. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
ProperContainment gives the 'suitably separated' region relation the split property needs (a causal collar strictly inside the larger region), with thickening and finite-lattice constructors. VonNeumannNet.SplitProperty and LocalNet.SplitProperty state the nested-form split property over a CausalIndexSet and derive the commutant form from it via locality. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Inhabits every class/structure the local-net development introduces: ProperContainment.integerChain (a separating causal collar), trivialNet/ scalarNet/unitalRep/zeroHom (faithful nets and split-property instances), so the interfaces are not vacuously satisfiable. Registers the new module in the aggregate root. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
/math-extract notes for the two objects formalized above: the causal index set of a Haag-Kastler net (CausalIndexSet) and the split inclusion of von Neumann algebras (VonNeumannAlgebra.IsSplitInclusion), drawn from HM06, GLRV99, NAA13, BGL93, BFV01, KOE03, dB74, DL84, HS17. Records the retrieval history for the five newly fetched sources in sources.md and indexes both notes in docs/math/README.md. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Six refuted claims from the /math-review pass over the causal-index-set and split-inclusion work: the ProperContainment collar re-adjudication, two citation-drift claims (Naaijkens 2012 vs NAA13, Verch 2025 §1.2), the zeroHom docstring/triviality contradiction, the isSplitInclusion_commutant docstring-contradiction claim, and the Yngvason arXiv:1401.2652 citation (verified against the fetched PDF). Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Replaces gelfand_naimark_theorem with three statements: exists_isometric (isometric, injective, closed-range representation), exists_starAlgEquiv_range (the classical *-isomorphism-onto-a-closed-subalgebra form), and exists_isometric_separable, which puts a separable C*-algebra on a separable Hilbert space. The last needs a countable witness, so PureState gains exists_norm_sq_of_ne_zero — a pure state norming a, not merely detecting it — and GNS/Separable builds the norming family indexed by a dense sequence of the algebra. lp separability over a countable index goes to ForMathlib. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
/math-extract note for the object formalized above — a faithful representation of a separable C*-algebra on a separable Hilbert space — drawn from BF26, LAN98, SHI12 and VER25. Records that the corpus never proves separability of the GNS Hilbert space (R7) and that BF26 states SepRepThm without a proof, and rejects both the all-states and the pure-state-classes direct sums as routes to it. Back-links the note to CStarRep.exists_isometric_separable and indexes it in docs/math/README.md. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
One refuted claim from the /math-review pass over the Gelfand-Naimark work: the four textbook locators in the module doc were filed as phantom citations because the extraction note records all five books as never retrieved. The refutation pass fetched chapter listings from OpenLibrary, the Library of Congress via the Wayback Machine, and Crossref, and found every cited chapter is the one the theorem actually sits in. The module doc now cites those chapters by title rather than the section numbers, which stay unconfirmed. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…s corollaries Package the WOT/SOT double-commutant halves proved in SOTClosedSubAlgebra.lean and WOTClosedSubAlgebra.lean into von Neumann's bicommutant theorem, for a possibly non-unital *-subalgebra acting non-degenerately: A = A'' iff A is WOT-closed iff A is SOT-closed. - InvariantSubspace.lean: add ActsNondegenerately, the non-unital hypothesis the equivalence needs (strictly weaker than 1 in A). - FiniteRank.lean (new): the finite-rank operators F(H), the witness that the non-unital generality is inhabited (negatively, on infinite-dimensional H). - TFAE.lean (new): DoubleCommutant.bicommutant_tfae and its unital/image corollaries, one_mem_of_isSOTClosed, the F(H) witness theorems, and VonNeumannAlgebra.ofIsWOTClosed/ofIsSOTClosed constructors. - StructureTheorem.lean: update OrthEquivFam.mem_sotClosure_adjoin for the renamed mem_sotClosure_of_mem_doubleCommutant_starSubalgebra. - QuantumSystem.lean: register the two new modules. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Sources: SHI12, LAN98, HIA20, KOS13, SOR23, VN30, CON00. Records the sources.md retrieval log for this corpus and the docs/math/README.md index row, with the implemented-as back-link to DoubleCommutant.bicommutant_tfae. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…NTS.md State the rule against reimplementing a Mathlib object locally and papering over the mismatch with a conversion lemma or Equiv/Homeomorph — migrate to the Mathlib object instead, since a bridge makes the duplication permanent and a ForMathlib/ copy can never be upstreamed once one exists. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Mechanical /lint-fix pass over the 120-column limit: re-wrap at binders, arguments, and calc steps, and re-flow doc-comment prose. No semantic change — Notation.lean's symbol table is reformatted as an HTML table since a Markdown pipe-table row cannot be wrapped without breaking its syntax. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Measured against the plugin VS Code's own Markdown preview uses
(@vscode/markdown-it-katex): no macro definition form survives from one
math span to the next inside a note — not \newcommand, not \gdef, not
\global\def. Each span is rendered with fresh options, so a note cannot
define macros for itself. The `$$\newcommand{...}$$` preamble this skill
previously prescribed does not work, and the failure is silent until a
reader opens the note and sees a wall of `Undefined control sequence`.
Add scripts/check_render.py + scripts/render_check.js: the latter renders
a note through the real pipeline and reports every ParseError with a line
number, plus "portability hazards" — spans that happen to render here but
rely on behaviour engines disagree about (a subscripted thin space, an
unbraced multi-token argument like \widetilde\mathcal U). The former is a
lighter allowlist-based fallback for when node/the pipeline isn't
available, generated by probing a real KaTeX build one command at a time
and keeping only what actually rendered.
Rewrite note-format.md's macro section and SKILL.md's step 6 accordingly:
plain KaTeX in a note's own voice, source macros confined to fenced code
or backticks, no preamble. Wired in as a fifth check alongside the
firewall/quote/locator/discipline checks.
Also record this run's source-retrieval attempts and locator
adjudications in sources.md, per the skill's append-only ledger.
New docs/math/umegaki-relative-entropy.md via /math-extract (large run, S=6, D=9, R=21, five lanes + a refutation pass). Adopts Hiai's standard f-divergence at f(t)=t log t (the totalised Araki relative-modular form) as the general definition, justified by the type-III generality-loss discriminator against the trace-based forms (Umegaki 1962, Hiai's semifinite restatement, Khatri–Wilde's finite-dimensional form). Notable findings the refutation pass forced onto the record: - Umegaki's own paper never uses the phrase "relative entropy" — it calls the object "information"; Hiai's "semifinite" attribution to it is a defensible generalisation of a claim the 1962 paper makes about itself, not a transcription of its (finite-class) standing hypothesis. - No source in the corpus proves the adopted form agrees with the trace form on a general semifinite algebra — only on B(H) and in finite dimensions — recorded as the note's principal open limitation. - Data processing fails for sub-unital (non-unital) Schwarz maps, with a worked 2x2 counterexample. - Umegaki's own monotonicity theorem is not the modern data-processing inequality: it needs two extra hypotheses the general form does not. worst-tier: c (the relative modular operator's basic properties are attested through Hiai's citations to Araki, whose papers could not be retrieved — see sources.md). Sources retrieved: Umegaki 1962 (Project Euclid PDF, MinerU-converted and independently cross-checked against the PDF's own OCR text layer), Hiai 2018, Vedral 2002, Witten 2018, Hollands–Sanders 2017 (already cached), Khatri–Wilde 2020. Araki's 1976/77 papers could not be obtained; recorded in sources.md with what was tried.
…r-span \gdef The prior fix (7f81394) established that no macro definition survives across math spans and moved quotes carrying a source's own macros into fenced code blocks. That's correct but throws away the point of writing $...$ in the first place: the quote shows as raw LaTeX instead of the notation the source intended, and a whole-quote code fence visually disrupts the surrounding prose. \gdef does carry within the span that defines it, though -- nothing has to survive anywhere for that. So the new default is a local, self-contained macro definition inside the same $...$ (or $$...$$) the quote already uses: $\gdef\lok#1{{\mathcal #1}}\lok{B}$ This renders exactly as the source intended, in every renderer tested (bare KaTeX, @vscode/markdown-it-katex), with no cross-span persistence required. Where one macro name means different things in different sources (HS17's \A = \mathfrak{A}, WIT18's \A = \mathcal{A}), each quote gets the definition belonging to its own source. This changes what "verbatim" certifies: the displayed span carries an audited \gdef prefix ahead of the unchanged quote text. That prefix is presentation, not content -- strip it before the quote check, and audit it against the source's own preamble (or mark "reconstructed" when that preamble is unrecoverable, as with KW20's private Book_KW class, or when the gap is a LaTeX primitive KaTeX doesn't implement, like \mbox). Fencing remains the fallback for macros that cannot be \gdef'd at all. check_render.py's scanner is rewritten to match: it now parses macro definitions with a proper balanced-brace scan (the previous regex silently mis-stripped nested bodies like \gdef\BH{{\cal B}({\cal H})}), judges each span for whether its OWN definitions satisfy its OWN uses, and flags only genuine problems -- a \newcommand/\renewcommand (never carries, even within its own span), a span that is bare definitions with nothing to use them (the old preamble pattern reborn one span at a time), or a command with no local \gdef and no KaTeX support at all. Verified against a deliberately broken regression file, with and without the node/katex pipeline available.
Applies the new per-span local-macro convention (1e4e1e7) to the three notes that carried a source's own macros in verbatim quotes. - causal-index-set.md, split-inclusion.md: their document-level macro preambles never worked in the first place (measured: no definition form crosses a math-span boundary in the renderer VS Code's preview uses), so every quote using them was already broken -- this is what the user reported. Removed the preambles; every affected quote's own macro(s) are now defined locally, inside the same $...$ they're used in, so the quotes render exactly as their sources wrote them instead of throwing ParseError or falling back to inert code. Byte content of every quote is unchanged; verified programmatically by stripping the injected \gdef prefixes and diffing against the pre-edit text. - umegaki-relative-entropy.md: replaces the whole-quote code-fencing from the note's initial extraction with the same per-span technique, for the same reason -- fencing hid the notation instead of rendering it, and visually broke the quotes out of the surrounding prose. Two quotes with no macros at all (HIA18's plain-KaTeX F-1.1 definition, HS17's plain-KaTeX drel1 equation) are upgraded from unrendered plain text to live $$ blocks. VED02's \mbox and KW20's \Tr/\supp are reconstructed (not copied, since KW20's Book_KW class is unrecoverable; \mbox is a LaTeX primitive KaTeX doesn't implement), labelled as such. All five notes under docs/math/ pass `check_render.py` clean, both with and without the node/katex pipeline.
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.