Repository navigation
Polish - #46
Merged
Merged
Polish#46
Conversation
- IsVacuumState, IsGroundStateForFlow and IsGroundStateForFlow.exists_strongContinuous_unitary take their GNS Hilbert space in Type u, the universe of the net (D1). - isCompact_weakStateSet drops [Nontrivial A]; the trivial case is the empty set (D7). - The blueprint states def:geodesic for spacetimes, matching the Lean (D2). - Curved Axiom 5: a formalization note and Lean implementation notes record that the oriented identity component is the group of isometries connected to the identity, with the equality waiting on a Myers-Steenrod-type theorem (D3). - Add the staged fix plan for the 1.0 review. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
- Replace a leaked process comment in OperatorIntegral.lean. - Move the MinkowskiSpacetime material out of the docstring of standardMinkowskiTimeOrientation into MinkowskiSpacetime's own. - Add docstrings to seven substantive theorems. - Correct the generality claim in GNS/Basic.lean and the "unconditionally for beta > 0" wording in KMS.lean. - Explain every remaining set_option (all are needed) and the nolint on L0; replace one erw with rw and explain the other two. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
- Extract the shared product estimate in OperatorIntegral.lean into norm_mul_sub_mul_lt, used by integral_bddMeasurable_mul and tendstoUniformly_mul_of_bounded. - Drop the unused timelike-v hypothesis from reverse_cauchy_schwarz_of_lorentzianAt and update its callers; the blueprint-named reverse_cauchy_schwarz keeps the blueprint's statement. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
- Formalization notes on the GNS existence proof, prpstn:hall-10.3 and
prpstn:integral-norm-bound, recording where the Lean route differs.
- \lean{} tags: add isSelfAdjoint_toOperator and integral_one; drop
the bounded special case exp_generator_unique from
lmm:exp-generator-unique.
- Narrow lmm:derivative-vanishes-along-path to the derivative claim.
- Trim the proof \uses{} of prpstn:hall-8.4, thrm:hall-8.10 and
thrm:spectral-theorem-for-bounded-operators to the nodes each proof
cites.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
- spacetime.tex: Lorentz, proper and orthochronous transformations, the inhomogeneous Lorentz group, Lorentz paths and the Lorentz invariance of causal precedence and spacelike separation. - haag-kastler-axioms.tex: weak-to-strong continuity of unitary groups and the strongly continuous GNS unitaries of an invariant state; stronger Lean forms added to three existing nodes. - haag-kastler-axioms-in-curved-spacetime.tex: joint satisfiability of the curved axioms and local commutativity under inclusion; four existing nodes cite their bundled or stronger Lean forms. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
- Home page: the density-theorem entry no longer cites a lemma range; list FunctionalCalculus on the 10.3 page. - Replace hard-coded chapter and section numbers with references. - Remove a stray asterisk, a contraction, and the unneeded non-emptiness hypothesis of the Boundedness Theorem. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
- check_temporal_wording.py flags "no longer", non-positional "previously" and history-telling "now" phrases; a temporal-ok marker skips a line. Reword the two lines it flags. - blueprint.yml drops the unused issues and pull-requests permissions. - Both workflows use actions/checkout@v6 and the same pinned lean-action; free-disk-space is pinned to v1.3.2. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
- Renumber every home-page entry from the rebuilt blueprint, add the 13 Chapter 10 nodes from stage 5, and recompute counts and page ranges (675 declarations, 1,188 Lean names, 345 PDF pages). - Log the build, lint, checkdecls and receipt refresh, and add the audit of the plan's changes. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
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.