cloning org repos...
cloned .github
cloned program
cloned atlas
cloned sieve
cloned lean
cloned k7
cloned k7-lean
fetched https://arithmon.com/
==========================================================================
ARITHMON CROSS-REPO CONSISTENCY REPORT
==========================================================================
ledger source : program/LEDGER.json
errors : 3
warnings : 12
-- axiom-count ---------------------------------------------------------
[FAIL] k7-lean 14 `axiom` declarations found, ledger says 15
. K3_eigenvalue_0
. K3_eigenvalue_0_bracketed
. K3_eigenvalue_1
. K3_eigenvalue_1_bracketed
. K3_eigenvalue_2
. K3_eigenvalue_2_bracketed
. K3_eigenvalue_3
. K3_eigenvalue_3_bracketed
. cheeger_inequality
. det_g_at_half
. det_g_at_half_bracketed
. literature_package
. neck_dominates
. spectral_upper_bound
-- count-drift ---------------------------------------------------------
[FAIL] k7-lean claim surface says '14 stated axioms' vs ledger axioms 15
. CITATION.cff:14
[FAIL] k7-lean claim surface says '14 axioms' vs ledger axioms 15
. README.md:53
-- root-version --------------------------------------------------------
[WARN] k7-lean GIFT.lean: no version string in first 15 lines
-- citation-cff --------------------------------------------------------
[WARN] .github no CITATION.cff: GitHub will not show a 'Cite this repository' button
[WARN] program no CITATION.cff: GitHub will not show a 'Cite this repository' button
[WARN] atlas no CITATION.cff: GitHub will not show a 'Cite this repository' button
[WARN] sieve no CITATION.cff: GitHub will not show a 'Cite this repository' button
[WARN] lean no CITATION.cff: GitHub will not show a 'Cite this repository' button
-- external-citation ---------------------------------------------------
[WARN] program README does not carry the indexed Physics Letters B citation in full form
-- doi-undocumented ----------------------------------------------------
[WARN] k7-lean 10.5281/zenodo.18920368 is cited only inside source code, never in any README, .cff or .bib: it is invisible to a reader and unverifiable by CI
. program/LEDGER.json
. k7-lean/GIFT/Foundations/Analysis/K7Orthonormality.lean
. k7-lean/GIFT/Spectral/ComputedWeylLaw.lean
-- axiom-taxonomy ------------------------------------------------------
[WARN] - the 15 axioms are characterised in 3 incompatible ways (chain, other, taxonomy): the count agrees but the description of what the 4 non-K3 axioms *are* does not
. chain: k7/publications/papers/markdown/k7_framework_3_5_S1_foundations.md:9
. other: k7/publications/outreach/k7_one_page.md:29
. taxonomy: k7/STRUCTURE.md:111
-- stale-link ----------------------------------------------------------
[WARN] - github.com/gift-framework/core still referenced in 4 file(s); currently redirects (200 https://github.com/Arithmon/K7-Lean). The redirect dies if that name is reused.
. k7/publications/papers/markdown/k7_framework_3_5_main.md
. k7/publications/papers/tex/k7_framework_3_5_main.tex
. k7/publications/outreach/joyce_theorem_now_in_lean.md
. k7/publications/outreach/13_theorems_zero_trust_required.md
-- line-endings --------------------------------------------------------
[WARN] k7 11 file(s) with CRLF endings: grep-based CI rules can diverge between machines
. SECURITY.md
. CODE_OF_CONDUCT.md
. publications/references/Bibliography.md
. publications/references/INDEPENDENT_VALIDATIONS.md
. publications/references/README.md
. publications/outreach/gift_from_bit.md
. publications/outreach/on_what_comes_first.md
. .github/scripts/fix_em_dashes.py
. .github/scripts/observable_calculator.py
. .github/scripts/cross_repo_check.py
[WARN] k7-lean 15 file(s) with CRLF endings: grep-based CI rules can diverge between machines
. GIFT/Foundations/K3HarmonicCorrection.lean
. GIFT/Foundations/NewtonKantorovich.lean
. GIFT/Foundations/ExplicitG2Metric.lean
. GIFT/Foundations/Analysis/HodgeTheory.lean
. GIFT/Foundations/Analysis/WedgeProduct.lean
. GIFT/Foundations/Analysis/E8Lattice.lean
. GIFT/Foundations/Analysis/K7Orthonormality.lean
. GIFT/Spectral/ComputedYukawa.lean
. GIFT/Spectral/ComputedWeylLaw.lean
. GIFT/Spectral/SpectralDemocracy.lean
-- lean-sorry ----------------------------------------------------------
[ok ] lean 0 real `sorry` (comments excluded, ledger allows 0)
[ok ] k7-lean 0 real `sorry` (comments excluded, ledger allows 0)
-- frozen-prediction ---------------------------------------------------
[ok ] - δ_CP = 197° consistent across 7 claim-surface assertion(s)
-- vocabulary ----------------------------------------------------------
[ok ] - no retired wording on live surfaces (3 form(s) tracked)
The scheduled cross-repo audit found at least one blocking inconsistency.
Canonical numbers live in
LEDGER.json. If the ledger is what changed,update the claim surfaces. If a claim surface is right, fix the ledger.
Full report