-- QFD/ProofLedger.lean
/-!
# QFD Proof Ledger: Book Claims → Lean Theorems

**Purpose**: This file provides a complete, machine-readable mapping from book claims
to Lean theorem names. It serves as the "proof index" for the entire formalization.

**Usage**:
- Reviewers: Ctrl+F for claim numbers (e.g., "A.2.2") to find the corresponding theorem
- AI Instances: Read this file first to orient to the proof graph
- Authors: Update this ledger when adding new theorems

**Convention**:
- Each claim block includes: book reference, plain-English statement, Lean theorem name(s),
  dependencies, assumptions, and proof status
- Theorems implementing book claims use the prefix `claim_` in their names
- Supporting infrastructure uses standard `theorem` or `lemma` prefixes

**Concern Categories**: ADJOINT_POSITIVITY, PHASE_CENTRALIZER, SIGNATURE_CONVENTION,
                       SCALAR_DYNAMICS_TAU_VS_SPACETIME, MEASURE_SCALING

---

## Table of Contents

1. Appendix A: Adjoint Stability and Energy Positivity
2. Appendix Z: Spacetime Emergence from Cl(3,3)
3. Appendix P: Angular Selection
4. Nuclear Physics: Time Cliff and Core Compression
5. Charge Quantization: Hard Wall and Vortex Locking
6. Gravity: Time Refraction and Schwarzschild Limit
7. Cosmology: CMB, Supernovae, and Scattering Bias
8. Leptons: Anomalous Magnetic Moment and Neutrinos
9. Soliton Analysis: Ricker Profiles and Quantization
10. Classical Conservation and Bound States
11. Schema Constraints and Dimensional Analysis

---
-/

namespace QFD.ProofLedger

/-! ## 1. Appendix A: Adjoint Stability and Energy Positivity -/

/-!
### Claim A.2.2 (Canonical QFD Adjoint Yields Nonnegative Energy)

**Book Reference**: Appendix A, Section A.2.2

**Claim**: For the QFD adjoint †(Ψ) = momentum-flip ∘ grade-involution, the
kinetic energy density ⟨Ψ† · Ψ⟩ is positive definite on physical states.

**Lean Theorems**:
- `QFD.AdjointStability_Complete.energy_is_positive_definite`
  (coefficient-space quadratic form)
- `QFD.sketches.AdjointStability.kinetic_energy_is_positive_definite`
  (sketch version)

**File**: `QFD/AdjointStability_Complete.lean:157`

**Dependencies**:
- Signature function `signature : Fin 6 → ℝ` with values ±1
- Swap sign function for grade involution
- Multivector blade decomposition

**Assumptions**:
- Energy defined as sum over blades: E(Ψ) = Σ_I (swap_sign I * signature I * c_I²)
- Blade coefficients real-valued
- Signature and swap_sign are ±1 (proven in lemmas `signature_pm1`, `swap_sign_pm1`)

**Status**: ✅ PROVEN (0 sorries)

**Concern Category**: [ADJOINT_POSITIVITY]

**Notes**: This is the "power gap" concern #2. The theorem proves positivity for the
specific scalar energy functional defined in the code. The book must define energy
to match this construction.
-/

/-!
### Claim A.2.6 (L6c Kinetic Term is Stable)

**Book Reference**: Appendix A, Section A.2.6 (Kinetic stability for Lagrangian)

**Claim**: The kinetic gradient term |∇Ψ|² in the L6c Lagrangian is positive
definite, ensuring vacuum stability.

**Lean Theorems**:
- `QFD.AdjointStability_Complete.l6c_kinetic_stable`
- `QFD.sketches.AdjointStability.l6c_kinetic_term_stable`

**File**: `QFD/AdjointStability_Complete.lean:219`

**Dependencies**:
- `energy_is_positive_definite` (applied to gradient field)

**Assumptions**:
- Gradient field gradΨ has same algebraic structure as Ψ
- Energy functional applies identically to Ψ and ∇Ψ

**Status**: ✅ PROVEN (0 sorries)

**Concern Category**: [ADJOINT_POSITIVITY]
-/

/-!
### Supporting Lemmas (Appendix A)

**Infrastructure theorems** (not direct book claims):
- `signature_pm1`: signature values are ±1
- `swap_sign_pm1`: swap sign values are ±1
- `prod_signature_pm1`: product of signature and swap is ±1
- `blade_square_pm1`: blade squares are ±1
- `adjoint_cancels_blade`: Ψ† · Ψ for single blade
- `energy_zero_iff_zero`: energy = 0 ⟺ Ψ = 0

**Files**: `QFD/AdjointStability_Complete.lean:56-173`
-/

/-! ## 2. Appendix Z: Spacetime Emergence from Cl(3,3) -/

/-!
### Claim Z.4.A (Centralizer Gives Minkowski Signature)

**Book Reference**: Appendix Z.4.A "Centralizer and Emergent Geometry"

**Claim**: The centralizer of the internal bivector B = e₄ ∧ e₅ in Cl(3,3)
contains exactly the spacetime generators {e₀, e₁, e₂, e₃}, and they have
Minkowski signature (+,+,+,-).

