Skip to content

Automate direct finite-symbol stability tactic - #333

Merged
PerAlexandersson merged 1 commit into
mainfrom
codex/finite-symbol-auto
Aug 4, 2026
Merged

Automate direct finite-symbol stability tactic#333
PerAlexandersson merged 1 commit into
mainfrom
codex/finite-symbol-auto

Conversation

@PerAlexandersson

Copy link
Copy Markdown
Owner

Summary

  • add rr_finite_symbol_stable_or_zero_auto for goal-directed operator/input inference and local certificate discovery
  • delegate through the existing inferred frontend so all forms invoke the proved finiteSymbol_preserves_stability declaration at one site
  • test selection in the presence of decoy operator and input stability certificates

API boundary

This is only the direct multiaffine stable-or-zero theorem surface. It does not discharge the false legacy homogeneous finite-symbol statement, the conjectural Jensen-pencil implication, the degree-d PF-bidiagonal backend, or an affine-bidiagonal application bridge.

Verification

  • focused external-cache build: RealRooted.Tactic.Examples.FiniteSymbol
  • full external-cache build: RealRooted (8,951 jobs; only pre-existing warnings)
  • python3 scripts/check_root_imports.py
  • git diff --check and touched-file line/placeholder scans
  • Claude Opus/max API and macro review; deduplication and decoy-certificate recommendation applied

@PerAlexandersson
PerAlexandersson merged commit 8499a36 into main Aug 4, 2026
1 check passed
@PerAlexandersson
PerAlexandersson deleted the codex/finite-symbol-auto branch August 4, 2026 06:19
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