README.md
Large Signal Model
README.md
1 # Large Signal Model publication source
2
3 The formal companion completes reviewed Lean mappings for all 87 numbered
4 proposition cores. Its accepted evidence contains 254 proof modules, 4,454 named
5 declarations and 2,887 named theorems. The exact theorem assumptions and source
6 correspondence are recorded in the sibling `Lean/COVERAGE.json`. Explanatory
7 prose and additional unnumbered claims retain their separate scope.
8
9 The complete 174-page layout is preserved in `source/Original_Monograph.pdf`.
10 The original publication's full XeLaTeX authoring files were unavailable. This
11 package retains that layout, the corrected editable mathematical body, its
12 scientific figures, fonts, glossary, references and reproducible update script.
13 It does not claim to reconstruct the missing XeLaTeX sources.
14
15 `build_monograph.py` applies explicit reviewed text and formal-status patches.
16 `source/FOUNDATIONS.md` is the corrected editable body, derived from the retained
17 `source/Original_Foundations.md`. The two figure files referenced directly by the
18 body are in `assets/figures`; every publication figure remains in the layout
19 input. The builder preserves the mathematical text and figures and refreshes the
20 single generated formal-count prefix. It refuses to overwrite later body edits.
21
22 `source/FORMAL_STATUS.json` supplies the publication's current coverage,
23 inventory, execution summary and compact grouped formal guide. The accepted
24 Lean receipt is `../Lean/verification/current/report.json`. Its 697 accepted
25 stages comprise 694 Lean stages and three Python checks. The permitted logical
26 axioms are `propext`, `Classical.choice` and `Quot.sound`.
27
28 Publication build and visual acceptance are separate records in
29 `review/CURRENT_ACCEPTANCE.json`. The current 174-page PDF passed its rebuild,
30 content and changed-page visual checks. Previous publication metadata is retained under
31 `review/predecessor_review_v018` with its original provenance.
32
33 Rebuild with Python 3 and the pinned PyMuPDF dependency. The required P052 fonts
34 and their upstream license are bundled in `assets/fonts`:
35
36 ```bash
37 python3 -m pip install -r requirements-rebuild.txt
38 python3 build_monograph.py
39 ```
40
41 The build fails if a required passage is missing, replacement text does not
42 fit, the page count changes, bookmarks move, or an untouched page changes in
43 text or pixels. It records those checks in `build/MONOGRAPH_VALIDATION.json`.