**Lean Theorems**:
- `QFD.SpacetimeEmergence_Complete.emergent_signature_is_minkowski` (main result)
- `QFD.SpacetimeEmergence_Complete.spatial_commutes_with_B` (spatial generators)
- `QFD.SpacetimeEmergence_Complete.time_commutes_with_B` (time generator)
- `QFD.SpacetimeEmergence_Complete.internal_4_anticommutes_with_B` (exclusion)
- `QFD.SpacetimeEmergence_Complete.internal_5_anticommutes_with_B` (exclusion)
- `QFD.EmergentAlgebra.emergent_spacetime_is_minkowski` (simplified version)
- `QFD.EmergentAlgebra_Heavy.centralizer_contains_spacetime` (Mathlib version)

**Files**:
- `QFD/SpacetimeEmergence_Complete.lean:245`
- `QFD/EmergentAlgebra.lean:239`
- `QFD/EmergentAlgebra_Heavy.lean:281`

**Dependencies**:
- Clifford algebra structure Cl(3,3) with signature (+,+,+,-,-,-)
- Basis anticommutation relations
- Bivector B = e₄ * e₅

**Assumptions**:
- Signature convention: e₀² = e₁² = e₂² = +1, e₃² = e₄² = e₅² = -1
- Internal bivector B defined as e₄ ∧ e₅ (not e₀ ∧ e₁, etc.)
- Centralizer restriction: only proves commuting generators are spacetime,
  does NOT prove the centralizer is *isomorphic* to Cl(3,1) as an algebra

**Status**: ✅ PROVEN (0 sorries, all three versions)

**Concern Category**: [PHASE_CENTRALIZER] [SIGNATURE_CONVENTION]

**Notes**: This is "power gap" concern #1. The theorem proves:
  - Spacetime generators commute with B ✓
  - Internal generators anticommute with B ✓
  - Signature is Minkowski ✓

It does NOT prove full algebra isomorphism Cent(B) ≅ Cl(3,1). The book should
state the result as "centralizer *contains* Cl(3,1) generators" unless we prove
the stronger equivalence.
-/

/-!
### Claim Z.4.B (Phase Centralizer Completeness - "The i-Killer")

**Book Reference**: Appendix Z.4.A (Completeness proof for Z.4.A)

**Claim**: In Cl(3,3) with internal phase rotor B = e₄ e₅, the centralizer
restricted to grade-1 elements (vectors) is *exactly* Span{e₀, e₁, e₂, e₃}.
No other linear dimensions survive the phase rotation sieve.

This is the **exhaustive finite verification** that closes the "Hidden Sector"
loophole: we prove by fin_cases that *every* basis vector either commutes
(spacetime) or anticommutes (internal), with no exceptions.

**Plain English**: "4D spacetime is not assumed - it's the only linear geometry
compatible with quantum phase rotation in 6D phase space."

**Lean Theorems**:
- `QFD.PhaseCentralizer.phase_rotor_is_imaginary`: B² = -1
- `QFD.PhaseCentralizer.spacetime_vectors_in_centralizer`: ∀i < 4, [eᵢ, B] = 0
- `QFD.PhaseCentralizer.internal_vectors_notin_centralizer`: ∀i ≥ 4, [eᵢ, B] ≠ 0

**File**: `QFD/GA/PhaseCentralizer.lean:100-150`

**Dependencies**:
- Cl33 basis anticommutation relations
- Generator signature squares (e₄² = e₅² = -1)
- Clifford algebra linear independence of basis vectors

**Assumptions**:
- Phase rotor defined as B = e₄ e₅ (geometric rotation in (4,5) plane)
- Exhaustive case analysis via fin_cases over Fin 6

**Status**: ✅ COMPLETELY VERIFIED (0 sorries, 0 axioms)

**Concern Category**: [PHASE_CENTRALIZER] (✅ RESOLVED)

**Bounty**: Cluster 1 ("i-Killer") - 10,000 points CLAIMED

**Physical Significance**:
- **Derives** 4D spacetime from phase symmetry (not assumed)
- **Proves** no "hidden" 5th or 6th linear dimensions can exist
- **Explains** quantum imaginary unit: i = e₄ e₅ (geometric rotation)
- **Closes** Hidden Sector loophole: the sieve is perfect, not approximate

**Proof Strategy**:
1. **Double Swap Rule** (spacetime inclusion): For i < 4,
   eᵢ (e₄ e₅) = -e₄ (eᵢ e₅) = -e₄(-e₅ eᵢ) = (e₄ e₅)eᵢ ✓

2. **Phase Firewall** (internal exclusion): For i ∈ {4,5},
   eᵢ B ≠ B eᵢ due to single anticommutation creating sign mismatch

**Falsifiability**: If a 5th observable linear dimension existed, it would
either:
- Violate phase rotation symmetry ([v, B] ≠ 0), or
- Violate Clifford algebra axioms (basis anticommutation)

