Skip to content

Infer derived matrix tactic certificates - #337

Merged
PerAlexandersson merged 1 commit into
mainfrom
codex/inferred-matrix-derived
Aug 4, 2026
Merged

Infer derived matrix tactic certificates#337
PerAlexandersson merged 1 commit into
mainfrom
codex/inferred-matrix-derived

Conversation

@PerAlexandersson

@PerAlexandersson PerAlexandersson commented Aug 4, 2026

Copy link
Copy Markdown
Owner

Summary

  • add bare inferred forms for the six derived matrix and row-threshold endpoints
  • reuse registered rectangularity, nonnegativity/threshold, and 2x2 certificates
  • preserve explicit named and positional frontend coverage and add a decoy-matrix smoke example

Verification

  • lake ... build RealRooted.Tactic.Examples.Matrix (8625 jobs)
  • lake ... build RealRooted (8951 jobs)
  • python3 scripts/check_root_imports.py
  • python3 scripts/generate-oeis-tactic-coverage.py --check
  • git diff --check
  • touched line-length and placeholder scans

All tactics invoke existing proved theorem declarations; no theorem files are changed.

@PerAlexandersson
PerAlexandersson merged commit 41d589c into main Aug 4, 2026
1 check passed
@PerAlexandersson
PerAlexandersson deleted the codex/inferred-matrix-derived branch August 4, 2026 10:54
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant