Project 8: Proof-Driven Fundamental Theorem Workbench

Build a theorem workbench that links formal statements (rank-nullity and FTLA) to executable checks and automated counterexamples for weakened claims.

Quick Reference

Attribute Value
Difficulty Expert (Level 4)
Time Estimate 2 weeks
Language Python + Markdown (optional Lean/Coq)
Prerequisites Proof basics, subspaces, rank/nullity
Key Topics FTLA, theorem contracts, counterexample engineering

1. Learning Objectives

  1. Write theorem statements with explicit assumptions and quantifiers.
  2. Prove core claims (rank-nullity, orthogonality relationships).
  3. Turn theorem assumptions into executable precondition checks.
  4. Auto-generate counterexamples when assumptions are removed.
  5. Separate mathematical violations from numerical tolerance artifacts.

2. Theoretical Foundation

2.1 Core Concepts

  • Rank-nullity identity as structural conservation law.
  • Four fundamental subspaces and orthogonality relations.
  • Proof contracts: assumption list + conclusion scope.
  • Counterexample discipline for claim hardening.

2.2 Why This Matters

Proofs and tests should reinforce each other. In production math code, theorems become API contracts. If assumptions are not encoded, pipelines fail silently in edge cases.

2.3 Historical Context / Background

Linear algebra education evolved from elimination procedures toward structural theorems. Modern scientific software engineering increasingly requires this theorem-contract perspective.

2.4 Common Misconceptions

  • Numerical success implies theorem truth.
  • Rank condition alone decides both existence and uniqueness.
  • A theorem can be “almost true” without explicit assumptions.

3. Project Specification

3.1 What You Will Build

A notebook + CLI toolkit that:

  • Stores theorem statements and assumptions
  • Executes symbolic/numeric verification workflows
  • Produces counterexample bundles for weakened variants

3.2 Functional Requirements

  1. Encode at least three theorem statements formally.
  2. Verify theorem predicates across random and adversarial matrices.
  3. Generate counterexamples when assumptions are intentionally relaxed.
  4. Export proof/test trace reports.

3.3 Non-Functional Requirements

  • Traceability: every check links to theorem clause.
  • Reproducibility: deterministic seeds and tolerance config.
  • Pedagogy: outputs readable by humans, not only machines.

3.4 Example Usage / Output

$ python theorem_workbench.py --claim rank_nullity --trials 400
[INFO] claim=rank_nullity
[PASS] dim(domain)=rank+nullity for all trials
[INFO] weakened_claim=uniqueness_without_null_check
[FOUND] counterexample matrix_id=adv_017
[REPORT] saved to reports/ftla_run_2026-02-12.md

3.5 Real World Outcome

You obtain a reusable theorem-verification harness that can gate linear-algebra modules in CI by mathematical preconditions, not only unit outputs.

4. Solution Architecture

4.1 High-Level Design

Claim Registry -> Assumption Checker -> Proof/Experiment Runner -> Counterexample Engine -> Reporter

4.2 Key Components

Component Responsibility Key Decisions
Claim Registry Stores theorem text and clauses Structured schema with quantifiers
Assumption Checker Validates matrix/map conditions Exact + tolerance-aware modes
Runner Executes validation trials Separate symbolic/numeric pathways
Counterexample Engine Break weakened claims Adversarial matrix generators
Reporter Writes proof-test trace Clause-level pass/fail mapping

4.3 Data Structures

TheoremClaim:
  id
  assumptions[]
  conclusion
  proof_notes
  validators[]

4.4 Algorithm Overview

  1. Load theorem claim.
  2. Validate assumptions for each candidate input.
  3. Evaluate theorem conclusion.
  4. If weakened mode: search for violating witness.
  5. Emit reproducible report.

5. Implementation Guide

5.1 Development Environment Setup

Set up Python environment
Install symbolic and notebook dependencies
Enable deterministic seeds in config

5.2 Project Structure

P08/
  claims/
  proofs/
  validators/
  counterexamples/
  reports/

5.3 The Core Question You’re Answering

“How can theorem assumptions be transformed into executable engineering contracts?”

5.4 Concepts You Must Understand First

  1. Rank-nullity theorem
  2. Orthogonality of row/null and col/left-null spaces
  3. Quantifiers and counterexample logic

5.5 Questions to Guide Your Design

  1. Which matrix families stress each theorem clause hardest?
  2. How do you report near-failures due to numerical precision?

5.6 Thinking Exercise

Write a false claim by deleting one assumption from a true theorem. Predict the smallest counterexample shape.

5.7 The Interview Questions They’ll Ask

  1. How do rank and nullity partition information flow?
  2. Why do orthogonality relations matter for least squares?
  3. What is the difference between proof and empirical evidence?
  4. How do you encode theorem assumptions in software APIs?
  5. Why are counterexamples first-class artifacts?

5.8 Hints in Layers

  • Hint 1: Start with integer matrices where exact arithmetic is easy.
  • Hint 2: Add structured adversarial generators (duplicate rows, nearly dependent columns).
  • Hint 3: Keep weakened-claim mode explicit and separate.
  • Hint 4: Report assumptions satisfied/unsatisfied before conclusions.

5.9 Books That Will Help

Topic Book Chapter
FTLA Strang Fundamental subspaces
Linear map proofs Axler Early theorem chapters
Proof methodology Hefferon Logic/proof appendices

5.10 Implementation Phases

  1. Claim schema and parser
  2. Exact arithmetic validators
  3. Counterexample engine
  4. Numeric mode and tolerance analysis

5.11 Key Implementation Decisions

  • Keep exact rational mode as source of truth.
  • Treat floating-point checks as approximation diagnostics, not proof.

6. Testing Strategy

6.1 Test Categories

  • Theorem-positive fixtures
  • Weakened-claim negatives
  • Numerical edge cases

6.2 Critical Test Cases

  1. Rank-nullity on random full-rank and rank-deficient matrices.
  2. Orthogonality checks using exact arithmetic.
  3. Counterexample generation for claim variants.

6.3 Test Data

  • Hand-crafted matrices + seeded random families.

7. Common Pitfalls & Debugging

  • Symptom: False theorem failures in float mode.
    • Why: Tolerance too strict for conditioning.
    • Fix: Condition-aware thresholds.
    • Quick test: Compare with exact mode.
  • Symptom: No counterexamples found for false claim.
    • Why: Search space lacks adversarial structures.
    • Fix: Add deterministic structured generators.
    • Quick test: Inject known violating fixture.

8. Extensions & Challenges

  • Integrate with Lean/Coq as formal proof companion.
  • Add theorem dependency graph visualization.
  • Add “proof debt” tracker for unproven assumptions.

9. Real-World Connections

  • CI gating for linear solver libraries.
  • Verification harnesses for ML preprocessing pipelines.
  • Educational proof assistants for engineering math courses.

10. Resources

11. Self-Assessment Checklist

  • I can restate each theorem with explicit assumptions.
  • I can generate counterexamples for weakened variants.
  • My report maps failures to specific theorem clauses.
  • I can explain differences between proof and numeric checks.

12. Submission / Completion Criteria

  • Completed theorem registry with at least three claims.
  • Reproducible report showing proof checks + counterexamples.
  • One note explaining tolerance policy and its limits.

This guide expands Project 8 from LINEAR_ALGEBRA_LEARNING_PROJECTS.md.