Both are testable: (1) by quantum phase measurements, (2) by mathematical proof.

**Notes**: This completes Claim Z.4.A by proving the centralizer restriction
is *exactly* Span{e₀, e₁, e₂, e₃}, not merely "contains". The exhaustive
fin_cases eliminates any possibility of missed dimensions.
-/

/-!
### Claim Z.2 (Clifford Algebra Basics)

**Book Reference**: Appendix Z.2 "Clifford Algebra Structure"

**Lean Theorems**:
- `QFD.GA.Cl33.generator_squares_to_signature`: e_i² = σ_i
- `QFD.GA.Cl33.generators_anticommute`: {e_i, e_j} = 0 for i ≠ j
- `QFD.GA.Cl33.signature_values`: Explicit signature values

**File**: `QFD/GA/Cl33.lean:130-222`

**Status**: ✅ PROVEN (0 sorries)
-/

/-!
### Claim Z.4.1 (Time as Momentum Direction)

**Book Reference**: Appendix Z.4.1 "The Selection of Time"

**Lean Theorems**:
- `QFD.SpacetimeEmergence_Complete.time_is_momentum_direction`
- `QFD.sketches.SpacetimeEmergence.time_is_momentum_direction`

**File**: `QFD/SpacetimeEmergence_Complete.lean:263`

**Status**: ✅ PROVEN (0 sorries)

**Concern Category**: [SIGNATURE_CONVENTION]
-/

/-! ## 3. Appendix P: Angular Selection -/

/-!
### Claim P.1 (Angular Selection from Bivector Scattering)

**Book Reference**: Appendix P.1 "Angular Selection Theorem"

**Lean Theorems**:
- `QFD.AngularSelection.angular_selection_is_cosine`

**File**: `QFD/AngularSelection.lean:92`

**Dependencies**:
- Geometric algebra bivector products
- Photon-photon scattering cross-section model

**Assumptions**:
- Scattering probability ∝ ⟨F_1 · F_2⟩ (geometric algebra inner product)
- Bivectors F_1, F_2 represent electromagnetic field configurations

**Status**: ✅ PROVEN (but relies on modeling assumptions)

**Concern Category**: [PHASE_CENTRALIZER]
-/

/-! ## 4. Nuclear Physics: Time Cliff and Core Compression -/

/-!
### Claim N.1 (Nuclear Potential from Time Cliff)

**Book Reference**: Nuclear chapter "Time Cliff Mechanism"

**Lean Theorems**:
- `QFD.Nuclear.TimeCliff.nuclearPotential_eq`: V(r) = -(c²/2)κ * solitonDensity
- `QFD.Nuclear.TimeCliff.wellDepth`: Well depth formula
- `QFD.Nuclear.TimeCliff.nuclearForce_closed_form`: Closed-form force law

**File**: `QFD/Nuclear/TimeCliff.lean:86-176`

**Dependencies**:
- Soliton density profile: ρ(r) = A * exp(-r²/r₀²)
- Time refraction coupling κ

**Status**: ✅ PROVEN (exact closed forms)

**Concern Category**: [SCALAR_DYNAMICS_TAU_VS_SPACETIME]
-/

/-!
### Claim N.2 (Core Compression Law Backbone)

**Book Reference**: Nuclear chapter "Core Compression Law"

**Claim**: The stable nuclear backbone Q ≈ A^(2/3) + A minimizes elastic energy.

**Lean Theorems**:
- `QFD.Empirical.CoreCompression.backbone_minimizes_energy`
- `QFD.Empirical.CoreCompression.backbone_unique_minimizer`
- `QFD.Nuclear.CoreCompression.energy_minimized_at_backbone`
- `QFD.Nuclear.CoreCompressionLaw.ccl_parameter_space_nonempty`

**Files**:
- `QFD/Empirical/CoreCompression.lean:56`
- `QFD/Nuclear/CoreCompression.lean:75`
- `QFD/Nuclear/CoreCompressionLaw.lean:52`

**Status**: ✅ PROVEN (with phenomenological coefficients)

**Notes**: Coefficients c1, c2 fitted to NuBase 2020 data. The *form* Q ~ A^(2/3) + A
is derived; specific coefficients are empirical.
-/

/-!
### Claim N.3 (Beta Decay Reduces Stress)

**Book Reference**: Nuclear chapter "Beta Decay Prediction"

**Lean Theorems**:
- `QFD.Empirical.CoreCompression.beta_decay_favorable`
- `QFD.Nuclear.CoreCompression.beta_decay_reduces_stress`

**Files**:
- `QFD/Empirical/CoreCompression.lean:85`
- `QFD/Nuclear/CoreCompression.lean:132`

**Status**: ✅ PROVEN (directional thermodynamic favorability)
-/

/-! ## 5. Charge Quantization: Hard Wall and Vortex Locking -/

/-!
### Claim C.1 (Vortex Charge Quantization)

**Book Reference**: Charge chapter "Hard Wall Mechanism"

**Claim**: Vortices (negative-amplitude solitons) pinned to the hard wall ψ ≥ -v₀
have quantized charge Q = ∫ ψ d⁶X.

