- Cargo.lock was generated but not tracked in initial commit
- Required for reproducible builds across machines
- Already in GDrive backup; this aligns Git with that state
- Fix q16_div to use truncation-toward-zero (matching q16_mul) so that
negative intermediates in intermittency produce correct Q16.16 values
- Correct Hagen-Poiseuille attribution in laminar branch comment
- Update preamble note to cover both q16_mul and q16_div truncation
- All 24 theorems still pass, build clean (3527 jobs)
Implements the UniversalBridge module in Lean with Q16.16 fixed-point
arithmetic, connecting the laminar exit (Re=2300, f=0.0278) and turbulent
entry (Re=4000, f=0.0398) with provable C¹ continuity.
Includes 24 verification theorems (boundary conditions, basis function
values, regime classification, controller gate semantics) and 10
executable #eval! witnesses as computational receipts.
Sourcery-bot housekeeping note on PR #11: REPO_ROOT was only mentioned
in comments after the cwd-resolution fix in 61005655 and was no longer
used by any logic in this module (other math-first scripts have their
own REPO_ROOT constants). Removed it. Folded the rationale that
previously lived in the comment above the constant into the
_git_toplevel docstring so future readers still see why we don't
hardcode the cwd.
Co-Authored-By: Allaun Silverfox <bigdataiscoming+9i37y6j2@protonmail.com>
Addresses Devin Review on PR #11 ("Staged regression test passes
vacuously — git diff runs in real repo, not temp repo").
Root cause:
scripts/math-first/require_math_evidence.py hardcoded
cwd=REPO_ROOT on the git subprocess. REPO_ROOT is computed from
__file__, which always resolves to the REAL repo path -- even when
the test invokes the script with cwd=tmp_path. So 'git diff
--cached --name-only' queried the real (clean) repo, returned an
empty list, and the script exited 0 via the noop short-circuit.
The regression test then printed OK while never actually
exercising the --staged classification logic.
Fix:
Introduce _git_toplevel() in require_math_evidence.py that runs
'git rev-parse --show-toplevel' from the *inherited* cwd. Both
_files_from_staged() and _files_from_git_diff() now use that
toplevel as their subprocess cwd. Pre-commit and CI both invoke
the script from inside the repo root anyway, so behaviour in
production is unchanged; only the test (and any other caller
that runs the script from a non-Research-Stack directory) now
works correctly.
Test hardening:
test_require_math_evidence.py's staged regression now drives the
script via plain subprocess with cwd=tmp_path (no runpy wrapper,
no os.chdir trickery) and covers three sub-cases against the same
temp repo:
(a) math-track-only staged -> expect exit 1 (negative)
(b) math-track + receipt staged -> expect exit 0 (the bug)
(c) math-track + claims.yaml -> expect exit 0 (registry)
Sub-case (a) is the key addition: with the pre-fix script, this
case wrongly returns 0 (real repo is clean -> noop), so the test
fails loudly. Verified locally by temporarily reverting the cwd
fix -- the test correctly reports
'FAIL staged_regression_negative: expected exit 1, got 0'.
Docs: docs/math-first-tooling.md notes that
receipt-required-for-math-content is a no-op in the CI
pre-commit job (pre-commit's --from-ref/--to-ref mode does not
touch the index, so --staged returns an empty list and the hook
exits 0). PR-scope enforcement of the same rule lives in the
dedicated require-evidence CI job. This addresses the Devin
Review info comment on .pre-commit-config.yaml.
Co-Authored-By: Allaun Silverfox <bigdataiscoming+9i37y6j2@protonmail.com>
Follow-up to PR #10. Addresses comments left by Devin Review.
Primary fix (the BUG comment, .pre-commit-config.yaml:86-87):
The receipt-required-for-math-content hook used files: '<math-track
regex>' with pass_filenames: true. Pre-commit applies that regex to
the staged file list BEFORE invoking the hook, so evidence files
(receipts under shared-data/artifacts/deepseek_review/, claims.yaml)
were stripped from argv. require_math_evidence.py then saw only the
math-track files, found no evidence, and exited 1 -- even when proper
evidence was committed alongside. The only case that worked was
Lean-only commits, because Lean files are dual-classified as both
math-track and evidence.
Fix: drive the hook from the index instead of argv.
* require_math_evidence.py grows a --staged mode that runs
'git diff --cached --name-only' itself, plus a mutex check so
--staged, --from-git-diff, and explicit FILES cannot be combined.
* .pre-commit-config.yaml hook switches to always_run: true,
pass_filenames: false, and 'entry: ... --staged'. The script
exits 0 early when no math-track files are staged, so the cost
of always_run is negligible.
Polish:
* claims-registry.schema.json: add required: ["status"] inside each
'if' subschema. Without it, an entry missing 'status' would also
spuriously trip the 'then' clauses (review_receipts, lean) before
the top-level required catch. Pure error-message cleanup.
* validate_claims_registry.py: replace the catch-all
re.compile(r'^[A-Za-z]+:') with a closed list of well-known URI
schemes (http, https, arxiv, doi, isbn, mailto, urn).
Module-name-shaped strings like 'Module:Theorem' will no longer
silently bypass the on-disk path check.
* validate_claims_registry.py: thread a FormatChecker through the
Draft202012Validator so format-keyword behaviour matches
validate_deepseek_receipts.py. No-op for today's schema but
cheap insurance for the next contributor who adds 'format'.
Regression tests:
* New scripts/math-first/test_require_math_evidence.py covers ten
classification cases plus the actual --staged regression: it spins
up a temp git repo, stages a math-track file + a receipt, invokes
the script with --staged, and asserts exit 0. Without the fix this
case fails, demonstrating the bug end-to-end.
* math-check.yml runs the new self-tests in CI.
Docs: * docs/math-first-tooling.md: document the --staged contract, why
always_run + pass_filenames: false is necessary, and how to run
the new self-tests.
Co-Authored-By: Allaun Silverfox <bigdataiscoming+9i37y6j2@protonmail.com>
pre-commit stashes unstaged changes, runs hooks, then pops the stash.
When the runner's working tree has LFS pointer files but git's LFS
smudge filter is configured (per .gitattributes), the stash/pop cycle
reports a phantom diff against the binary content git thinks it
should smudge, and the pop fails with
"the patch applies to ... which does not match the current contents".
All hooks themselves pass on this PR (validated locally and visible in
the previous CI run for #10). Clearing the LFS filters locally for the
pre-commit job removes the disagreement without mutating the repo or
any LFS-tracked files.
Co-Authored-By: Allaun Silverfox <bigdataiscoming+9i37y6j2@protonmail.com>
Adds automated guardrails so mathematical rigor is enforced by tooling
instead of by convention. See docs/math-first-tooling.md for the full
contract.
Schemas + registry:
- shared-data/schemas/deepseek-review-receipt.schema.json
Draft 2020-12 schema for the existing ollama_deepseek_review_receipt_v1
and ollama_deepseek_review_continuation_receipt_v1 receipt formats. Pins
sha256:<hex> hashes, non-negative token counts, repo-relative POSIX
paths, and rejects additional fields.
- shared-data/schemas/claims-registry.schema.json
Schema for claims.yaml. Requires review_receipts when status is
verified-by-ai and a lean source when status is formally-proven.
- claims.yaml
Initial registry entry: prime-gap-entropy-collapse (verified-by-ai)
linked to the two existing receipts under
shared-data/artifacts/deepseek_review/.
Validators (scripts/math-first/):
- validate_deepseek_receipts.py: validates tracked or passed receipts
against the JSON Schema; shared by pre-commit and CI.
- test_validate_deepseek_receipts.py: positive + 7 negative fixtures
asserting exit-code behaviour.
- validate_claims_registry.py: schema check + unique id check + on-disk
existence check for every referenced repo-relative path.
- require_math_evidence.py: gate that requires a DeepSeek receipt, a
Lean change, or a claims.yaml update alongside edits to math-track
surfaces (Lean Semantics kernels, ArithmeticSpec docs, stack
solidification receipts).
Pre-commit (.pre-commit-config.yaml):
- check-json, check-yaml, end-of-file-fixer, trim trailing whitespace,
detect-private-key (scoped to math-first files only per AGENTS.md
Do Not Sweep).
- Local hooks wiring all three math-first validators above.
CI (.github/workflows/math-check.yml):
- validate-schemas: compiles every schema, runs both validators, runs
the validator self-tests, then re-invokes the canonical Ollama
emitter in --verify-only mode against every tracked receipt to
re-check answer_sha256 against the answer-file bytes on disk.
- require-evidence: enforces the math-track evidence rule at PR scope.
- pre-commit: runs all pre-commit hooks against the PR diff so the
contract holds even for contributors who skip installing hooks
locally.
MCP (.mcp.json):
- filesystem, sympy, wolfram-alpha, lean, deepseek-review entries
pointing at off-the-shelf upstream servers and at the canonical
ollama_deepseek_review_emitter.py. Secrets stay in the runtime env
(WOLFRAM_ALPHA_APPID, OLLAMA_API_KEY) and are never embedded.
Docs (docs/math-first-tooling.md):
- Philosophy, surfaces, schema reference, registry workflow, hook
catalogue, CI catalogue, MCP catalogue, end-to-end verify command.
shared-data/schemas/*.schema.json and claims.yaml live under paths the
top-level .gitignore would normally exclude; they are force-added via
git add -f the same way existing promoted receipts under
shared-data/artifacts/deepseek_review/ are tracked (per AGENTS.md).
Co-Authored-By: Allaun Silverfox <bigdataiscoming+9i37y6j2@protonmail.com>
