Repository navigation
Stage B: restrained editorial and publication cleanup - #98
Conversation
- Issue templates linked docs/FAQ.md, docs/OPEN_PROBLEMS.md and docs/CONCEPTUAL_PRIMER.md, which no longer exist; they now link the documentation site. The labels triage and theory do not exist in the repository and are dropped; the bug template's version command uses uv. - The pull request template ran only tests/test_core.py and ruff on src/; it now names the commands CI runs. - Dependabot watched the pip ecosystem, whose PRs edited pyproject.toml without the lock and were all closed unmerged; the Python block now uses the uv ecosystem, only existing labels, and a seven-day cooldown for both ecosystems (the cooldown was also a Semgrep warning). - CODEOWNERS named @navi-bot, which GitHub reports as an unknown owner; the organisation bot is @project-navi-bot. - The ci.yml and codeql.yml header comments described codeql as a required check; the live ruleset requires lint, typecheck, security, semgrep and quality-gate, and the comments now say so.
Figure 3 shaded the eigenvalue indicator as 'Viable' / 'Non-viable' by the sign of lambda_1 although the canonical closure there has a = kappa gamma mu > 0, where the spectral condition is sufficient only (Theorem 3.16; Proposition 3.21 gives a positive solution with lambda_1 > 0). Figure 1's 'Subcritical (no emergence)' is exact only for a = 0 (Proposition 3.19). Both legends now say what the theorems say. Regenerated with figures/generate_figures.py (ALL_FIGURES_OK); the other five figures are byte-identical and their metadata-only PDF rebuilds were not committed.
- cliff.toml configured git-cliff, which no workflow, hook, script or release process ever ran; the changelog page no longer refers to it. - requirements.txt duplicated pyproject.toml without installing the cd package itself, so the documented pip fallback could not run the tests. - paper/Makefile, cd_stack.dot and cd_stack.svg built a stack diagram that nothing includes: the .tex has no graphics and the docs never embed it. - pyproject.toml: the sdist only-include list still named LICENSE.md, which PR #96 replaced with LICENSE; the Documentation URL now points at the documentation site rather than the repository. - .gitignore ignores .serena/ (local code-intelligence state that git add would otherwise catch). uv lock --check passes; no dependency changed.
- The abstract still named the operational condition CD(alpha, epsilon, delta); Definition 5.1 is CD(epsilon, delta) and Section 5 explains why the scale alpha is not identifiable and was dropped. - The contributions list said Proposition 3.21 'gives an explicit positive solution'; the proposition exhibits an explicit subsolution and a constant supersolution and establishes a positive solution between them, which is not given in closed form. - The discussion claimed the notebook's parameter sweeps show how the bifurcation structure depends on the closure form; the notebook sweeps the contradiction cost under the canonical closure only and Remark 3.24 establishes no bifurcation type, so the sentence now says what the notebook does and that comparing closure forms is future work. No statement, proof or number elsewhere changes. The PDF is the byte-reproducible build in the pinned image (30 pages).
CLAUDE.md described a Makefile that built only an orphan diagram, a 'v0.1.0 Alpha' status, seven workflows (there are eight), a test-count recipe that missed tests/repo/, trigger paths that were incomplete, and a ruleset that required codeql; the live ruleset requires lint, typecheck, security, semgrep and quality-gate. It also repeated the per-file test map and the testing philosophy from tests/README.md and cited Theorem 3.12 for the eigenvalue formula (Definition 3.13). The file now states the live facts, points at tests/README.md instead of duplicating it, gives the notebook command CI actually needs (in place, fresh kernel, no timing metadata), and carries the two maintainer procedures that lived in the .claude skills. The two skills are removed: one described PDEInfra 'axioms' (they are structure-field hypotheses) and the other still counted output cells and said not to commit the executed notebook, both contrary to CI and the tests. The pre-edit hook message told maintainers to rebuild the PDF with plain latexmk, which would fail the byte-identity gate; it now names paper/build_paper.sh. The review-rubric agent's stale test count and citation are corrected. .claude/worktrees/ is ignored.
…and the landing page Open problems: write the forced equation and the parabolic starting point with the paper's sign convention (Remark 3.17; forward heat equation), name the saturating model V1', describe Proposition 3.21 as an enclosure between barriers rather than a closed-form solution, and drop "now". Roadmap: describe Proposition 4.9 as a domain exclusion (Remark 4.10), not a cost statement; label the clinical mappings as a Heuristic; fold the usable detail of experiments/README.md (Henon setup, toy transformer task, behavioural measures) into items 2, 6 and 7 ahead of its removal. Landing page: the paper's theorem names (positive existence), the notebook's branch plots without a bifurcation claim (Remark 3.24), the cd_formalization directory with its unconditional and conditional files, and the correct count of open problems.
Rename the ci.yml badge to CI, replace the bold triad and its slogan with one plain sentence, drop the hand-written table of contents (GitHub renders its own), reduce Quick Start to the commands plus a link to the quickstart page, and point the experiments bullet at the roadmap items that now hold that content. The entry ramps and the 30-second concept list now live only on the docs landing page; the README keeps a pointer and the viability-threshold statement (Theorem 3.16, Propositions 3.19 and 3.21), which is the key mathematical qualification. The Development Process section becomes a short Provenance section with the same facts and a corrected description of the Lean assumption boundary (PDEInfra fields are hypotheses, not axioms; SolutionOperator also carries assumptions; the finite-graph theorem is unconditional). Bold slogans become plain sentences and the covenant bullet list is trimmed to the voluntary-invitation sentence. The t-shirt line and the Commercial Services section are unchanged.
CONTRIBUTING.md and docs/how-to/contributing.md were near-identical copies. The docs page is now the canonical full text: it names the saturating model V1', allows "Observation (numerical)" alongside Theorem / Conjecture / Heuristic for facts established by computation, and closes with a plain sentence instead of a bold refrain. The root CONTRIBUTING.md becomes a short file that points to the canonical page and states the four must-knows (uv only, run the tests, conventional commits and branch names, label mathematical claims). It stays because the pull request template links to it.
paper: Section 6 is "Discussion and limitations", Appendix B (transfer of the cited Euclidean results to the manifold) gets a row, the theorem list is the canonical summary, the duplicate BibTeX block points to CITATION.cff, and the graphviz build line goes with the diagram. notebooks: the notebook checks discrete claims, not the continuum theorems; the inline definitions are named as they exist (check, converse_barrier, solve_bvp_V1prime, history, independent_3d_matrix) and the 3D operators come from the library. src: the structure tree lists graph.py and _validation.py, the API reference covers all 33 names in __all__ with correct return shapes ((A, h), (A, hx, hy), the four solution_type labels), the exact-solution checks cite the test files that hold them, and the requirements.txt sentence and "(3D coming)" are gone. tests: the 2D eigenvalue test compares against the analytic formula, the validator checks marker placement rather than claim order (also in tests/repo/README.md), the count command is scoped to test_*.py so the README example is not counted, the failing-test rule says "usually", the example cites Definition 3.13, and the required checks are the live list (codeql runs but is not required). tests/repo: "guard" is "gate". figures: section references point at the paper's actual sections, the threshold is exact only for a = 0 (Proposition 3.19), the indicator is a sufficient condition when a > 0, and the citation points to CITATION.cff. experiments/README.md is removed; its usable content moved into the roadmap in the previous commit, and the quickstart tree no longer lists the directory.
SECURITY.md: supported versions are 1.1.x and current main; the core library does no file I/O (only the figure script and the notebook write files); the covenant link uses the canonical docs URL. NOTICE.md: copyright year left as authored (2026; zensical.toml says 2024-2026, a discrepancy for the owner to settle), the covenant URL instead of a path that no longer exists, and a content list that includes the finite-graph model, the paper appendices, the Lean formalization and the Python library. CODE_OF_CONDUCT.md: only the broken OPEN_PROBLEMS.md link is replaced by the canonical Open Problems page. CITATION.cff: the promotional triad sentence in the abstract becomes a plain description with the same facts; version, date, title, authors and license are unchanged. Changelog page: link to GitHub Releases and short entries for v1.0.0, v1.1.0, the Stage A revision (PR #97) and this Stage B pull request; the git-cliff sentence is gone with the tool. Quickstart: the test description points at tests/README.md for the count and its command instead of repeating numbers, the notebook summary is one sentence, and the tree no longer lists experiments/.
…ph model Deduplicate code that was byte-identical or algebraically identical across modules, without changing any numerical result: - _monotone_label existed twice (solvers.py, graph.py); it is now one private helper in analysis.py (not exported), imported by both modules. - _plateau_level computed max(1, (q_+ / c_min)^(1/(p-1))), which is exactly max(1, linfty_bound(q, c, p)); it now calls linfty_bound. The float result was checked to be identical on scalar and array inputs, including q <= 0. - The eigen-solve block repeated in principal_eigenpair_1d/2d/3d (assemble A - diag(q), take the smallest eigenpair, orient and normalize the vector) is one helper, _principal_interior; the callers only place the interior vector on their own grid. - The 1D and 2D solver tails (boundary_err, maxPhi, min_interior, branch, L-infinity bound) are one _finalize helper; the inline 2D initial-guess block is _initial_2d, mirroring _initial_1d, so a string initial_guess in 2D now raises "initial_guess must be None or an array of shape ..." instead of NumPy's cast error (test written first in test_solver_diagnostics.py). The warning stacklevel in _attach_bound moves from 3 to 4 so the L-infinity warning still points at the solver's caller. - graph.py: the repeated "copy w and zero the diagonal" is _off_diagonal. Kept separate on purpose: the two _residual_state closures and the two solver loops (the graph solver accepts on the residual alone; the finite-difference solvers also require the last update below tol), and the graph spectral assembly versus eigenvalues.py. The continuum finite-difference model, the Lean finite-graph model and the 3D eigenvalue illustration remain distinct and are not relabelled. Equivalence: all 7 figure PNGs are md5-identical to the committed ones; the executed notebook's outputs are unchanged apart from the interpreter path line and one eigsh (ARPACK random start vector) noise digit that also varies between two runs of the same code.
Behaviour change (stricter rejection at the system boundary): every scalar parameter below now goes through the shared _validation helpers, so strings, bools (Python and NumPy) and NaN raise ValueError instead of being coerced by float() / comparison or passing silently. - graph.py: solve_graph atol/rtol used float() and accepted "1e-12" and numpy bools; they now use check_nonnegative_scalar. The SemioticGraph carrying-capacity check uses require_positive_coefficient. - analysis.py: residual_2d spacings hx/hy use check_positive_scalar (a bool True previously passed as 1.0); linfty_bound validates beta_b and c with check_finite_field (a finite scalar, never a bool or string, or a finite array) and require_positive_coefficient. - fields.py: kappa/gamma use the new check_unit_interval_scalar, lam uses check_nonnegative_scalar (lam = 0 stays admissible, and the docstring now says λ ≥ 0 to match the code that always allowed it), mu/x/X/Y use check_finite_array, sigma uses check_positive_scalar and the centres and amplitude use check_finite_scalar. NaN previously passed through lam, sigma, amplitude and the arrays. - _validation.py gains two small helpers the existing ones could not express: check_unit_interval_scalar (a scalar in [0, 1]; the array form already lived in graph.py) and check_finite_field (scalar-or-array, shape-free, rejecting scalar bools and strings like coefficient_1d does). - Signature drift fixed: solve_2d_picard's beta_b and residual_2d's coefficient parameters are annotated float | np.ndarray, which is what the code accepted and the tests exercise. Tests were written first (test_fields.py, test_graph.py, test_analysis_statistics.py, test_solver_diagnostics.py): 25 of the new cases failed on the previous code for the reasons above. Equivalence: all 7 figure PNGs are md5-identical; the executed notebook's outputs are unchanged apart from the interpreter path line and the eigsh noise digit already documented in the previous commit.
Behaviour change. presence_statistics reported the support fraction of any field whose maximum exceeded 1e-10, while classify_branch calls a field with max |Phi| <= 1e-6 (_ZERO_BRANCH_TOL) the zero branch. A collapsed run with max ~ 5e-10 was therefore labelled "zero" and at the same time reported a support fraction of 1.00, because every interior node exceeded 1% of a numerically-zero maximum. The two cutoffs now agree: the support fraction is 0.0 when max(Phi) <= _ZERO_BRANCH_TOL and the computed value otherwise. The docstring states the cutoff and its origin. Tests were written first in test_analysis_statistics.py: a field with max 5e-7 gives support_fraction == 0.0 (failed before), a field with max 2e-6 keeps the computed value, and the zero-field test is unchanged. Equivalence: all 7 figure PNGs are md5-identical. In the executed notebook the only substantive output change is cell 27's collapsed case, whose "support=1.00" becomes "support=0.00" (the corrected reading); the interpreter path line and the eigsh noise digit differ as documented in the previous commits.
Delete fields.constant_field, fields.linear_gradient_1d, fields.step_function_1d and operators.grid_2d. A grep over src/, tests/, figures/, notebooks/, docs/, paper/, README.md and CLAUDE.md finds no caller of any of them (the only textual hits are the test names test_constant_field_matches_* in tests/test_eigenvalues.py, which call the eigenvalue solvers, not the helper), and none is listed in src/cd/__init__.py's __all__. grid_1d stays: grid_3d uses it. Unused constructors are surface area that nothing validates; the notebook and figures build their fields from the exported constructors only.
Strengthening only; no assertion is weakened or changed in meaning. - test_core.py accepted a run on inf_err < 1e-8 alone, which the package's own documentation says is never sufficient. Both Picard convergence tests now require check_convergence(info)[0] (residual criterion, strict update criterion against the recorded tol, boundary data, and the type and finiteness of every diagnostic); the iteration bound is kept. - Two exact duplicates are removed after reading both copies: tests/repo/test_validate_notebook.py::test_committed_notebook_passes_with_ stored_outputs (the same validate() call as test_validate_notebook_required ::test_committed_notebook_contains_every_required_claim, which also asserts the required-claim count) and test_review_regressions.py:: test_convergence_checker_accepts_a_real_run (the same solve and assertion as test_solver_diagnostics.py::test_ordinary_converged_run_records_tol_and_ satisfies_strict_update_criterion, which asserts more). - tests/conftest.py holds the helpers that were copied between files: factory fixtures for the three-vertex Lean graphs (triangle_with_b, graph_with_self_weight), the closed-form discrete 1D eigenvalue (discrete_lambda1_1d, which test_barriers.py had inlined twice), and the session-scoped converged_1d_report built from a real converged run. tests/repo/conftest.py holds ROOT (repo_root), a fresh script loader (load_script) replacing the three _load() copies, and the notebook writer (write_notebook). The tests take the fixtures instead; their assertions are untouched. - tests/README.md and tests/repo/README.md record the new counts and the fixtures: 207 test functions in 17 files (183 package, 23 repository). Checked: uv build --sdist lists tests/conftest.py and no tests/repo/ entry (the sdist exclude still applies), and the suite collects 293 tests.
Docstrings and comments only; no assertion changes.
- test_review_regressions.py: the module docstring named a squash-merged
commit and a review stage instead of the properties the tests check. It
now lists those properties (self-weight-free spectral assembly verified
against the direct operator and the Rayleigh quotient, an exact edge
condition, indeterminate status near zero, accepted solved starts,
rejected negative initial data, sign-checked branch labels, a checker that
re-validates its numbers).
- test_barriers.py: "the repaired paper argument" becomes "the paper's
barrier argument for Theorem 3.16".
- test_solver_diagnostics.py: two tests narrated history ("kept for
compatibility", "reports produced before tol was recorded"). They now
state the claim: solution_type labels a converged run by amplitude alone,
and a report without the recorded tol is unvalidated, never accepted. The
first of these carried the narration in its name, so the test is renamed
(test_converged_run_is_labelled_by_amplitude); its assertions are the same.
- test_independent_checks.py: the docstring of the zero-start collocation
test said the previous test finds the positive branch; the previous test
shows a small start collapsing to zero, and the positive branch is found by
test_fd_solution_agrees_with_independent_collocation. The docstring now
says so.
Docstrings only; no code changes. CLAUDE.md and CONTRIBUTING.md require every
mathematical claim in a docstring to carry its status. Each claim below is
now labelled Theorem / Proposition / Lemma with its paper number (verified
against the paper text: Lemma 3.10, Theorem 3.12, Definition 3.13,
Theorem 3.16, Propositions 3.19 and 3.21, Definition 3.25, Theorem 3.26,
Corollary 3.27, Remark 3.28, Example 3.29, Proposition 3.30, Remark 3.31,
Proposition 3.32), Theorem for closed-form facts about the discrete
operators, Heuristic for modelling choices, or Observation (numerical).
- operators.py: the module docstring said 1D and 2D only (3D exists); the
closed-form eigenvalue of the tridiagonal matrix is labelled.
- eigenvalues.py: the exact threshold for a = 0 cites Proposition 3.19, the
converse counterexamples cite Propositions 3.21 (continuum) and 3.32
(graph), the continuum eigenvalue cites Definition 3.13, the Kronecker-sum
formulas in 2D and 3D and the monotonicity of lambda_1 in the potential
are labelled Theorem, and the 3D routine is named as the third, distinct
model.
- graph.py: the module status list and the docstrings of
principal_eigenpair, spectral_report, edge_condition_holds, jacobi_map,
proof_constants, linfty_bound_graph and triangle cite the paper numbers
and the Lean declarations they implement.
- fields.py: the interpretive notes of the canonical closure and the
creative drive are labelled Heuristic (modelling choices, not theorems).
- analysis.py: history narration is removed ("Compatibility: reports
produced before ...", "historical amplitude labels", "(corrected form)");
linfty_bound cites Lemma 3.10 and separates the discrete a = 0 theorem
from the a > 0 heuristic.
- __init__.py and tests/test_continuum_counterexample.py said "Proposition"
without a number; they now cite 3.19 and 3.21 (and 3.32 for the graph).
pyproject.toml and cd.__version__ move from 0.1.0 to 1.1.0, and uv.lock is regenerated: the only change in the lock is the root package entry's version line (confirmed with git diff uv.lock; uv lock --check and uv sync --locked pass). No test or docstring under src/ or tests/ asserts the old version.
…-execute on Python 3.12 - The validator's REQUIRED_CHECKS list grows from 26 to 36 names, now in notebook order: it adds the convergence and residual checks that the required claims depend on (a claim about converged solves is vacuous without them), the Lean crosswalk facts of the triangle (L u = 2 and |grad u| = 2, energy(0,1,1) = -2 and lambda_1 = -1, the proof constants), and two 3D statements the interpretation cell made without asserting them: the weak bump (lambda = 0.3) gives a negative and the strong bump (lambda = 1.5) a positive discrete indicator, and near the threshold the discrete indicator is negative while the continuum value is positive. The test now pins the list's length and uniqueness and checks that the required names occur in the committed notebook in list order. - Notebook edits through nbformat: the stale description of the inline code (it named helpers that do not exist and said 3D was not in the library), the absolute local path printed by the first cell, the 'repaired proof' narration, section headings as level 2 under the title, the Jacobi history plotted for as many iterations as the solver actually needed (978/890, previously a fixed 400), and the two new checks. Per-cell nbconvert timestamps are stripped and cell ids are unchanged. - Re-executed in place from a fresh Python 3.12 kernel (the version CI uses) with record_timing=False so future runs do not churn metadata; 48 checks pass, NOTEBOOK VALID, nbqa clean, 855 KB. The collapsed 2D case now prints support=0.00 for the zero branch, following the support-fraction cutoff fix in the library.
…s on a clean tree
…nder the figures The stack diagram (cd_stack.dot, cd_stack.svg) came back after the cleanup removed it as unreferenced. Its content is audited against the current paper: every box now cites the statement it summarises (Definitions 2.3, 3.1, 3.3, 3.34, 3.36, 3.38, 3.40, 3.42; Theorems 3.12, 3.16, 3.26; Propositions 3.19, 3.21; Remarks 3.37, 3.39, 3.41, 3.43, 3.44). Corrections to what the old diagram claimed: the model is the Dirichlet problem only (no Robin condition); the creative drive a = kappa gamma mu is static in the model; the spectral condition is exact only for a = 0 and sufficient with drive; the debt variable carries its a priori bound; the feedback loop is a tendency that is not analysed; the old 'predictions' box (hysteresis, debt predicting fragility, burnout prediction) is replaced by the architectural interpretation the paper actually states, marked heuristic; the capacity-erosion extension is marked deferred and not analysed. paper/stack_figures.py renders the single source as the brand-themed SVG for the documentation site (dark background, DM Sans and Fraunces, teal accent, as in the takens-formalization proof-architecture diagram) and, with a print palette and compact labels (the plabel attributes), as the two paper figures: Layer 1 for Figure 1 and Layers 2 to 4 with the extension and the two Layer 1 context nodes for Figure 2. Graphviz output is byte-reproducible under the fixed SOURCE_DATE_EPOCH the paper build uses, and the SVG carries the SHA-256 of its source so a stale render is detectable without graphviz. make -C paper runs the renderer.
… the PDF Figure 1 (the mathematical core) opens Section 3 and Figure 2 (the temporal closure and its feedback into the operator) opens Section 3.7; both float, their captions cite the statements by reference, and the text points to them. graphicx is loaded and the build script copies the two figure PDFs into the build directory, so the figures are inputs to the byte-identity gate. Rebuilt in the pinned image: two builds byte-identical, 32 pages, no unresolved references; statement numbers are unchanged.
A new explanation page shows the brand-themed diagram (click to open at full size), reads it layer by layer with the paper's statement numbers, and ends with a status table: proved, defined, heuristic, deferred. It is in the navigation after the conceptual primer, in the landing page's table, and linked from the README.
…e rebuilt paper The diagram names paper statements by number, which drift when a numbered statement is inserted. scripts/check_stack_citations.py reads every Kind n.m token in the source (abbreviations Def., Thm, Prop., Rem. included) and fails when one does not occur in the pdftotext output of the rebuilt PDF; the paper workflow runs it after the byte-identity gate. tests/repo/test_stack_diagram.py pins the rendered outputs to the source hash, checks the source structure the renderer relies on, and covers the checker with negative fixtures. The pre-edit hook blocks direct edits to the rendered files, and CLAUDE.md documents the regeneration rule.
…d anchor its citation check An audit of the diagram against the paper found edges and statements the paper does not support, and a citation check that could not fail: - Figure 2 dropped the operator-to-eigenvalue edge, so the drawn feedback loop stopped at the operator; the edge is now drawn in both figures. - The finite-graph theorem sat in the continuum results box, fed by the continuum model and its eigenvalue. It is a separate model (Remark 3.33): Theorem 3.26 now has its own node with all three hypotheses (interior graph connected, graph eigenvalue negative, edge condition a(x), a(y) <= sqrt(w(x,y)) for all distinct interior x, y with w(x,y) > 0) and a dashed 'analogue' link only. - The dynamical closure depends on the fields at time t (Definition 3.42); that edge is added. The architectural interpretation (Remark 3.43) interprets the closure, not the loop; the edge is corrected and no longer called heuristic. - The V1' model states 0 <= a <= 1, c >= c0 > 0, p > 1; Proposition 3.21 is a counterexample to necessity, not a statement that the condition is 'sufficient only'; debt rises only while D < (eta/rho)[psi - psi_s]^+. - Captions: lambda_1 comes from the operator (Definition 3.13), not from V1'; psi's derivatives enter R_base and psi itself enters the debt; the closure supplies b(., t), so the operator and lambda_1(t) are re-evaluated. - Paper: the proxy-and-calibration paragraph moves inside Remark 3.37, which the diagram cites for it; Remark 3.41 states the debt condition of Remark 3.39; Remark 3.44 keeps the eroded fields in [0,1] by projection. Statement numbers are unchanged. hyperref now loads after float, which removes the duplicate figure and table anchors. - Print legibility: compact print labels, tighter layout and no graphviz margin; node text prints at 8.5 pt (Figure 1) and 7.4 pt (Figure 2). The citation check matched any occurrence of a number, so the numbers printed inside the figures always satisfied it. It now reads one '// cites: <Kind> <n.m> = <title>)' line per cited statement or section, parses plural and section citations in the diagram and on the CD Stack page, and requires each statement header in the rebuilt PDF to carry exactly that title. Negative tests cover a renumbered header, a truncated and an extended title, an unmapped citation, and figure text that must not count. Rebuilt in the pinned image: byte-identical, 32 pages, no unresolved references.
The page reads the diagram layer by layer with the hypotheses of each result, uses the full content width, and drops the sentences about how the diagram is generated and kept consistent.
… docs pages An audit of every README and documentation page (the author's essays and the code of conduct excluded) removed process narration, self- justification, filler transitions, hype and restated disclaimers, and fixed the accuracy problems it found: the figure notes no longer imply that fig1-fig7 are the paper's figures, Open Problem 10 records that Section 3.7 defines a temporal closure that is not analysed, the Henon parameters no longer reuse the names a and b, the roadmap's expected outcome is labelled a conjecture, and the changelog lists the CD Stack page and the paper's stack figures.
The README states the model, a table of what is proved and how, the assumption boundary of the Lean development, the numerics, the build commands and the project layout. The development section follows the fd-formalization README: what the author did, the other contributors, and what AI tools did, without a defence of the process. Andrew Edmark (finite-graph formulation) and Yongxi Lin (bornological T_compact) are credited as in the formalization's README and listed in CONTRIBUTORS.md. The classical elliptic results are described as cited and transferred to the manifold (Appendix B), not proved in the paper.
AGENTS.md holds the repository guidance for any coding agent or contributor; CLAUDE.md is the one-line import @AGENTS.md. The citation- check description follows the anchored-title check.
Dependabot moved actions/checkout to 3d3c42e5 (v7.0.1) in figures.yml, notebooks.yml and paper.yml but left the '# v6' comments, so those pins named the wrong release.
The paper build copied the committed figure PDFs, and the freshness tests only checked a source-hash comment in the SVG, that the two SVG copies agree, and PDF magic bytes. A stale render or a renderer-only change passed all three. paper/build_figures.sh now runs stack_figures.py in the image of paper/figures.Dockerfile (Debian forky by digest, packages from the 2026-09-18 snapshot, DM Sans and Fraunces from a fixed google/fonts commit by SHA-256), with the checkout read-only and no network. `check` renders all four outputs into an empty directory and requires the committed copies to be byte-identical; `update` (make -C paper) installs them. The paper workflow runs the check and builds the paper from the rendered figures, so the byte-identity gate on the PDF now covers the source, the renderer and the environment. A change to docs/assets/cd-stack.svg alone also triggers the workflow. The committed outputs are re-rendered in the image and the paper rebuilt: text is unchanged, pages 5 and 18 differ. Layout is the same up to one edge route in Figure 2. The SVG hash comment stays as a quick check without a renderer.
Stage B had presence_statistics reuse the zero-branch tolerance 1e-6 of classify_branch as the floor below which the support fraction is 0. The two numbers answer different questions: a branch label for a solver run, and the share of interior nodes above 1% of the maximum. For Phi = [0, 5e-7, 0] the support fraction became 0.0 while the interior mean stayed 5e-7. The floor is 1e-10 again, as before Stage B. A regression pins the 5e-7 case at 1.0 and fails with the 1e-6 floor; one more test pins the floor itself.
AGENTS.md, tests/README.md, CONTRIBUTING.md and the math-claim-validator agent said the tests are mathematical proofs, that they do not test implementation behaviour, and that a failing test after a src/cd/ change means the code is wrong. The suite also tests validation, reports, diagnostics, artefact freshness and packaging; finite computations do not prove theorems; and earlier repairs corrected oracles as well as code. tests/README.md now says the tests check implementation contracts and numerical consequences of the paper's statements, with the proofs in the paper and the Lean development, and holds the rule for a failing test: find out which side is wrong, never weaken an assertion to get a pass, correct an oracle only with a stated reason and equivalent or stronger coverage, add a regression for a reproduced defect. The other three files point to it.
The field helpers said strings, bools and NaN are rejected and described mu as a field in [0, 1]. That holds for the scalars (kappa, gamma, lam). Array inputs go through np.asarray(value, dtype=float): numeric strings and bools are coerced, and mu is checked for finiteness only. The _validation module docstring said coefficients outside their domain never reach a solver; the drive a is not range-checked. linfty_bound and its test class had the same scalar-only claim. The docstrings now state the scalar and array policies separately. No behaviour changes. A new test pins that mu outside [0, 1] passes through unchanged, so clipping cannot be introduced silently. Also fixes "either" in the failing-test rule.
Proposed for the author's approval; the rest of the essay is unchanged. - Zero care: the care-weighted geometry admits only paths where care is positive (Definitions 4.7-4.8, Proposition 4.9); Remark 4.10 shows this is not a proof that every crossing costs infinitely much. The sentence said the cost is infinite. - Support versus strain: kappa*gamma > lambda*mu is a local statement. Viability is the global spectral condition; b = 3/4 everywhere on (0, pi) still has lambda_1 = +1/4 (Proposition 3.21). The sentence made the local inequality the viability condition. - Threshold: crossing it guarantees a positive solution (Theorem 3.16) and is necessary only without drive (Proposition 3.19); with drive a positive solution exists below it (Proposition 3.21). The sentence said "only". - Predictions: the paper states the falsifiability criteria as empirical proposals, not consequences of the stationary PDE (Section 5.2). The sentence said the framework generates predictions.
…EADME Proposed for the author's confirmation. The development section attributed the current proof form (truncated Schaefer framework, ordered barriers) to April 2025 - March 2026, and described the AI assistance as numerics, tests, docs and Lean. The March 2026 manuscript used Schaefer's theorem with sub- and supersolutions; the truncated form, the ordered barriers, the continuum counterexample and the finite-graph section entered in the 2026 revision, after a mathematical review. The section now credits the original framework with its dates, states what the revision changed and that it was done with contributor input and AI assistance, keeps Nelson Spence responsible for the final claims, keeps the named contributors' credits, and adds the revision work to the AI paragraph.
…loor Executed in place from a fresh Python 3.12 kernel (record_timing off); NOTEBOOK VALID with 48 checks, nbqa ruff clean. The collapsed 2D case (branch zero, max 4.6e-10) prints support=1.00 again, as before Stage B; with the 1e-6 floor it printed 0.00. Other differences are rounding-level: the 1D eigenvalue error 1.34e-10 -> 1.27e-10, one plot's PNG bytes, and how two stdout chunks are grouped.
1fa270d to
858fad2
Compare
|
/agentic_review |
Code Review by Qodo
1.
|
- Bug template: drop the `pip list` alternative; the repository is uv only. - test_closed_form_on_scalars_and_fields: docstring cites Lemma 3.10 and the scalar, field and B <= 0 cases. - eigenvalues module docstring: each clause of the threshold statement leads with its statement (Theorem 3.16, Proposition 3.19, Propositions 3.21 and 3.32). - README: the Lean counterpart of Theorem 3.16 (exists_pos_isWeakCoherentConfiguration) concludes a nonnegative solution positive at one interior point, with no enclosure; the status cell now says so instead of crediting Lean with the full statement.
1.1.0 is the v1.1.0 tag of 2026-03-06. The code since then differs (Stage A, Stage B, four helpers removed, stricter scalar validation), so reporting 1.1.0 would give two codebases one version. 1.2.0.dev0 marks it unreleased. pyproject.toml, cd.__version__, uv.lock (project entry only), AGENTS.md and the changelog follow; CITATION.cff still cites the 1.1.0 release. The notebook prints the version, so it is re-executed (Python 3.12, NOTEBOOK VALID with 48 checks); the other output changes are rounding-level.
As the author chose: crossing the viability threshold guarantees a positive presence field under the model's assumptions (Theorem 3.16); it is necessary when creative drive vanishes (Proposition 3.19); positive fields can exist below it when drive is active (Proposition 3.21). The sentence in the author's voice between them is unchanged.
The 2D printout put support=1.00 next to branch=zero for the collapsed case (max 4.6e-10). Support is the share of interior nodes above 1% of the maximum, so it says nothing about whether the field is zero. The line now reads "relative support=1.00 (branch=zero at tolerance 1e-6)"; the branch label moved into that parenthesis. Re-executed on Python 3.12, NOTEBOOK VALID with 48 checks.
…ision date As the author chose. The title said "Lean 4-Verified Existence Conditions"; Lean proves the finite-graph theorem outright but the continuum existence theorems only conditionally on PDEInfra (Appendix A). The date keeps the original and adds the revision: "January 2026; revised October 2026". CITATION.cff (both titles), the README citation, paper/README.md, the FAQ citation and BibTeX, and the changelog follow. Rebuilt in the pinned image from the checked figures: byte-identical to the committed PDF, 32 pages, no unresolved references, 27/27 cited headers; only page 1 changes.
…2026 copyright As the author chose: - README: "What AI tools did" is one generic sentence that keeps the 2026 mathematical review and reconstruction alongside the code, docs and Lean work. - CONTRIBUTORS.md: Nelson Spence's line matches the README's split between the original framework and the 2026 revision, with responsibility for the final claims. - Copyright 2025-2026 in NOTICE.md, the README and zensical.toml (was 2026, and 2024-2026 from the docs scaffold); the framework dates from April 2025.
Stage B of the research revision on top of Stage A (
692054a): editorial and publication cleanup, the stack diagram as paper figures and a docs page, vendor-neutral agent guidance, and the corrections from the review of1fa270d. Rebased onmainat9663329; the Scorecard commit was dropped because #101 removed the workflow. No theorem, proof, operator or numerical model changes except where stated.What changed
paper/cd_stack.dot, rendered bypaper/stack_figures.pyas the docs SVG and paper Figures 1 and 2; audited against the paper (edges, the finite-graph hypotheses, Proposition 3.21 as a counterexample to necessity).scripts/check_stack_citations.pyrequires every cited statement to have a matching header in the rebuilt PDF. New docs page, The CD Stack.paper/build_figures.shrenders in the image ofpaper/figures.Dockerfile(Debian by digest, packages from the 2026-09-18 snapshot, DM Sans and Fraunces by SHA-256; checkout read-only, no network).checkrequires all four committed outputs to be byte-identical to the render;paper.ymlruns it and builds the paper from the rendered figures. Committed outputs re-rendered and the paper rebuilt: text identical, pages 5 and 18 differ, one edge route in Figure 2 changed.presence_statisticskeeps its 1e-10 support floor (review B3); the 1e-6 zero-branch tolerance is not reused. Regression at max 5e-7.tests/README.md(what the tests establish, when a test fails);AGENTS.md,CONTRIBUTING.mdand the validator agent point to it (review B4).858fad2: bug template is uv only; the Lemma 3.10 test cites its lemma;eigenvalues.pylabels each threshold clause; the README says the Lean counterpart of Theorem 3.16 concludes positivity at one interior point only.AGENTS.mdwithCLAUDE.mdas@AGENTS.md;cliff.tomlandrequirements.txtremoved.Author decisions (applied)
3d5fe95), threshold paragraph tightened (c78002f).e9f4454).3f4e075).6f22aa6); the review is credited generically, AI assistance is one generic sentence,CONTRIBUTORS.mdmatches, copyright 2025-2026 (ebc86f7).Verification at
ebc86f7906115b; no package or test change since)