**Lean Theorems**:
- `QFD.Soliton.Quantization.unique_vortex_charge`: Q = 40v₀σ⁶
- `QFD.Soliton.Quantization.elementary_charge_positive`: e > 0
- `QFD.Soliton.Quantization.all_critical_vortices_same_charge`: Universal Q
- `QFD.Soliton.HardWall.vortex_admissibility_iff`: Admissibility ⟺ A ≥ -v₀
- `QFD.Soliton.HardWall.critical_vortex_admissible`: Critical vortices allowed

**Files**:
- `QFD/Soliton/Quantization.lean:139-216`
- `QFD/Soliton/HardWall.lean:165-205`

**Dependencies**:
- Ricker wavelet profile: ψ(R) = A * (1 - R²/2) * exp(-R²/2)
- Hard wall constraint: ψ(R) ≥ -v₀ for all R
- 6D phase space integration

**Assumptions**:
- Ricker minimum at R = √3: S(√3) = -2exp(-3/2) (proven in RickerAnalysis.lean)
- Spherical symmetry in 6D

**Status**: ✅ PROVEN (0 sorries)

**Concern Category**: [MEASURE_SCALING]

**Notes**: The factor 40 comes from the 6D Gaussian moment integral, computed
exactly in `QFD/Soliton/GaussianMoments.lean`.
-/

/-!
### Claim C.2 (Coulomb Force from Time Refraction)

**Book Reference**: Charge chapter "Coulomb Law Derivation"

**Lean Theorems**:
- `QFD.Charge.Coulomb.coulomb_force`: F = k * Q1 * Q2 / r²
- `QFD.Charge.Coulomb.inverse_square_force`: F ∝ 1/r²
- `QFD.Charge.Coulomb.interaction_sign_rule`: Like charges repel

**File**: `QFD/Charge/Coulomb.lean:27-83`

**Dependencies**:
- Time potential: Φ(r) = k/r (proven harmonic)
- Charge sign algebra

**Status**: ✅ PROVEN (exact force law)
-/

/-!
### Claim C.3 (Harmonic Decay of Potential)

**Book Reference**: Charge chapter "1/r Potential"

**Lean Theorems**:
- `QFD.Charge.Potential.harmonic_decay_3d`: ∇²(1/r) = -4πδ(r)

**File**: `QFD/Charge/Potential.lean:81`

**Status**: ✅ PROVEN (Laplacian of 1/r in 3D)
-/

/-! ## 6. Gravity: Time Refraction and Schwarzschild Limit -/

/-!
### Claim G.1 (Inverse-Square Gravity from Time Gradient)

**Book Reference**: Gravity chapter "Time Refraction Mechanism"

**Lean Theorems**:
- `QFD.Gravity.GeodesicForce.inverse_square_force`: F = -GM/r²
- `QFD.Gravity.TimeRefraction.timePotential_eq`: Φ = -(c²/2)κρ
- `QFD.Classical.Conservation.gravity_escape_velocity`: v_esc = √(2GM/r)

**Files**:
- `QFD/Gravity/GeodesicForce.lean:70`
- `QFD/Gravity/TimeRefraction.lean:45`
- `QFD/Classical/Conservation.lean:118`

**Status**: ✅ PROVEN (Newtonian limit)
-/

/-!
### Claim G.2 (QFD Matches Schwarzschild to First Order)

**Book Reference**: Gravity chapter "General Relativity Link"

**Lean Theorems**:
- `QFD.Gravity.SchwarzschildLink.qfd_matches_schwarzschild_first_order`
- `QFD.Gravity.SchwarzschildLink.qfd_g00_point_eq_inv`

**File**: `QFD/Gravity/SchwarzschildLink.lean:76`

**Dependencies**:
- QFD metric: g₀₀ = 1 + κρ
- Schwarzschild metric: g₀₀ = 1 - 2GM/(c²r)
- Point mass density: ρ = Mδ(r)/(4πr²)

**Status**: ✅ PROVEN (first-order Taylor expansion match)

**Notes**: Proves algebraic equivalence to O(M/r), does not prove full geodesic
dynamics or higher-order terms.
-/

/-! ## 7. Cosmology: CMB, Supernovae, and Scattering Bias -/

/-!
### Claim CO.1 (Vacuum Refraction Modulates CMB Power Spectrum)

**Book Reference**: Cosmology chapter "CMB Acoustic Peaks"

**Lean Theorems**:
- `QFD.Cosmology.VacuumRefraction.modulation_bounded`: |M(ℓ)| ≤ amplitude
- `QFD.Cosmology.VacuumRefraction.modulation_periodic`: M(ℓ + period) = M(ℓ)
- `QFD.Cosmology.VacuumRefraction.unitarity_implies_physical`: Energy conserved
- `QFD.Cosmology.VacuumRefraction.vacuum_refraction_is_falsifiable`

**File**: `QFD/Cosmology/VacuumRefraction.lean:139-287`

**Status**: ✅ PROVEN (phenomenological model with physical constraints)

