import PhysicsLogicConsumer.CondensedMatter.DensityVariational import PhysicsLogicConsumer.CondensedMatter.SpatialScreening import PhysicsLogic.Framework.GappedBandHallQuantization import PhysicsLogic.Framework.DensityFunctional import PhysicsLogic.Framework.CanonicalGibbsNormalization import PhysicsLogic.Framework.TopologicalTransverseResponse import PhysicsLogic.Framework.ParityResolvedFractionalJosephsonResponse import PhysicsLogic.Framework.TransverseMeissnerScreening import PhysicsLogic.Framework.OneParameterLocalizationScaling import PhysicsLogic.Philosophy.Symmetry import Mathlib.LinearAlgebra.Matrix.Kronecker import Mathlib.Analysis.Calculus.Deriv.Pow import Mathlib.Analysis.Matrix.Hermitian import Mathlib.Analysis.Real.Pi.Bounds /-! Independent tests of Haldane 1988 pp. 2016-2017 and TKNN 1982 pp. 406-408. The actual corner masses and continuum dispersions test the selected local spectral inputs, not a proof of the global Bloch spectrum. Spectral-flow and Kubo identifications remain distinct. Nonlinear control curves test only what the zero-field response contract entails, not a finite-field material. -/ set_option autoImplicit false set_option backward.isDefEq.respectTransparency false namespace PhysicsLogicConsumer.CondensedMatter open PhysicsLogic.Framework structure HoneycombParameters where nearestHopping : ℝ secondHopping : ℝ phase : ℝ staggered : ℝ noncomputable def HoneycombParameters.chiralShift (p : HoneycombParameters) : ℝ := 3 * Real.sqrt 3 * p.secondHopping * Real.sin p.phase noncomputable def HoneycombParameters.positiveMass (p : HoneycombParameters) : ℝ := p.staggered - p.chiralShift noncomputable def HoneycombParameters.negativeMass (p : HoneycombParameters) : ℝ := p.staggered + p.chiralShift noncomputable def massSign (mass : ℝ) : ℤ := if 0 < mass then 1 else if mass < 0 then -1 else 0 def MassSignIndexAt (p : HoneycombParameters) (index : ℤ) : Prop := 2 * index = massSign p.negativeMass - massSign p.positiveMass noncomputable def diracEnergy (mass momentum : ℝ) : ℝ := Real.sqrt (momentum ^ 2 + mass ^ 2) def GappedValleysAt (p : HoneycombParameters) : Prop := ∀ momentum, 0 < diracEnergy p.positiveMass momentum ∧ 0 < diracEnergy p.negativeMass momentum theorem nonzero_mass_gives_positive_dirac_energy (mass : ℝ) (nonzero : mass ≠ 0) (momentum : ℝ) : 0 < diracEnergy mass momentum := by apply Real.sqrt_pos.2 exact add_pos_of_nonneg_of_pos (sq_nonneg momentum) (sq_pos_of_ne_zero nonzero) noncomputable def positiveChirality : HoneycombParameters := ⟨1, 1 / (3 * Real.sqrt 3), Real.pi / 2, 0⟩ noncomputable def negativeChirality : HoneycombParameters := { positiveChirality with phase := -(Real.pi / 2) } noncomputable def trivialInsulator : HoneycombParameters := { positiveChirality with staggered := 2 } theorem source_corner_mass_values : positiveChirality.positiveMass = -1 ∧ positiveChirality.negativeMass = 1 ∧ negativeChirality.positiveMass = 1 ∧ negativeChirality.negativeMass = -1 ∧ trivialInsulator.positiveMass = 1 ∧ trivialInsulator.negativeMass = 3 := by have root : Real.sqrt 3 ≠ 0 := ne_of_gt (Real.sqrt_pos.2 (by norm_num)) have shift : 3 * Real.sqrt 3 * (1 / (3 * Real.sqrt 3)) = (1 : ℝ) := by field_simp have positiveShift : positiveChirality.chiralShift = 1 := by dsimp [HoneycombParameters.chiralShift, positiveChirality] rw [Real.sin_pi_div_two, mul_one] exact shift have negativeShift : negativeChirality.chiralShift = -1 := by dsimp [HoneycombParameters.chiralShift, negativeChirality, positiveChirality] rw [Real.sin_neg, Real.sin_pi_div_two, mul_neg, mul_one, shift] have trivialShift : trivialInsulator.chiralShift = 1 := positiveShift simp only [HoneycombParameters.positiveMass, HoneycombParameters.negativeMass, positiveShift, negativeShift, trivialShift] norm_num [positiveChirality, negativeChirality, trivialInsulator] theorem source_nonoverlap_parameter_restriction : |positiveChirality.secondHopping / positiveChirality.nearestHopping| < (1 / 3 : ℝ) := by have square : Real.sqrt 3 ^ 2 = 3 := Real.sq_sqrt (by norm_num) have nonnegative := Real.sqrt_nonneg (3 : ℝ) have root : 1 < Real.sqrt 3 := by nlinarith have denominator : 0 < 3 * Real.sqrt 3 := by linarith dsimp [positiveChirality] rw [div_one, abs_of_pos (div_pos (by norm_num) denominator)] exact (div_lt_iff₀ denominator).2 (by nlinarith) theorem local_gap_does_not_select_anomalous_index : (GappedValleysAt positiveChirality ∧ MassSignIndexAt positiveChirality 1) ∧ (GappedValleysAt negativeChirality ∧ MassSignIndexAt negativeChirality (-1)) ∧ (GappedValleysAt trivialInsulator ∧ MassSignIndexAt trivialInsulator 0) := by obtain ⟨plus, minus, reversePlus, reverseMinus, trivialPlus, trivialMinus⟩ := source_corner_mass_values have gap (p : HoneycombParameters) (hp : p.positiveMass ≠ 0) (hm : p.negativeMass ≠ 0) : GappedValleysAt p := fun momentum => ⟨nonzero_mass_gives_positive_dirac_energy _ hp momentum, nonzero_mass_gives_positive_dirac_energy _ hm momentum⟩ refine ⟨⟨gap _ (by rw [plus]; norm_num) (by rw [minus]; norm_num), ?_⟩, ⟨gap _ (by rw [reversePlus]; norm_num) (by rw [reverseMinus]; norm_num), ?_⟩, ⟨gap _ (by rw [trivialPlus]; norm_num) (by rw [trivialMinus]; norm_num), ?_⟩⟩ all_goals norm_num [MassSignIndexAt, plus, minus, reversePlus, reverseMinus, trivialPlus, trivialMinus, massSign] theorem reversed_chiralities_have_identical_cone_spectra (momentum : ℝ) : diracEnergy positiveChirality.positiveMass momentum = diracEnergy negativeChirality.positiveMass momentum ∧ diracEnergy positiveChirality.negativeMass momentum = diracEnergy negativeChirality.negativeMass momentum := by obtain ⟨plus, minus, reversePlus, reverseMinus, _, _⟩ := source_corner_mass_values simp [plus, minus, reversePlus, reverseMinus, diracEnergy] def numberDensityDifference (index : ℤ) (field : ℝ) : ℝ := (index : ℝ) * 2 * field def chargeDensityDifference (index : ℤ) (field : ℝ) : ℝ := 2 * numberDensityDifference index field theorem spectral_flow_and_streda_fix_signed_response (index : ℤ) (coefficient : ℝ) (streda : DifferentialHallResponse.At (chargeDensityDifference index) coefficient) : coefficient = (index : ℝ) * 4 ∧ DifferentialHallResponse.IntegerNormalizedAt (chargeDensityDifference index) index 4 := by have density : HasDerivAt (numberDensityDifference index) ((index : ℝ) * 2 / 1) 0 := by simpa [numberDensityDifference] using (hasDerivAt_id (0 : ℝ)).const_mul ((index : ℝ) * 2) have result := DifferentialHallResponse.signed_density_and_streda_determine_hall_response (numberDensityDifference index) (chargeDensityDifference index) 2 1 coefficient index (by norm_num) (by norm_num) density rfl streda norm_num [DifferentialHallResponse.conductanceQuantum] at result exact result theorem signed_density_derivative (index : ℤ) : DifferentialHallResponse.At (chargeDensityDifference index) ((index : ℝ) * 4) := by have density := (hasDerivAt_id (0 : ℝ)).const_mul ((index : ℝ) * 2) unfold DifferentialHallResponse.At convert density.const_mul 2 using 1 ring /-- The source spectral-flow law in units e = 2, h = 1, with the signs read from the masses. -/ noncomputable def valleyNumberDensity (p : HoneycombParameters) (field : ℝ) : ℝ := ((massSign p.negativeMass - massSign p.positiveMass : ℤ) : ℝ) * field noncomputable def valleyChargeDensity (p : HoneycombParameters) (field : ℝ) : ℝ := 2 * valleyNumberDensity p field theorem mass_sign_spectral_flow_realizes_differential_response (p : HoneycombParameters) (index : ℤ) (massRule : MassSignIndexAt p index) : DifferentialHallResponse.IntegerNormalizedAt (valleyChargeDensity p) index 4 := by have conversion : valleyChargeDensity p = chargeDensityDifference index := by funext field dsimp [valleyChargeDensity, valleyNumberDensity, chargeDensityDifference, numberDensityDifference] rw [← massRule] push_cast ring rw [conversion] exact (spectral_flow_and_streda_fix_signed_response index _ (signed_density_derivative index)).2 theorem opposite_chiralities_have_opposite_differential_hall_response : (GappedValleysAt positiveChirality ∧ GappedValleysAt negativeChirality) ∧ DifferentialHallResponse.IntegerNormalizedAt (valleyChargeDensity positiveChirality) 1 4 ∧ DifferentialHallResponse.IntegerNormalizedAt (valleyChargeDensity negativeChirality) (-1) 4 ∧ ¬DifferentialHallResponse.At (valleyChargeDensity negativeChirality) 4 := by have phases := local_gap_does_not_select_anomalous_index have negative := mass_sign_spectral_flow_realizes_differential_response negativeChirality (-1) phases.2.1.2 refine ⟨⟨phases.1.1, phases.2.1.1⟩, mass_sign_spectral_flow_realizes_differential_response positiveChirality 1 phases.1.2, negative, ?_⟩ intro positive have contradiction := positive.unique negative.2 norm_num at contradiction theorem gapped_trivial_phase_has_zero_differential_response : GappedValleysAt trivialInsulator ∧ DifferentialHallResponse.IntegerNormalizedAt (valleyChargeDensity trivialInsulator) 0 4 := ⟨local_gap_does_not_select_anomalous_index.2.2.1, mass_sign_spectral_flow_realizes_differential_response trivialInsulator 0 local_gap_does_not_select_anomalous_index.2.2.2⟩ def nonlinearCurrent (field : ℝ) : ℝ := 4 * field + field ^ 3 theorem zero_field_quantization_does_not_fix_finite_field_measurement : DifferentialHallResponse.IntegerNormalizedAt nonlinearCurrent 1 4 ∧ ¬(nonlinearCurrent 1 / 1 = 4) := by have higherOrder : DifferentialHallResponse.FirstOrderRemainderAt (fun field : ℝ => field ^ 3) := ⟨by norm_num, by simpa using (hasDerivAt_id (0 : ℝ)).pow 3⟩ have response := (DifferentialHallResponse.first_order_remainder_preserves_response 4 _ higherOrder).2 exact ⟨DifferentialHallResponse.normalized_coefficient_gives_integer_response nonlinearCurrent 4 4 1 response (by norm_num) (by norm_num), by norm_num [nonlinearCurrent]⟩ /-- p = 3, q = 1, r = 1 selects s = 1, t = 0; in Landau level N = 2 the total is one. -/ theorem filled_landau_levels_change_total_response : (1 : ℤ) = 1 * 1 + 0 * 3 ∧ 2 * Int.natAbs (1 : ℤ) < 3 ∧ (0 + (2 : ℤ) - 1) ≠ 0 ∧ DifferentialHallResponse.IntegerNormalizedAt nonlinearCurrent (0 + 2 - 1) 4 := by refine ⟨by norm_num, by norm_num, by norm_num, ?_⟩ exact zero_field_quantization_does_not_fix_finite_field_measurement.1 namespace SpectralProbe abbrev Hilbert := EuclideanSpace Complex (Fin 2) def hamiltonianMatrix : Matrix (Fin 2) (Fin 2) Complex := !![0, 0; 0, 2] def velocityOneMatrix : Matrix (Fin 2) (Fin 2) Complex := !![0, 1; 1, 0] def velocityTwoMatrix : Matrix (Fin 2) (Fin 2) Complex := !![0, -Complex.I; Complex.I, 0] noncomputable def spectral : SpectralHallResponse.SpectralData Hilbert (Fin 2) where hamiltonian := hamiltonianMatrix.toEuclideanLin.toContinuousLinearMap.toPMap ⊤ operatorOne := velocityOneMatrix.toEuclideanLin.comp (Submodule.subtype ⊤) operatorTwo := velocityTwoMatrix.toEuclideanLin.comp (Submodule.subtype ⊤) eigenstate := fun index => ⟨EuclideanSpace.basisFun (Fin 2) Complex index, by simp⟩ energy := fun index => if index = 0 then 0 else 2 occupied := fun index => index = 0 theorem matrices_are_hermitian : hamiltonianMatrix.IsHermitian ∧ velocityOneMatrix.IsHermitian ∧ velocityTwoMatrix.IsHermitian := by refine ⟨?_, ?_, ?_⟩ all_goals ext left right fin_cases left <;> fin_cases right <;> simp [hamiltonianMatrix, velocityOneMatrix, velocityTwoMatrix, Matrix.conjTranspose_apply] theorem actual_eigenbasis : spectral.EigenSystemAt := by refine ⟨?_, (EuclideanSpace.basisFun (Fin 2) Complex).orthonormal, ?_, ?_⟩ · change (hamiltonianMatrix.toEuclideanLin.toContinuousLinearMap.toPMap ⊤).adjoint = _ rw [ContinuousLinearMap.toPMap_adjoint_eq_adjoint_toPMap_of_dense _ (by simp)] apply congrArg (fun operator : Hilbert →L[Complex] Hilbert => operator.toPMap ⊤) apply ContinuousLinearMap.isSelfAdjoint_iff_isSymmetric.mpr exact Matrix.isHermitian_iff_isSymmetric.mp matrices_are_hermitian.1 · change Dense (Submodule.span Complex (Set.range (EuclideanSpace.basisFun (Fin 2) Complex).toBasis) : Set Hilbert) rw [(EuclideanSpace.basisFun (Fin 2) Complex).toBasis.span_eq] simp · intro index change hamiltonianMatrix.toEuclideanLin (EuclideanSpace.basisFun (Fin 2) Complex index) = (((if index = 0 then 0 else 2) : Real) : Complex) • EuclideanSpace.basisFun (Fin 2) Complex index fin_cases index <;> ext coordinate <;> fin_cases coordinate <;> norm_num [Matrix.toLpLin_apply, hamiltonianMatrix, Matrix.mulVec, dotProduct, Fin.sum_univ_two, EuclideanSpace.basisFun_apply] theorem hermitian_velocity_operators : spectral.HermitianOnDomainAt spectral.operatorOne ∧ spectral.HermitianOnDomainAt spectral.operatorTwo := by constructor · intro left right exact (Matrix.isHermitian_iff_isSymmetric.mp matrices_are_hermitian.2.1) (left : Hilbert) (right : Hilbert) · intro left right exact (Matrix.isHermitian_iff_isSymmetric.mp matrices_are_hermitian.2.2) (left : Hilbert) (right : Hilbert) theorem occupied_empty_gap : spectral.OccupiedGapAt 1 1 := by refine ⟨by norm_num, ?_, ?_⟩ all_goals intro index; fin_cases index <;> norm_num [spectral] theorem spectral_response_is_nonvacuous : spectral.NonvacuousSpectralResponseAt 1 1 := by classical letI : Finite spectral.TransitionIndex := by unfold SpectralHallResponse.SpectralData.TransitionIndex infer_instance exact ⟨actual_eigenbasis, occupied_empty_gap, ⟨0, rfl⟩, ⟨1, by change (1 : Fin 2) ≠ 0; decide⟩, hermitian_velocity_operators.1, hermitian_velocity_operators.2, Summable.of_finite⟩ def transition : spectral.TransitionIndex := ⟨⟨0, rfl⟩, ⟨1, by change (1 : Fin 2) ≠ 0; decide⟩⟩ theorem only_transition (index : spectral.TransitionIndex) : index = transition := by rcases index with ⟨⟨left, occupied⟩, ⟨right, empty⟩⟩ have leftValue : left = 0 := occupied have rightNonzero : right ≠ 0 := empty have rightValue : right = 1 := by fin_cases right <;> simp_all subst left subst right rfl theorem matrix_element_of_matrix (matrix : Matrix (Fin 2) (Fin 2) Complex) (left right : Fin 2) : spectral.matrixElement (matrix.toEuclideanLin.comp (Submodule.subtype ⊤)) left right = matrix left right := by change inner Complex (EuclideanSpace.basisFun (Fin 2) Complex left) (matrix.toEuclideanLin (EuclideanSpace.basisFun (Fin 2) Complex right)) = matrix left right rw [EuclideanSpace.basisFun_inner] fin_cases right <;> simp [Matrix.toLpLin_apply, EuclideanSpace.basisFun_apply] theorem actual_spectral_sum : spectral.spectralSum = Complex.I / 2 := by have single : spectral.spectralSum = spectral.transitionTerm transition := tsum_eq_single transition (fun index different => False.elim (different (only_transition index))) rw [single] change spectral.numerator 0 1 / (((0 - 2) ^ 2 : Real) : Complex) = Complex.I / 2 have first := matrix_element_of_matrix velocityOneMatrix have second := matrix_element_of_matrix velocityTwoMatrix change ∀ left right, spectral.matrixElement spectral.operatorOne left right = velocityOneMatrix left right at first change ∀ left right, spectral.matrixElement spectral.operatorTwo left right = velocityTwoMatrix left right at second simp only [SpectralHallResponse.SpectralData.numerator, first, second] norm_num [velocityOneMatrix, velocityTwoMatrix] ring theorem actual_response : spectral.response 1 = (-1 / 2 : Complex) := by rw [SpectralHallResponse.SpectralData.response, actual_spectral_sum] norm_num [← mul_div_assoc, Complex.I_mul_I] /-- H + x V1 + y V2 is a local parameter probe, not a periodic Bloch or twist-torus model. -/ noncomputable def localHamiltonian (x y : Real) : spectral.hamiltonian.domain →ₗ[Complex] Hilbert := spectral.hamiltonian.toFun + (x : Complex) • spectral.operatorOne + (y : Complex) • spectral.operatorTwo theorem actual_hamiltonian_derivatives : spectral.HamiltonianDerivativeOperatorsAt localHamiltonian := by refine ⟨by simp [localHamiltonian], fun vector => ⟨?_, ?_⟩⟩ · change HasDerivAt (fun x : Real => spectral.hamiltonian vector + x • spectral.operatorOne vector + (0 : Real) • spectral.operatorTwo vector) (spectral.operatorOne vector) 0 simpa using ((hasDerivAt_id (0 : Real)).smul_const (spectral.operatorOne vector)).const_add (spectral.hamiltonian vector) · change HasDerivAt (fun y : Real => spectral.hamiltonian vector + (0 : Real) • spectral.operatorOne vector + y • spectral.operatorTwo vector) (spectral.operatorTwo vector) 0 simpa using ((hasDerivAt_id (0 : Real)).smul_const (spectral.operatorTwo vector)).const_add (spectral.hamiltonian vector) /-- In units e = hbar = area = 1, the conductance quantum is 1/(2 pi). -/ theorem gap_and_local_kubo_data_do_not_imply_integer_response : spectral.NonvacuousSpectralResponseAt 1 1 ∧ spectral.HamiltonianDerivativeOperatorsAt localHamiltonian ∧ ¬∃ index : Int, spectral.response 1 = (index : Complex) / (2 * Real.pi) := by refine ⟨spectral_response_is_nonvacuous, actual_hamiltonian_derivatives, ?_⟩ rintro ⟨index, integerResponse⟩ rw [actual_response] at integerResponse have piNonzero : (Real.pi : Complex) ≠ 0 := by exact_mod_cast Real.pi_ne_zero have value : (index : Real) = -Real.pi := by have denominator : (2 : Complex) * Real.pi ≠ 0 := mul_ne_zero (by norm_num) piNonzero have product := (div_eq_iff denominator).mp integerResponse.symm have complexValue : (index : Complex) = -(Real.pi : Complex) := by rw [product] ring exact_mod_cast complexValue have lower : (-4 : Int) < index := by exact_mod_cast (show (-4 : Real) < index by rw [value]; linarith [Real.pi_lt_four]) have upper : index < (-3 : Int) := by exact_mod_cast (show (index : Real) < -3 by rw [value]; linarith [Real.pi_gt_three]) omega theorem identical_spectral_gap_does_not_fix_hall_sign : spectral.NonvacuousSpectralResponseAt 1 1 ∧ spectral.swapOperators.NonvacuousSpectralResponseAt 1 1 ∧ spectral.response 1 = (-1 / 2 : Complex) ∧ spectral.swapOperators.response 1 = (1 / 2 : Complex) := by refine ⟨spectral_response_is_nonvacuous, (spectral.swapping_operators_preserves_nonvacuity 1 1).mpr spectral_response_is_nonvacuous, actual_response, ?_⟩ rw [spectral.swapping_operators_reverses_response, actual_response] norm_num noncomputable def changeEigenstatePhase (data : SpectralHallResponse.SpectralData Hilbert (Fin 2)) : SpectralHallResponse.SpectralData Hilbert (Fin 2) := { data with eigenstate := fun index => -data.eigenstate index } theorem phase_change_is_a_unitary_identification (data : SpectralHallResponse.SpectralData Hilbert (Fin 2)) : data.UnitarySpectralIdentificationAt (changeEigenstatePhase data) (LinearIsometryEquiv.neg Complex) := by refine ⟨rfl, rfl, fun _ => rfl, ?_, ?_⟩ · intro index change data.operatorOne (-data.eigenstate index) = -(data.operatorOne (data.eigenstate index)) exact map_neg _ _ · intro index change data.operatorTwo (-data.eigenstate index) = -(data.operatorTwo (data.eigenstate index)) exact map_neg _ _ theorem rephasing_the_eigenvectors_preserves_the_response : (changeEigenstatePhase spectral).state 0 ≠ spectral.state 0 ∧ (changeEigenstatePhase spectral).response 1 = spectral.response 1 := by refine ⟨?_, spectral.unitary_identification_preserves_response _ _ (phase_change_is_a_unitary_identification spectral) 1⟩ change -EuclideanSpace.basisFun (Fin 2) Complex 0 ≠ EuclideanSpace.basisFun (Fin 2) Complex 0 intro same have component := congrArg (fun vector : Hilbert => vector 0) same norm_num [EuclideanSpace.basisFun_apply] at component theorem spectral_response_is_real : (spectral.response 1).im = 0 := spectral.summable_hermitian_response_is_real hermitian_velocity_operators.1 hermitian_velocity_operators.2 spectral_response_is_nonvacuous.2.2.2.2.2.2 1 theorem actual_torus_average_uses_the_reversed_bracket : TwistCurvatureResponse.torusAverage (fun _ _ => Complex.I * ((1 ^ 2 / 1 : Real) : Complex) * (Complex.I / (2 * Real.pi))) = ((1 ^ 2 / (2 * Real.pi) : Real) : Complex) * TwistCurvatureResponse.normalizedCurvature (fun _ _ => Complex.I / (2 * Real.pi)) := by exact TwistCurvatureResponse.averaging_response_gives_oriented_curvature (fun _ _ => Complex.I / (2 * Real.pi)) 1 (2 * Real.pi) 1 (by positivity) (by field_simp) end SpectralProbe /-! A separate finite Fock representation of the solvable two-site wire. The orbital locations, electron operators, and parity are constructed here; no paper module or production countermodel supplies the witness. -/ namespace MajoranaWire noncomputable section open FermionicModeAlgebra abbrev FockBasis := Fin 2 × Fin 2 def electron : Operator (Fin 2) := !![0, 1; 0, 0] def occupationParity : Operator (Fin 2) := !![1, 0; 0, -1] def orbitals : Family (Fin 2) FockBasis where annihilation := ![ Matrix.kronecker electron (1 : Operator (Fin 2)), Matrix.kronecker occupationParity electron] def firstSitePair : MajoranaPair FockBasis := MajoranaPair.ofFermion (orbitals.annihilation 0) def secondSitePair : MajoranaPair FockBasis := MajoranaPair.ofFermion (orbitals.annihilation 1) def endPair : MajoranaPair FockBasis where first := firstSitePair.first second := secondSitePair.second def bulkHamiltonian : Operator FockBasis := (2 * Complex.I) • (firstSitePair.second * secondSitePair.first) def endData (coupling : Real) : FiniteMajoranaParity.Data FockBasis where pair := endPair splitting := coupling def wireHamiltonian (coupling : Real) : Operator FockBasis := bulkHamiltonian + (endData coupling).hamiltonian def totalParity : Operator FockBasis := Matrix.kronecker occupationParity occupationParity def hopping : Operator FockBasis := star (orbitals.annihilation 0) * orbitals.annihilation 1 + star (orbitals.annihilation 1) * orbitals.annihilation 0 set_option maxHeartbeats 1600000 in theorem constructed_electron_operators_obey_car : orbitals.CARAt := by intro first second fin_cases first <;> fin_cases second <;> constructor <;> ext ⟨rowA, rowB⟩ ⟨columnA, columnB⟩ <;> fin_cases rowA <;> fin_cases rowB <;> fin_cases columnA <;> fin_cases columnB <;> norm_num [anticommutator, orbitals, electron, occupationParity, Matrix.kronecker, Matrix.mul_apply, Fintype.sum_prod_type, Fin.sum_univ_two, Matrix.star_apply, Matrix.vecMul, dotProduct] set_option maxHeartbeats 1600000 in theorem selected_end_operators_obey_canonical_majorana_relations : endPair.CanonicalAt := by refine ⟨?_, ?_, ?_, ?_, ?_⟩ <;> ext ⟨rowA, rowB⟩ ⟨columnA, columnB⟩ <;> fin_cases rowA <;> fin_cases rowB <;> fin_cases columnA <;> fin_cases columnB <;> norm_num [SelfConjugateAt, anticommutator, endPair, firstSitePair, secondSitePair, MajoranaPair.ofFermion, orbitals, electron, occupationParity, Matrix.kronecker, Matrix.mul_apply, Fintype.sum_prod_type, Fin.sum_univ_two, Matrix.star_apply, Matrix.vecMul, dotProduct] theorem independently_selected_ends_are_nonvacuous : endPair.NonvacuousCanonicalMajoranaPairAt := endPair.canonical_pair_is_nonvacuous selected_end_operators_obey_canonical_majorana_relations theorem actual_end_coupling_has_two_nonempty_parity_sectors (coupling : Real) : (endData coupling).NonvacuousEffectiveParityPairAt := (endData coupling).canonical_majorana_pair_realizes_nonvacuous_effective_parity independently_selected_ends_are_nonvacuous set_option maxHeartbeats 1600000 in theorem solvable_wire_has_exact_uncoupled_end_zero_modes : FermionicModeAlgebra.commutator bulkHamiltonian endPair.first = 0 ∧ FermionicModeAlgebra.commutator bulkHamiltonian endPair.second = 0 := by constructor <;> ext ⟨rowA, rowB⟩ ⟨columnA, columnB⟩ <;> fin_cases rowA <;> fin_cases rowB <;> fin_cases columnA <;> fin_cases columnB <;> norm_num [FermionicModeAlgebra.commutator, bulkHamiltonian, endPair, firstSitePair, secondSitePair, MajoranaPair.ofFermion, orbitals, electron, occupationParity, Matrix.kronecker, Matrix.mul_apply, Fintype.sum_prod_type, Fin.sum_univ_two, Matrix.star_apply, Matrix.vecMul, dotProduct, mul_assoc] <;> ring theorem finite_end_coupling_has_nonzero_exact_operator_residuals : FermionicModeAlgebra.commutator (wireHamiltonian (3 / 5)) endPair.first = (-Complex.I * (3 / 5 : Complex)) • endPair.second ∧ FermionicModeAlgebra.commutator (wireHamiltonian (3 / 5)) endPair.second = (Complex.I * (3 / 5 : Complex)) • endPair.first := by have endResiduals := endPair.effective_pair_coupling_has_actual_majorana_residuals selected_end_operators_obey_canonical_majorana_relations (3 / 5) have distribute (a b c : Operator FockBasis) : FermionicModeAlgebra.commutator (a + b) c = FermionicModeAlgebra.commutator a c + FermionicModeAlgebra.commutator b c := by simp only [FermionicModeAlgebra.commutator] noncomm_ring constructor · rw [wireHamiltonian, distribute, solvable_wire_has_exact_uncoupled_end_zero_modes.1, zero_add] simpa [endData, FiniteMajoranaParity.Data.hamiltonian] using endResiduals.1 · rw [wireHamiltonian, distribute, solvable_wire_has_exact_uncoupled_end_zero_modes.2, zero_add] simpa [endData, FiniteMajoranaParity.Data.hamiltonian] using endResiduals.2 theorem finite_coupling_is_parity_preserving_but_not_an_exact_zero_mode : (endData (3 / 5)).ParityPreservingAt (endData (3 / 5)).hamiltonian ∧ FermionicModeAlgebra.commutator (endData (3 / 5)).hamiltonian endPair.first ≠ 0 ∧ FermionicModeAlgebra.commutator (endData (3 / 5)).hamiltonian endPair.second ≠ 0 := by have actual := actual_end_coupling_has_two_nonempty_parity_sectors (3 / 5) exact ⟨actual.2.2.2.2.1, nonzero_effective_splitting_prevents_exact_majorana_zero_modes endPair independently_selected_ends_are_nonvacuous (3 / 5) (by norm_num)⟩ theorem parity_preserving_perturbations_have_zero_opposite_sector_blocks (perturbation : Operator FockBasis) (preserved : (endData (3 / 5)).ParityPreservingAt perturbation) : (endData (3 / 5)).positiveProjector * perturbation * (endData (3 / 5)).negativeProjector = 0 ∧ (endData (3 / 5)).negativeProjector * perturbation * (endData (3 / 5)).positiveProjector = 0 := (endData (3 / 5)).parity_preserving_perturbation_has_no_cross_sector_block (actual_end_coupling_has_two_nonempty_parity_sectors (3 / 5)) perturbation preserved set_option maxHeartbeats 1600000 in theorem electron_hopping_preserves_total_but_not_first_orbital_parity : hopping * totalParity = totalParity * hopping ∧ hopping * firstSitePair.parity ≠ firstSitePair.parity * hopping ∧ hopping (0, 1) (1, 0) = 1 := by refine ⟨?_, ?_, ?_⟩ · ext ⟨rowA, rowB⟩ ⟨columnA, columnB⟩ fin_cases rowA <;> fin_cases rowB <;> fin_cases columnA <;> fin_cases columnB <;> norm_num [hopping, totalParity, orbitals, electron, occupationParity, Matrix.kronecker, Matrix.mul_apply, Fintype.sum_prod_type, Fin.sum_univ_two, Matrix.star_apply, Matrix.vecMul, dotProduct] · intro commute have entry := congrArg (fun matrix : Operator FockBasis => matrix (0, 1) (1, 0)) commute norm_num [hopping, firstSitePair, MajoranaPair.parity, MajoranaPair.ofFermion, orbitals, electron, occupationParity, Matrix.kronecker, Matrix.mul_apply, Fintype.sum_prod_type, Fin.sum_univ_two, Matrix.star_apply, Matrix.vecMul, dotProduct] at entry · norm_num [hopping, orbitals, electron, occupationParity, Matrix.kronecker, Matrix.mul_apply, Fintype.sum_prod_type, Fin.sum_univ_two, Matrix.star_apply, Matrix.vecMul, dotProduct] def mixedSpinCoefficients : Coefficients (Fin 2) := Coefficients.majorana ![(3 / 5 : Complex), 4 * Complex.I / 5] theorem independent_complex_spin_combination_is_an_actual_normalized_majorana : orbitals.NonvacuousLinearMajoranaAt mixedSpinCoefficients ∧ orbitals.linearOperator mixedSpinCoefficients * orbitals.linearOperator mixedSpinCoefficients = (1 : Operator FockBasis) := by refine ⟨orbitals.conjugate_nonzero_weights_realize_an_actual_majorana constructed_electron_operators_obey_car _ (Coefficients.majorana_coefficients_are_self_conjugate _) ⟨0, by norm_num [mixedSpinCoefficients, Coefficients.majorana]⟩, ?_⟩ have square := orbitals.actual_majorana_square_has_its_own_normalization constructed_electron_operators_obey_car ![(3 / 5 : Complex), 4 * Complex.I / 5] norm_num [Fin.sum_univ_two, Complex.normSq_apply] at square exact square theorem an_imaginary_rephase_changes_literal_self_conjugacy_but_can_be_undone : let mode := orbitals.linearOperator mixedSpinCoefficients star ((-Complex.I) • mode) = -((-Complex.I) • mode) ∧ ¬SelfConjugateAt ((-Complex.I) • mode) ∧ Complex.I • ((-Complex.I) • mode) = mode := by have actual := independent_complex_spin_combination_is_an_actual_normalized_majorana.1 exact imaginary_rephasing_is_not_literal_self_conjugacy _ actual.2.2.2.2 actual.2.2.2.1 def totalElectronNumber : Operator FockBasis := star (orbitals.annihilation 0) * orbitals.annihilation 0 + star (orbitals.annihilation 1) * orbitals.annihilation 1 set_option maxHeartbeats 1600000 in theorem superconducting_pairing_preserves_parity_not_electron_number : bulkHamiltonian * totalParity = totalParity * bulkHamiltonian ∧ FermionicModeAlgebra.commutator bulkHamiltonian totalElectronNumber ≠ 0 := by constructor · ext ⟨rowA, rowB⟩ ⟨columnA, columnB⟩ fin_cases rowA <;> fin_cases rowB <;> fin_cases columnA <;> fin_cases columnB <;> norm_num [bulkHamiltonian, totalParity, firstSitePair, secondSitePair, MajoranaPair.ofFermion, orbitals, electron, occupationParity, Matrix.kronecker, Matrix.mul_apply, Fintype.sum_prod_type, Fin.sum_univ_two, Matrix.star_apply, Matrix.vecMul, dotProduct, mul_assoc] · intro conserved have entry := congrArg (fun matrix : Operator FockBasis => matrix (0, 0) (1, 1)) conserved norm_num [FermionicModeAlgebra.commutator, bulkHamiltonian, totalElectronNumber, firstSitePair, secondSitePair, MajoranaPair.ofFermion, orbitals, electron, occupationParity, Matrix.kronecker, Matrix.mul_apply, Fintype.sum_prod_type, Fin.sum_univ_two, Matrix.star_apply, Matrix.vecMul, dotProduct, mul_assoc] at entry /-- Nonunit kets; both have squared norm two. No probability law uses them unnormalized. -/ def evenKet : FockBasis -> Complex := fun state => if state.1 = state.2 then 1 else 0 def oddKet : FockBasis -> Complex := fun state => if state.1 = state.2 then 0 else 1 theorem two_actual_parity_kets_are_nonzero_and_orthogonal : (∑ state, Complex.normSq (evenKet state)) = 2 ∧ (∑ state, Complex.normSq (oddKet state)) = 2 ∧ (∑ state, star (evenKet state) * oddKet state) = 0 := by simp only [Fintype.sum_prod_type, Fin.sum_univ_two] norm_num [evenKet, oddKet] set_option maxHeartbeats 1600000 in theorem actual_parity_kets_have_the_finite_wire_energy_splitting : Matrix.mulVec totalParity evenKet = evenKet ∧ Matrix.mulVec totalParity oddKet = -oddKet ∧ Matrix.mulVec (wireHamiltonian (3 / 5)) evenKet = (-23 / 10 : Complex) • evenKet ∧ Matrix.mulVec (wireHamiltonian (3 / 5)) oddKet = (-17 / 10 : Complex) • oddKet := by refine ⟨?_, ?_, ?_, ?_⟩ <;> funext ⟨rowA, rowB⟩ <;> fin_cases rowA <;> fin_cases rowB <;> norm_num [Matrix.mulVec, dotProduct, evenKet, oddKet, totalParity, wireHamiltonian, bulkHamiltonian, endData, FiniteMajoranaParity.Data.hamiltonian, MajoranaPair.effectiveHamiltonian, endPair, firstSitePair, secondSitePair, MajoranaPair.ofFermion, orbitals, electron, occupationParity, Matrix.kronecker, Matrix.mul_apply, Fintype.sum_prod_type, Fin.sum_univ_two, Matrix.star_apply, Matrix.vecMul, mul_assoc] <;> ring_nf <;> norm_num def unconjugatedSpinCoefficients : Coefficients (Fin 2) where annihilation := ![(3 / 5 : Complex), 4 * Complex.I / 5] creation := ![(3 / 5 : Complex), 4 * Complex.I / 5] theorem unit_coefficient_weight_does_not_replace_actual_conjugation : (∑ orbital, Complex.normSq (unconjugatedSpinCoefficients.annihilation orbital)) = 1 ∧ orbitals.linearOperator unconjugatedSpinCoefficients ≠ 0 ∧ ¬SelfConjugateAt (orbitals.linearOperator unconjugatedSpinCoefficients) := by refine ⟨by norm_num [unconjugatedSpinCoefficients, Fin.sum_univ_two, Complex.normSq_apply], orbitals.nonzero_canonical_coefficient_gives_nonzero_operator constructed_electron_operators_obey_car _ ⟨0, by norm_num [unconjugatedSpinCoefficients]⟩, ?_⟩ intro selfConjugate have coefficients := (orbitals.actual_self_conjugacy_iff_conjugate_coefficients constructed_electron_operators_obey_car unconjugatedSpinCoefficients).mp selfConjugate 1 have imaginary := congrArg Complex.im coefficients norm_num [unconjugatedSpinCoefficients] at imaginary end end MajoranaWire namespace ThermalFermionReuse noncomputable section /-! An independent three-mode fermion system tests Kohn-Sham 1965 (3.3), (3.9), and the fixed-number distinction in (3.10)-(3.12). The grand Gibbs energy is log(2) times the actual particle number. Its mean is one, not its three available modes; conditioning on exactly one particle gives the three-state canonical sector. The equal one-body densities do not identify number fluctuations or entropy. Only public canonical APIs are imported; this is not a continuum density-functional or Sommerfeld-limit model. -/ open PhysicsLogic.Framework MeasureTheory open scoped BigOperators abbrev Configuration := Bool × Bool × Bool def occupied (bit : Bool) : Real := if bit then 1 else 0 def number (configuration : Configuration) : Real := occupied configuration.1 + occupied configuration.2.1 + occupied configuration.2.2 def siteOccupation (site : Fin 3) (configuration : Configuration) : Real := ![occupied configuration.1, occupied configuration.2.1, occupied configuration.2.2] site def grand : FiniteCanonicalData Configuration where beta := 1 energy := fun configuration => Real.log 2 * number configuration def fixedOne : FiniteCanonicalData (Fin 3) where beta := 1 energy := fun _ => Real.log 2 def oneParticleConfiguration (site : Fin 3) : Configuration := ![(true, false, false), (false, true, false), (false, false, true)] site def oneModeWeight (bit : Bool) : Real := if bit then 1 / 2 else 1 theorem the_three_fermionic_mode_weights_are_computed_from_actual_energy (configuration : Configuration) : grand.boltzmannWeight configuration = oneModeWeight configuration.1 * oneModeWeight configuration.2.1 * oneModeWeight configuration.2.2 := by have exponential : Real.exp (-Real.log 2) = 1 / 2 := by rw [Real.exp_neg, Real.exp_log (by norm_num)] norm_num change Real.exp (-1 * (Real.log 2 * number configuration)) = _ have exponent : -1 * (Real.log 2 * number configuration) = (-Real.log 2 * occupied configuration.1 + -Real.log 2 * occupied configuration.2.1) + -Real.log 2 * occupied configuration.2.2 := by unfold number ring rw [exponent, Real.exp_add, Real.exp_add] rcases configuration with ⟨first, second, third⟩ cases first <;> cases second <;> cases third <;> norm_num [occupied, oneModeWeight, exponential] theorem the_eight_state_grand_partition_is_twenty_seven_eighths : grand.partition = 27 / 8 := by unfold FiniteCanonicalData.partition simp_rw [the_three_fermionic_mode_weights_are_computed_from_actual_energy] norm_num [Fintype.sum_prod_type, Fintype.sum_bool, oneModeWeight] theorem the_grand_probabilities_are_the_actual_normalized_product_weights (configuration : Configuration) : grand.probability configuration = (8 / 27) * oneModeWeight configuration.1 * oneModeWeight configuration.2.1 * oneModeWeight configuration.2.2 := by rw [FiniteCanonicalData.probability, the_eight_state_grand_partition_is_twenty_seven_eighths, the_three_fermionic_mode_weights_are_computed_from_actual_energy] ring theorem both_ensembles_use_the_public_nonvacuous_gibbs_normalization : grand.NonvacuousFiniteCanonicalWeightsAt ∧ fixedOne.NonvacuousFiniteCanonicalWeightsAt := ⟨grand.computed_finite_weights_realize_nonvacuous_canonical_normalization, fixedOne.computed_finite_weights_realize_nonvacuous_canonical_normalization⟩ theorem the_fixed_one_particle_probabilities_are_one_third (site : Fin 3) : fixedOne.probability site = 1 / 3 := by norm_num [FiniteCanonicalData.probability, FiniteCanonicalData.partition, FiniteCanonicalData.boltzmannWeight, fixedOne, Real.exp_neg, Real.exp_log, Fin.sum_univ_succ] theorem the_grand_number_sum_is_one : (∑ configuration, grand.probability configuration * number configuration) = 1 := by simp_rw [the_grand_probabilities_are_the_actual_normalized_product_weights] norm_num [number, occupied, oneModeWeight, Fintype.sum_prod_type, Fintype.sum_bool] theorem the_public_mean_api_returns_one_grand_mean_particle : (∫ configuration, number configuration ∂grand.law) = 1 := by rw [grand.finite_canonical_mean_is_the_actual_weighted_state_sum] exact the_grand_number_sum_is_one theorem the_public_mean_api_returns_nonzero_grand_number_variance : (∫ configuration, (number configuration - 1) ^ 2 ∂grand.law) = 2 / 3 := by rw [grand.finite_canonical_mean_is_the_actual_weighted_state_sum] simp_rw [the_grand_probabilities_are_the_actual_normalized_product_weights] norm_num [number, occupied, oneModeWeight, Fintype.sum_prod_type, Fintype.sum_bool] theorem every_fixed_one_configuration_has_exactly_one_particle (site : Fin 3) : number (oneParticleConfiguration site) = 1 := by fin_cases site <;> norm_num [number, occupied, oneParticleConfiguration] theorem the_public_mean_api_returns_zero_fixed_sector_number_variance : (∫ site, (number (oneParticleConfiguration site) - 1) ^ 2 ∂fixedOne.law) = 0 := by rw [fixedOne.finite_canonical_mean_is_the_actual_weighted_state_sum] simp_rw [every_fixed_one_configuration_has_exactly_one_particle] simp theorem the_public_mean_api_returns_the_same_one_body_density_in_both_ensembles (site : Fin 3) : (∫ configuration, siteOccupation site configuration ∂grand.law) = 1 / 3 ∧ (∫ location, siteOccupation site (oneParticleConfiguration location) ∂fixedOne.law) = 1 / 3 := by constructor · rw [grand.finite_canonical_mean_is_the_actual_weighted_state_sum] simp_rw [the_grand_probabilities_are_the_actual_normalized_product_weights] fin_cases site <;> norm_num [siteOccupation, occupied, oneModeWeight, Fintype.sum_prod_type, Fintype.sum_bool] · rw [fixedOne.finite_canonical_mean_is_the_actual_weighted_state_sum] simp_rw [the_fixed_one_particle_probabilities_are_one_third] fin_cases site <;> norm_num [siteOccupation, occupied, oneParticleConfiguration, Fin.sum_univ_succ] def shannonEntropy {State : Type} [Fintype State] [Nonempty State] (ensemble : FiniteCanonicalData State) : Real := -∑ state, ensemble.probability state * Real.log (ensemble.probability state) theorem the_public_log_weight_api_computes_the_entropy_from_actual_energy {State : Type} [Fintype State] [Nonempty State] (ensemble : FiniteCanonicalData State) : shannonEntropy ensemble = ensemble.beta * (∑ state, ensemble.probability state * ensemble.energy state) + Real.log ensemble.partition := by unfold shannonEntropy simp_rw [ensemble.finite_canonical_log_probability_is_energy_and_partition] calc _ = ∑ state, (ensemble.beta * (ensemble.probability state * ensemble.energy state) + Real.log ensemble.partition * ensemble.probability state) := by rw [← Finset.sum_neg_distrib] apply Finset.sum_congr rfl intro state _ ring _ = _ := by rw [Finset.sum_add_distrib, ← Finset.mul_sum, ← Finset.mul_sum, ensemble.finite_canonical_probabilities_sum_to_one, mul_one] theorem the_grand_entropy_is_three_log_three_minus_two_log_two : shannonEntropy grand = 3 * Real.log 3 - 2 * Real.log 2 := by rw [the_public_log_weight_api_computes_the_entropy_from_actual_energy, the_eight_state_grand_partition_is_twenty_seven_eighths] have energySum : (∑ configuration, grand.probability configuration * grand.energy configuration) = Real.log 2 := by change (∑ configuration, grand.probability configuration * (Real.log 2 * number configuration)) = _ calc _ = Real.log 2 * ∑ configuration, grand.probability configuration * number configuration := by rw [Finset.mul_sum] apply Finset.sum_congr rfl intro configuration _ ring _ = _ := by rw [the_grand_number_sum_is_one, mul_one] rw [energySum, Real.log_div (by norm_num) (by norm_num), show (27 : Real) = 3 ^ 3 by norm_num, show (8 : Real) = 2 ^ 3 by norm_num, Real.log_pow, Real.log_pow] dsimp [grand] ring theorem the_fixed_sector_entropy_is_log_three : shannonEntropy fixedOne = Real.log 3 := by unfold shannonEntropy simp_rw [the_fixed_one_particle_probabilities_are_one_third] norm_num [Fin.sum_univ_succ, Real.log_div] ring theorem the_same_one_body_density_does_not_determine_the_grand_or_canonical_entropy : ((∀ site, (∫ configuration, siteOccupation site configuration ∂grand.law) = ∫ location, siteOccupation site (oneParticleConfiguration location) ∂fixedOne.law) ∧ (∫ configuration, number configuration ∂grand.law) = 1) ∧ shannonEntropy grand ≠ shannonEntropy fixedOne := by refine ⟨⟨fun site => (the_public_mean_api_returns_the_same_one_body_density_in_both_ensembles site).1.trans (the_public_mean_api_returns_the_same_one_body_density_in_both_ensembles site).2.symm, the_public_mean_api_returns_one_grand_mean_particle⟩, ?_⟩ rw [the_grand_entropy_is_three_log_three_minus_two_log_two, the_fixed_sector_entropy_is_log_three] have strict := Real.strictMonoOn_log (show (2 : Real) ∈ Set.Ioi 0 by norm_num) (show (3 : Real) ∈ Set.Ioi 0 by norm_num) (by norm_num : (2 : Real) < 3) linarith def oneParticleProbability : Real := ∑ configuration, if number configuration = 1 then grand.probability configuration else 0 theorem the_actual_grand_probability_of_the_one_particle_sector_is_four_ninths : oneParticleProbability = 4 / 9 := by unfold oneParticleProbability simp_rw [the_grand_probabilities_are_the_actual_normalized_product_weights] norm_num [number, occupied, oneModeWeight, Fintype.sum_prod_type, Fintype.sum_bool] theorem conditioning_the_grand_ensemble_on_one_particle_recovers_the_fixed_sector (site : Fin 3) : grand.probability (oneParticleConfiguration site) / oneParticleProbability = fixedOne.probability site := by rw [the_actual_grand_probability_of_the_one_particle_sector_is_four_ninths, the_grand_probabilities_are_the_actual_normalized_product_weights, the_fixed_one_particle_probabilities_are_one_third] fin_cases site <;> norm_num [oneParticleConfiguration, oneModeWeight] theorem actual_mean_particle_calibration_does_not_make_the_grand_number_sharp : (grand.NonvacuousFiniteCanonicalWeightsAt ∧ (∫ configuration, number configuration ∂grand.law) = 1) ∧ ¬(∫ configuration, (number configuration - 1) ^ 2 ∂grand.law) = 0 := by refine ⟨⟨both_ensembles_use_the_public_nonvacuous_gibbs_normalization.1, the_public_mean_api_returns_one_grand_mean_particle⟩, ?_⟩ rw [the_public_mean_api_returns_nonzero_grand_number_variance] norm_num end end ThermalFermionReuse namespace SelectedStateReuse open PhysicsLogic.Philosophy.Symmetry /-! A homogeneous Landau free-energy diagnostic with its own scales. Its minima are variational states of this model, not a microscopic equilibrium construction or a finite-volume quantum symmetry-breaking claim. -/ def freeEnergy (temperature orderParameter : Real) : Real := orderParameter ^ 4 + (temperature ^ 2 - 9) * orderParameter ^ 2 def symmetry : SelectedPhysicalSymmetryContext Unit Real Real Unit Real Unit where lawInvariantUnder := fun temperature _ => ∀ orderParameter, freeEnergy temperature (-orderParameter) = freeEnergy temperature orderParameter stateTransformsTo := fun _ initial final => final = -initial observableValue := fun _ state => state physicallyAdmissible := fun _ _ => True selectedStateForLaw := fun temperature state _ => 0 < temperature ∧ ∀ other, freeEnergy temperature state ≤ freeEnergy temperature other physicalTransformation := fun _ => True theorem reflection_preserves_the_actual_free_energy (temperature : Real) : symmetry.lawInvariantUnder temperature () := by intro orderParameter dsimp [symmetry, freeEnergy] ring theorem reflection_is_functional_and_preserves_the_selected_minima (temperature : Real) : symmetry.SelectedActionAt temperature () () := by constructor · intro initial first second firstImage secondImage exact firstImage.trans secondImage.symm · intro state selected refine ⟨-state, ⟨trivial, selected.2.1, ?_⟩, rfl⟩ intro other rw [reflection_preserves_the_actual_free_energy temperature state] exact selected.2.2 other theorem low_temperature_energy_is_a_shifted_nonnegative_square (state : Real) : freeEnergy 1 state = (state ^ 2 - 4) ^ 2 - 16 := by unfold freeEnergy ring theorem the_low_temperature_selects_exactly_two_minima (state : Real) : symmetry.SelectedStateAt 1 state () ↔ state = 2 ∨ state = -2 := by constructor · intro selected have bound := selected.2.2 2 rw [low_temperature_energy_is_a_shifted_nonnegative_square, low_temperature_energy_is_a_shifted_nonnegative_square] at bound have square : (state ^ 2 - 4) ^ 2 = 0 := by nlinarith [sq_nonneg (state ^ 2 - 4)] have radius := sq_eq_zero_iff.mp square rcases le_total state 0 with nonpositive | nonnegative · right; nlinarith · left; nlinarith · rintro (rfl | rfl) all_goals refine ⟨trivial, by norm_num, ?_⟩ intro other rw [low_temperature_energy_is_a_shifted_nonnegative_square, low_temperature_energy_is_a_shifted_nonnegative_square] nlinarith [sq_nonneg (other ^ 2 - 4)] theorem the_high_temperature_selects_exactly_the_symmetric_minimum (state : Real) : symmetry.SelectedStateAt 4 state () ↔ state = 0 := by constructor · intro selected have bound := selected.2.2 0 dsimp [freeEnergy] at bound have square : state ^ 2 = 0 := by nlinarith [sq_nonneg state, sq_nonneg (state ^ 2)] exact sq_eq_zero_iff.mp square · rintro rfl refine ⟨trivial, by norm_num, ?_⟩ intro other dsimp [freeEnergy] nlinarith [sq_nonneg other, sq_nonneg (other ^ 2)] theorem the_low_temperature_has_actual_selected_movement : symmetry.LawSymmetricSelectedMovedStateAt 1 () 2 () := by refine ⟨reflection_preserves_the_actual_free_energy 1, (the_low_temperature_selects_exactly_two_minima 2).mpr (Or.inl rfl), -2, (the_low_temperature_selects_exactly_two_minima (-2)).mpr (Or.inr rfl), rfl, ?_⟩ norm_num theorem the_library_recovers_breaking_from_the_selected_minima : symmetry.SpontaneouslyBrokenAt 1 () 2 () := by have moved := selected_movement_and_physical_action_establish_spontaneous_breaking symmetry 1 () 2 () the_low_temperature_has_actual_selected_movement trivial (reflection_is_functional_and_preserves_the_selected_minima 1) exact moved_selected_breaking_implies_noninvariant_selected_breaking symmetry 1 () 2 () moved theorem the_library_exhibits_the_other_selected_minimum : ∃ partner, symmetry.SelectedStateAt 1 partner () ∧ partner = -2 ∧ partner ≠ 2 := by have retained := spontaneous_breaking_requires_selected_state_and_preserved_family symmetry 1 () 2 () the_library_recovers_breaking_from_the_selected_minima obtain ⟨partner, selected, acts, distinct⟩ := retained.2.2 exact ⟨partner, selected, acts, distinct⟩ theorem the_excited_high_temperature_configuration_retains_raw_state_asymmetry : symmetry.LawSymmetricMovedStateAt 4 () 1 () ∧ symmetry.SelectedActionAt 4 () () ∧ ¬symmetry.StateInvariant () 1 ∧ symmetry.SelectedStateAt 4 0 () ∧ symmetry.StateInvariant () 0 := by refine ⟨⟨reflection_preserves_the_actual_free_energy 4, trivial, -1, trivial, rfl, ?_⟩, reflection_is_functional_and_preserves_the_selected_minima 4, ?_, (the_high_temperature_selects_exactly_the_symmetric_minimum 0).mpr rfl, ?_⟩ · norm_num · norm_num [SymmetryActionContext.StateInvariant, symmetry] · norm_num [SymmetryActionContext.StateInvariant, symmetry] theorem the_library_rejects_the_excited_high_temperature_configuration : ¬symmetry.SpontaneouslyBrokenAt 4 () 1 () := by intro alleged have selected := (spontaneous_breaking_requires_selected_state_and_preserved_family symmetry 4 () 1 () alleged).1 have lower := selected.2 0 norm_num [freeEnergy] at lower theorem one_temperatures_selected_state_is_not_anothers : symmetry.SelectedStateAt 1 2 () ∧ ¬symmetry.SelectedStateAt 4 2 () := by refine ⟨the_library_recovers_breaking_from_the_selected_minima.2.1, ?_⟩ intro selected have zero := (the_high_temperature_selects_exactly_the_symmetric_minimum 2).mp selected norm_num at zero end SelectedStateReuse namespace ScaleFlowReuse /- These independently constructed conductance curves test conditional scale-flow logic. Neither curve is claimed to be the microscopic Anderson model. -/ noncomputable def vanishing : PositiveLogScaleTrajectory := ⟨fun logWidth => Real.log 2 - 3 * logWidth⟩ noncomputable def unresolvedFloor (floor : Real) : PositiveLogScaleTrajectory := ⟨fun logWidth => Real.log (2 * Real.exp (-3 * logWidth) + floor)⟩ noncomputable def floorBeta (floor value : Real) : Real := -3 + 3 * floor / value theorem the_vanishing_curve_has_the_actual_positive_conductance (t : Real) : vanishing.observable t = 2 * Real.exp (-3 * t) := by change Real.exp (Real.log 2 - 3 * t) = _ rw [sub_eq_add_neg, Real.exp_add, Real.exp_log (by norm_num : (0 : Real) < 2)] congr 2 ring theorem the_vanishing_curve_has_the_actual_constant_beta (t : Real) : vanishing.HasBetaAt (fun _ => -3) t := by change HasDerivAt (fun s : Real => Real.log 2 - 3 * s) (-3) t convert (hasDerivAt_const t (Real.log 2)).sub ((hasDerivAt_id t).const_mul 3) using 1 norm_num theorem the_library_derives_the_zero_large_scale_limit : Filter.Tendsto vanishing.observable Filter.atTop (nhds 0) := vanishing.future_continuation_and_a_negative_monotone_beta_force_zero (fun _ => -3) 0 (fun t _ => the_vanishing_curve_has_the_actual_constant_beta t) (fun _ _ _ _ _ => le_refl _) (fun _ _ => by norm_num) theorem the_library_excludes_a_persistent_conducting_response : ¬vanishing.PersistentPositiveResponse := vanishing.a_zero_limit_excludes_a_persistent_positive_response the_library_derives_the_zero_large_scale_limit theorem the_floor_curve_has_the_actual_positive_conductance (floor : Real) (positive : 0 < floor) (t : Real) : (unresolvedFloor floor).observable t = 2 * Real.exp (-3 * t) + floor := by apply Real.exp_log positivity theorem the_floor_curve_has_its_actual_autonomous_beta (floor : Real) (positive : 0 < floor) (t : Real) : (unresolvedFloor floor).HasBetaAt (floorBeta floor) t := by have denominator : 0 < 2 * Real.exp (-3 * t) + floor := by positivity have exponential := ((hasDerivAt_id t).const_mul (-3)).exp have conductance := (exponential.const_mul 2).add_const floor have logarithm := conductance.log (ne_of_gt denominator) change HasDerivAt (fun s : Real => Real.log (2 * Real.exp (-3 * s) + floor)) (floorBeta floor ((unresolvedFloor floor).observable t)) t rw [the_floor_curve_has_the_actual_positive_conductance floor positive t] convert logarithm using 1 dsimp [floorBeta] field_simp [ne_of_gt denominator] ring theorem the_library_certifies_the_floor_curve_at_every_scale (floor : Real) (positive : 0 < floor) (t : Real) : (unresolvedFloor floor).NonvacuousBetaAt (floorBeta floor) t := (unresolvedFloor floor).an_actual_beta_derivative_is_nonvacuous (floorBeta floor) t (the_floor_curve_has_its_actual_autonomous_beta floor positive t) theorem the_floor_curve_has_negative_beta_at_every_finite_scale (floor : Real) (positive : 0 < floor) (t : Real) : floorBeta floor ((unresolvedFloor floor).observable t) < 0 := by rw [the_floor_curve_has_the_actual_positive_conductance floor positive t] have denominator : 0 < 2 * Real.exp (-3 * t) + floor := by positivity have ratio : 3 * floor / (2 * Real.exp (-3 * t) + floor) < 3 := by apply (div_lt_iff₀ denominator).mpr nlinarith [Real.exp_pos (-3 * t)] dsimp [floorBeta] linarith theorem the_library_rejects_an_independently_reassigned_floor_beta (floor : Real) (positive : 0 < floor) (t slope : Real) (derivative : HasDerivAt (unresolvedFloor floor).logObservable slope t) : floorBeta floor ((unresolvedFloor floor).observable t) = slope := (unresolvedFloor floor).the_beta_value_is_fixed_by_the_actual_derivative (floorBeta floor) t slope (the_floor_curve_has_its_actual_autonomous_beta floor positive t) derivative theorem the_floor_curve_has_a_positive_large_scale_limit (floor : Real) (positive : 0 < floor) : Filter.Tendsto (unresolvedFloor floor).observable Filter.atTop (nhds floor) := by have decays : Filter.Tendsto (fun t : Real => Real.exp (-3 * t)) Filter.atTop (nhds 0) := Real.tendsto_exp_atBot.comp ((Filter.tendsto_const_mul_atBot_of_neg (by norm_num : (-3 : Real) < 0)).mpr Filter.tendsto_id) have shifted := (decays.const_mul 2).add_const floor have curve : (unresolvedFloor floor).observable = fun t => 2 * Real.exp (-3 * t) + floor := funext (the_floor_curve_has_the_actual_positive_conductance floor positive) rw [curve] simpa only [mul_zero, zero_add] using shifted theorem an_arbitrarily_small_unresolved_floor_changes_the_large_scale_conclusion (floor : Real) (positive : 0 < floor) : (∀ t, |(unresolvedFloor floor).observable t - vanishing.observable t| = floor) /\ (∀ t, (unresolvedFloor floor).NonvacuousBetaAt (floorBeta floor) t) /\ (∀ t, floorBeta floor ((unresolvedFloor floor).observable t) < 0) /\ (unresolvedFloor floor).PersistentPositiveResponse /\ ¬Filter.Tendsto (unresolvedFloor floor).observable Filter.atTop (nhds 0) := by refine ⟨?_, the_library_certifies_the_floor_curve_at_every_scale floor positive, the_floor_curve_has_negative_beta_at_every_finite_scale floor positive, ?_, ?_⟩ · intro t rw [the_floor_curve_has_the_actual_positive_conductance floor positive t, the_vanishing_curve_has_the_actual_positive_conductance] simpa using abs_of_pos positive · refine ⟨floor, positive, Filter.Eventually.of_forall fun t => ?_⟩ rw [the_floor_curve_has_the_actual_positive_conductance floor positive t] nlinarith [Real.exp_pos (-3 * t)] · intro vanishes have equal := tendsto_nhds_unique (the_floor_curve_has_a_positive_large_scale_limit floor positive) vanishes exact (ne_of_gt positive) equal theorem the_unresolved_floor_introduces_a_positive_beta_zero (floor : Real) (positive : 0 < floor) : floorBeta floor floor = 0 := by dsimp [floorBeta] field_simp [ne_of_gt positive] ring end ScaleFlowReuse end PhysicsLogicConsumer.CondensedMatter