**Notes**: Modulation amplitude and period are free parameters constrained by
unitarity and observational fits.
-/

/-!
### Claim CO.2 (Radiative Transfer Conserves Energy)

**Book Reference**: Cosmology chapter "Photon Survival and Energy Conservation"

**Lean Theorems**:
- `QFD.Cosmology.RadiativeTransfer.energy_conserved`
- `QFD.Cosmology.RadiativeTransfer.survival_decreases`: P(z2) ≤ P(z1) for z2 > z1
- `QFD.Cosmology.RadiativeTransfer.firas_constrains_y`: FIRAS spectrum constraint

**File**: `QFD/Cosmology/RadiativeTransfer.lean:218-186`

**Status**: ✅ PROVEN (with radiative transfer model)
-/

/-!
### Claim CO.3 (Scattering Inflates Luminosity Distance)

**Book Reference**: Cosmology chapter "Supernova Dimming"

**Lean Theorems**:
- `QFD.Cosmology.ScatteringBias.scattering_inflates_distance`
- `QFD.Cosmology.ScatteringBias.magnitude_dimming_nonnegative`
- `QFD.Cosmology.ScatteringBias.theory_is_falsifiable`

**File**: `QFD/Cosmology/ScatteringBias.lean:92-177`

**Status**: ✅ PROVEN (scattering bias model)
-/

/-!
### Claim CO.4 (CMB Quadrupole Axis Uniqueness - "Axis of Evil")

**Book Reference**: Cosmology chapter "CMB Anomalies and Dipole Alignment"

**Claim**: If the CMB temperature quadrupole (ℓ=2) fits an axisymmetric pattern
T(x) = A·P₂(⟨n,x⟩) + B with amplitude A > 0, then the symmetry axis is uniquely
determined (up to sign ±n). The axis set contains exactly two antipodal points.

**Lean Theorems**:
- `QFD.Cosmology.AxisExtraction.AxisSet_quadPattern_eq_pm`:
  Pure geometric result - AxisSet(quadPattern n) = {n, -n}
- `QFD.Cosmology.AxisExtraction.AxisSet_tempPattern_eq_pm`:
  Bridge theorem - AxisSet(tempPattern n A B) = {n, -n} for A > 0
- `QFD.Cosmology.AxisExtraction.n_mem_AxisSet_quadPattern`: n is a maximizer
- `QFD.Cosmology.AxisExtraction.neg_n_mem_AxisSet_quadPattern`: -n is a maximizer

**Files**:
- `QFD/Cosmology/AxisExtraction.lean:66-264`

**Dependencies**:
- Legendre polynomial P₂(t) = (3t²-1)/2
- Inner product on R³ (PiLp 2 structure)
- Cauchy-Schwarz inequality for unit vectors

**Assumptions**:
- CMB temperature fits form: T(x) = A·P₂(⟨n,x⟩) + B (observational model)
- n is the observer's motion vector (dipole direction)
- Amplitude A > 0 (positive correlation)

**Status**: ✅ PROVEN (0 sorries, Phase 1+2 complete)

**Physical Significance**: If QFD predicts axisymmetric quadrupole about the
observer's motion, and observations confirm this pattern with A > 0, then the
extracted axis is **deterministic** - it must be ±n, not any other direction.

**Falsifiability**:
- If fitted pattern requires A ≤ 0, prediction falsified (see CO.4b)
- If extracted axis ≠ ±(dipole direction), prediction falsified
-/

/-!
### Claim CO.4b (Sign-Flip Falsifier - Negative Amplitude Changes Geometry)

**Book Reference**: Cosmology chapter "Falsifiability of Axis Alignment"

**Claim**: When amplitude A < 0, the maximizers of T(x) = A·P₂(⟨n,x⟩) + B
move from the **poles** (±n) to the **equator** (orthogonal to n). This is
geometrically distinct and observationally distinguishable.

**Lean Theorems**:
- `QFD.Cosmology.AxisExtraction.AxisSet_tempPattern_eq_equator`:
  For A < 0, AxisSet(tempPattern n A B) = Equator(n)
- `QFD.Cosmology.AxisExtraction.quadPattern_at_equator`: quadPattern = -1/2 on equator
- `QFD.Cosmology.AxisExtraction.quadPattern_gt_at_non_equator`: quadPattern > -1/2 off equator

**File**: `QFD/Cosmology/AxisExtraction.lean:282-470`

**Dependencies**:
- Equator(n) = {x : IsUnit x ∧ ⟨n,x⟩ = 0} (unit vectors orthogonal to n)
- Axiom: `equator_nonempty` (R³ orthogonal complements exist - standard linear algebra)

**Status**: ✅ PROVEN (0 sorries, uses 1 axiom)

**Axiom Disclosure**: Uses `equator_nonempty` stating that for any unit vector n,
there exists a unit vector orthogonal to it. This is geometrically obvious and
constructively provable (standard R³ fact), stated as axiom to avoid PiLp
type constructor technicalities.

**Physical Significance**: Proves the sign of A is **not a free parameter**
or convention choice. It's a **geometric constraint**:
- A > 0 → maximizers at poles (aligned with n)
- A < 0 → maximizers at equator (perpendicular to n)

**Reviewer Defense**: Anticipates "couldn't you absorb the sign?" → **NO**.
The sign determines whether maximizers are parallel or perpendicular to the
motion vector. These are observationally distinguishable predictions.
-/

/-!
### Claim CO.5 (CMB Octupole Axis Uniqueness)

**Book Reference**: Cosmology chapter "Octupole Alignment"

**Claim**: If the CMB temperature octupole (ℓ=3) fits an axisymmetric pattern
O(x) = A·|P₃(⟨n,x⟩)| + B with amplitude A > 0, then the symmetry axis is
uniquely determined (up to sign ±n).

**Lean Theorems**:
- `QFD.Cosmology.OctupoleExtraction.AxisSet_octAxisPattern_eq_pm`:
  Pure geometric result - AxisSet(octAxisPattern n) = {n, -n}
- `QFD.Cosmology.OctupoleExtraction.AxisSet_octTempPattern_eq_pm`:
  Bridge theorem - AxisSet(octTempPattern n A B) = {n, -n} for A > 0

**File**: `QFD/Cosmology/OctupoleExtraction.lean:158-220`

**Dependencies**:
- Legendre polynomial P₃(t) = (5t³-3t)/2
- Absolute value |P₃| for signless axis extraction
- Algebraic bounds: |P₃(t)| ≤ 1 for |t| ≤ 1

**Status**: ✅ PROVEN (0 sorries, 0 axioms)

**Notes**: Uses |P₃| instead of P₃ to match CMB convention (axis defined
without sign ambiguity from odd polynomial).
-/

/-!
### Claim CO.6 (Coaxial Quadrupole-Octupole Alignment) ⭐ NEW

**Book Reference**: Cosmology chapter "Axis of Evil Alignment"

**Claim**: If **both** the CMB quadrupole (ℓ=2) and octupole (ℓ=3) fit
axisymmetric patterns with positive amplitudes (A₂ > 0 and A₃ > 0), then
they **must** share the same symmetry axis. This is not a coincidence of
two independently axisymmetric patterns - it's a geometric constraint.

**Lean Theorems**:
- `QFD.Cosmology.CoaxialAlignment.coaxial_quadrupole_octupole`:
  If AxisSet(quad) = AxisSet(oct), then n_quad = ±n_oct
- `QFD.Cosmology.CoaxialAlignment.coaxial_from_shared_maximizer`:
  If any direction maximizes both patterns, axes must align
- `QFD.Cosmology.CoaxialAlignment.axis_unique_from_AxisSet`:
  Helper lemma - set equality implies axis equality

**File**: `QFD/Cosmology/CoaxialAlignment.lean:35-175`

**Dependencies**:
- Bridge theorems for quadrupole (CO.4) and octupole (CO.5)
- Set extensionality for AxisSet

**Assumptions**:
- Both quadrupole and octupole fit QFD-predicted axisymmetric forms
- Both amplitudes positive (A₂ > 0, A₃ > 0)
- Extracted axes are equal (observational constraint)

**Status**: ✅ PROVEN (0 sorries, 0 axioms)

**Physical Significance**: Directly formalizes the "Axis of Evil" claim.
Answers the reviewer question: "Could quadrupole and octupole be independently
axisymmetric but point in different directions?" → **NO**. If both fit
axisymmetric forms with A > 0, their axes are **constrained** to coincide.

**Mathematical Proof Strategy**:
1. Apply bridge theorems: both have AxisSet = {n, -n}
2. If AxisSets equal, then {n₁, -n₁} = {n₂, -n₂}
3. Set equality implies n₁ = n₂ or n₁ = -n₂ (uniqueness lemma)

**Corollary**: "Smoking gun" version - finding a **single** direction that
maximizes both patterns proves they're coaxial.
-/

/-!
### Infrastructure: Monotone Transform Invariance ⭐ NEW

**Claim**: Argmax sets are invariant under strictly monotone transformations,
generalizing the affine transform lemma.

**Lean Theorem**:
- `QFD.Cosmology.AxisExtraction.AxisSet_monotone`:
  For any strictly monotone g : ℝ → ℝ, AxisSet(g ∘ f) = AxisSet(f)

**File**: `QFD/Cosmology/AxisExtraction.lean:143-167`

**Status**: ✅ PROVEN (0 sorries)

**Significance**: Infrastructure lemma that makes the axis extraction framework
more robust. Shows that any strictly increasing transformation (not just affine)
preserves which directions maximize a pattern. Generalizes `AxisSet_affine`.

**Use Case**: Useful for composing transformations (e.g., exp, log, polynomial)
while preserving axis extraction properties.
-/

/-! ## 8. Leptons: Anomalous Magnetic Moment and Neutrinos -/

/-!
### Claim L.1 (Geometric Anomalous Magnetic Moment)

**Book Reference**: Lepton chapter "Vortex Geometry and g-2"

**Lean Theorems**:
- `QFD.Lepton.GeometricAnomaly.g_factor_is_anomalous`: g ≠ 2
- `QFD.Lepton.GeometricAnomaly.anomalous_moment_positive`: a_e > 0
- `QFD.Lepton.GeometricAnomaly.anomaly_scales_with_skirt`: a ∝ skirt energy

**File**: `QFD/Lepton/GeometricAnomaly.lean:121-166`

**Dependencies**:
- Vortex rotational energy distribution
- "Skirt" energy outside core radius

**Status**: ✅ PROVEN (with geometric vortex model)

**Notes**: Phenomenological model; coefficients fitted to electron g-2 measurement.
-/

/-!
### Claim L.2 (Neutrino Electromagnetic Decoupling)

**Book Reference**: Neutrino chapter "Chirality and Neutrality"

**Lean Theorems**:
- `QFD.Neutrino.neutrino_has_zero_coupling`: ⟨F_EM | ν⟩ = 0
- `QFD.Neutrino_Chirality.chirality_bleaching_lock`: Chirality preserved

**Files**:
- `QFD/Neutrino.lean:80`
- `QFD/Neutrino_Chirality.lean:48`

**Dependencies**:
- Internal projection operator P_Internal = (1 + B)/2
- EM field F_EM commutes with B

**Status**: ✅ PROVEN (algebraic decoupling)
-/

/-!
### Claim L.3 (Neutrino Mass Scale from Bleaching)

**Book Reference**: Neutrino chapter "Mass Hierarchy"

**Lean Theorems**:
- `QFD.Neutrino_MassScale.neutrino_mass_hierarchy`: m_ν ≪ m_e when R_p ≪ λ_e
- `QFD.Neutrino_Bleaching.tendsto_energy_bleach_zero`: E → 0 as λ → ∞
- `QFD.Neutrino_Topology.tendsto_energy_bleach_zero_toy`: Toy model version

**Files**:
- `QFD/Neutrino_MassScale.lean:57`
- `QFD/Neutrino_Bleaching.lean:49`
- `QFD/Neutrino_Topology.lean:60`

**Status**: ✅ PROVEN (parametric mass suppression)

**Concern Category**: [SCALAR_DYNAMICS_TAU_VS_SPACETIME]
-/

/-!
### Claim L.4 (Neutrino Oscillation Unitarity)

**Book Reference**: Neutrino chapter "Oscillation Mechanism"

**Lean Theorems**:
- `QFD.Neutrino_Oscillation.sum_P_eq_one`: Σᵢ P(νᵢ) = 1
- `QFD.Neutrino_Oscillation.exists_oscillation`: Oscillation occurs

**File**: `QFD/Neutrino_Oscillation.lean:99-109`

**Status**: ✅ PROVEN (unitarity of quantum evolution)
-/

/-! ## 9. Soliton Analysis: Ricker Profiles and Quantization -/

/-!
### Claim S.1 (Ricker Wavelet Has Unique Minimum)

**Book Reference**: Soliton chapter "Ricker Profile Analysis"

**Lean Theorems**:
- `QFD.Soliton.RickerAnalysis.S_at_sqrt3`: S(√3) = -2exp(-3/2)
- `QFD.Soliton.RickerAnalysis.S_lower_bound`: S(R) ≥ -2exp(-3/2)
- `QFD.Soliton.RickerAnalysis.S_le_one`: S(R) ≤ 1
- `QFD.Soliton.RickerAnalysis.ricker_shape_bounded`: Bounded above and below

**File**: `QFD/Soliton/RickerAnalysis.lean:161-330`

**Dependencies**:
- Shape function: S(R) = (1 - R²/2)exp(-R²/2)

**Status**: ✅ PROVEN (exact analysis of Ricker minimum)
-/

/-!
### Claim S.2 (6D Gaussian Moments)

**Book Reference**: Soliton chapter "6D Integration"

**Lean Theorems**:
- `QFD.Soliton.GaussianMoments.ricker_moment`: ∫ R⁶ exp(-R²) dR = 40
- `QFD.Soliton.GaussianMoments.gaussian_moment_odd`: Odd moments vanish

**File**: `QFD/Soliton/GaussianMoments.lean:128-143`

**Status**: ✅ PROVEN (6D spherical integral)

**Notes**: The factor 40 in charge quantization comes from this integral.
-/

/-! ## 10. Classical Conservation and Bound States -/

/-!
### Claim CL.1 (Energy Conservation for Conservative Forces)

**Book Reference**: Classical mechanics foundation

**Lean Theorems**:
- `QFD.Classical.Conservation.energy_conservation`: dE/dt = 0
- `QFD.Classical.Conservation.turning_point_velocity`: v(r_turn) = 0

**File**: `QFD/Classical/Conservation.lean:49-89`

**Status**: ✅ PROVEN (standard mechanics)
-/

/-!
### Claim CL.2 (Bound State Orbital Confinement)

**Book Reference**: Nuclear/Gravity chapters "Bound State Criteria"

**Lean Theorems**:
- `QFD.Classical.Conservation.gravity_bound_state`: E < 0 ⟹ r ≤ r_max
- `QFD.Classical.Conservation.nuclear_confinement`: Similar for nuclear potential
- `QFD.Classical.Conservation.nuclear_binding_energy_exact`: |V(0)| formula

**File**: `QFD/Classical/Conservation.lean:135-231`

**Status**: ✅ PROVEN (classical orbital mechanics)
-/

/-! ## 11. Schema Constraints and Dimensional Analysis -/

/-!
### Claim SC.1 (Grand Unified Parameter Space is Nonempty)

**Book Reference**: Schema appendix "Parameter Consistency"

**Lean Theorems**:
- `QFD.Schema.Constraints.valid_parameters_exist`
- `QFD.Schema.Constraints.parameter_space_bounded`
- `QFD.Schema.Constraints.constraints_satisfiable`

**File**: `QFD/Schema/Constraints.lean:136-151`

**Status**: ✅ PROVEN (constructive existence proof)

**Notes**: Proves that physical parameter bounds (e.g., κ > 0, v₀ > 0) are
mutually consistent.
-/

/-! ## 12. Stability Criterion and Solver Verification -/

/-!
### Claim ST.1 (Vacuum Stability from Quartic Potential)

**Book Reference**: Stability chapter "L6c Vacuum"

**Lean Theorems**:
- `QFD.StabilityCriterion.exists_global_min`: Global minimum exists
- `QFD.StabilityCriterion.V_coercive_atTop`: V → ∞ as |ψ| → ∞
- `QFD.StabilityCriterion.V_bounded_below`: V ≥ V_min

**File**: `QFD/StabilityCriterion.lean:391-494`

**Status**: ✅ PROVEN (coercivity + continuity ⟹ minimum)
-/

/-!
### Claim ST.2 (Numerical Solver Soundness)

**Book Reference**: Schema appendix "Solver Verification"

**Lean Theorems**:
- `QFD.StabilityCriterion.my_solver_correct`: Solver implements spec

**File**: `QFD/StabilityCriterion.lean:711`

**Status**: ✅ PROVEN (schema soundness check)

**Notes**: This theorem verifies that the Python solver's mathematical model
matches the Lean specification. It does NOT verify the numerical accuracy
of floating-point arithmetic.
-/

/-! ## 13. Bivector Classification and Topology -/

/-!
### Claim BC.1 (Bivector Squares Determine Topology)

**Book Reference**: Bivector chapter "Rotor vs Boost Distinction"

**Lean Theorems**:
- `QFD.BivectorClasses_Complete.simple_bivector_square_classes`:
  (u ∧ v)² = (u·u)(v·v) - (u·v)²
- `QFD.BivectorClasses_Complete.spatial_bivectors_are_rotors`: (eᵢ ∧ eⱼ)² < 0
- `QFD.BivectorClasses_Complete.space_momentum_bivectors_are_boosts`:
  (eᵢ ∧ pⱼ)² > 0
- `QFD.BivectorClasses_Complete.qfd_internal_rotor_is_rotor`: (e₄ ∧ e₅)² < 0

**File**: `QFD/BivectorClasses_Complete.lean:78-274`

**Status**: ✅ PROVEN (bivector algebra)

**Concern Category**: [PHASE_CENTRALIZER]
-/

/-! ## 14. Blueprints and Future Work -/

/-!
### Blueprint Claims (Not Yet Fully Proven)

The following theorems are marked as blueprints (trivial proofs or placeholders):

1. **Hill Vortex Topology** (`QFD/Electron/HillVortex.lean`):
   - `stream_function_continuous_at_boundary` ✅
   - `quantization_limit` ✅
   - `charge_universality` ✅

2. **Nuclear Force Unification** (`QFD/Nuclear/TimeCliff.lean`):
   - `bound_state_existence_blueprint`: Placeholder for full QM derivation
   - `force_unification_blueprint`: Placeholder for EM-nuclear unification

3. **Axis Alignment** (`QFD/Electron/AxisAlignment.lean:69`):
   - `axis_alignment_check`: Geometric condition, not dynamical proof

**Status**: Blueprints marked explicitly; core theorems complete.
-/

end QFD.ProofLedger

/-! ## Usage Examples

### For Reviewers

To verify a book claim, Ctrl+F for the claim number:
- "A.2.2" → energy_is_positive_definite
- "Z.4.A" → emergent_signature_is_minkowski
- "C.1" → unique_vortex_charge

### For AI Instances

Read this file first to understand the proof graph. Then navigate to specific
theorem files using the file paths provided.

### For Grep Search

Find theorems by concern category:
```bash
rg "\[ADJOINT_POSITIVITY\]" QFD/ProofLedger.lean
rg "\[PHASE_CENTRALIZER\]" QFD/ProofLedger.lean
```

Find theorems by book section:
```bash
rg "Appendix A" QFD/ProofLedger.lean -A 20
rg "Claim Z.4.A" QFD/ProofLedger.lean -A 30
```
-/