diff --git a/Hqiv/Geometry/ComptonNuclearTorus.lean b/Hqiv/Geometry/ComptonNuclearTorus.lean new file mode 100644 index 0000000..b430911 --- /dev/null +++ b/Hqiv/Geometry/ComptonNuclearTorus.lean @@ -0,0 +1,63 @@ +import Hqiv.Geometry.NuclearTorusPerturbation +import Hqiv.Physics.ComptonIRWindow + +/-! +# Compton/IR-window sourced nuclear torus angles + +Build `NuclearTorusConfig` directly from Compton phase coordinates `x_i = ω_i t_i`, +with per-channel constraints `0 < t_i < t_IR,i`, and prove each linking angle lies in +the HQIV phase window `0 < x_i < θ` (`θ = horizonQuarterPeriod`). +-/ + +namespace Hqiv.Geometry + +open Hqiv + +/-- Per-channel Compton-sourced angle `x = ω_compton(E,ħ) * t`. -/ +noncomputable def comptonLinkedAngle (E ħ t : ℝ) (hħ : 0 < ħ) : ℝ := + Hqiv.Physics.comptonPhaseX E ħ t (ne_of_gt hħ) + +/-- Build a `NuclearTorusConfig` from three Compton-sourced phase angles. -/ +noncomputable def comptonLinkedNuclearTorusConfig + (E : Fin 3 → ℝ) (ħ : ℝ) (hħ : 0 < ħ) (t : Fin 3 → ℝ) : NuclearTorusConfig where + linkingAngles := fun i => comptonLinkedAngle (E i) ħ (t i) hħ + +theorem comptonLinkedAngle_mem_window + (E ħ t : ℝ) (hE : 0 < E) (hħ : 0 < ħ) (ht : 0 < t) + (htIR : t < Hqiv.Physics.comptonTIR E ħ hE hħ) : + 0 < comptonLinkedAngle E ħ t hħ ∧ + comptonLinkedAngle E ħ t hħ < Hqiv.Physics.phaseTheta := by + unfold comptonLinkedAngle + simpa using Hqiv.Physics.compton_phase_window E ħ t hE hħ ht htIR + +theorem comptonLinkedNuclearTorusConfig_angle_mem_window + (E : Fin 3 → ℝ) (ħ : ℝ) (hħ : 0 < ħ) (t : Fin 3 → ℝ) + (hE : ∀ i : Fin 3, 0 < E i) + (ht : ∀ i : Fin 3, 0 < t i) + (htIR : ∀ i : Fin 3, t i < Hqiv.Physics.comptonTIR (E i) ħ (hE i) hħ) + (i : Fin 3) : + 0 < (comptonLinkedNuclearTorusConfig E ħ hħ t).linkingAngles i ∧ + (comptonLinkedNuclearTorusConfig E ħ hħ t).linkingAngles i < Hqiv.Physics.phaseTheta := by + simpa [comptonLinkedNuclearTorusConfig] using + comptonLinkedAngle_mem_window (E i) ħ (t i) (hE i) hħ (ht i) (htIR i) + +theorem comptonLinkedNuclearTorusConfig_angles_pos + (E : Fin 3 → ℝ) (ħ : ℝ) (hħ : 0 < ħ) (t : Fin 3 → ℝ) + (hE : ∀ i : Fin 3, 0 < E i) + (ht : ∀ i : Fin 3, 0 < t i) + (htIR : ∀ i : Fin 3, t i < Hqiv.Physics.comptonTIR (E i) ħ (hE i) hħ) : + ∀ i : Fin 3, 0 < (comptonLinkedNuclearTorusConfig E ħ hħ t).linkingAngles i := by + intro i + exact (comptonLinkedNuclearTorusConfig_angle_mem_window E ħ hħ t hE ht htIR i).1 + +theorem comptonLinkedNuclearTorusConfig_angles_lt_phaseTheta + (E : Fin 3 → ℝ) (ħ : ℝ) (hħ : 0 < ħ) (t : Fin 3 → ℝ) + (hE : ∀ i : Fin 3, 0 < E i) + (ht : ∀ i : Fin 3, 0 < t i) + (htIR : ∀ i : Fin 3, t i < Hqiv.Physics.comptonTIR (E i) ħ (hE i) hħ) : + ∀ i : Fin 3, (comptonLinkedNuclearTorusConfig E ħ hħ t).linkingAngles i < Hqiv.Physics.phaseTheta := by + intro i + exact (comptonLinkedNuclearTorusConfig_angle_mem_window E ħ hħ t hE ht htIR i).2 + +end Hqiv.Geometry + diff --git a/Hqiv/Physics/ComptonIRWindow.lean b/Hqiv/Physics/ComptonIRWindow.lean new file mode 100644 index 0000000..b6f67f5 --- /dev/null +++ b/Hqiv/Physics/ComptonIRWindow.lean @@ -0,0 +1,94 @@ +import Mathlib.Data.Real.Basic +import Mathlib.Algebra.Order.Field.Basic +import Mathlib.Tactic +import Hqiv.Physics.ComptonHorizonPhase +import Hqiv.Physics.GlobalDetuning + +/-! +# Compton phase IR window (`0 < x < θ`) + +This module isolates the phase-window statement: + +* `θ := horizonQuarterPeriod = π/2`, +* `x := ω * t`, +* `t_IR := θ / ω` (for `ω > 0`). + +Then `0 < t < t_IR` implies `0 < x < θ`. + +This is the derivation-first hook requested for chemistry/QC participation windows +without fixing geometric binding angles directly. +-/ + +namespace Hqiv.Physics + +noncomputable section + +/-- Phase cap `θ` used by the quarter-turn window. -/ +noncomputable def phaseTheta : ℝ := Hqiv.horizonQuarterPeriod + +/-- Phase variable `x = ω t`. -/ +noncomputable def phaseX (ω t : ℝ) : ℝ := ω * t + +/-- Frequency-implied IR time window `t_IR = θ / ω` (`ω > 0`). -/ +noncomputable def tIR (ω : ℝ) (_hω : 0 < ω) : ℝ := phaseTheta / ω + +theorem phaseTheta_eq_pi_div_two : phaseTheta = Real.pi / 2 := by + unfold phaseTheta + simpa using horizonQuarterPeriod_eq_pi_div_two + +theorem phaseTheta_pos : 0 < phaseTheta := by + rw [phaseTheta_eq_pi_div_two] + positivity + +theorem phase_window_of_time_window (ω t : ℝ) (hω : 0 < ω) (ht : 0 < t) (htIR : t < tIR ω hω) : + 0 < phaseX ω t ∧ phaseX ω t < phaseTheta := by + constructor + · unfold phaseX + exact mul_pos hω ht + · unfold phaseX tIR at * + have hmul' : t * ω < (phaseTheta / ω) * ω := mul_lt_mul_of_pos_right htIR hω + have hdiv : (phaseTheta / ω) * ω = phaseTheta := by + field_simp [ne_of_gt hω] + have hmul : ω * t < phaseTheta := by + nlinarith [hmul', hdiv] + simpa [mul_comm] using hmul + +/-- Compton-specialized phase variable `x = ω_compton * t`. -/ +noncomputable def comptonPhaseX (E ħ t : ℝ) (hħ : ħ ≠ 0) : ℝ := + phaseX (omegaCompton E ħ hħ) t + +/-- Compton-specialized IR cutoff `t_IR = θ / ω_compton`. -/ +noncomputable def comptonTIR (E ħ : ℝ) (hE : 0 < E) (hħ : 0 < ħ) : ℝ := + tIR (omegaCompton E ħ (ne_of_gt hħ)) (omegaCompton_pos E ħ hE hħ) + +theorem compton_phase_window (E ħ t : ℝ) (hE : 0 < E) (hħ : 0 < ħ) (ht : 0 < t) + (htIR : t < comptonTIR E ħ hE hħ) : + 0 < comptonPhaseX E ħ t (ne_of_gt hħ) ∧ + comptonPhaseX E ħ t (ne_of_gt hħ) < phaseTheta := by + simpa [comptonPhaseX, comptonTIR] using + phase_window_of_time_window (omegaCompton E ħ (ne_of_gt hħ)) t + (omegaCompton_pos E ħ hE hħ) ht htIR + +/-- A bounded participation coordinate from the phase window: `η = x/θ`. -/ +noncomputable def phaseParticipationEta (x : ℝ) : ℝ := x / phaseTheta + +theorem phaseParticipationEta_mem_unit (x : ℝ) (hx0 : 0 < x) (hxθ : x < phaseTheta) : + 0 < phaseParticipationEta x ∧ phaseParticipationEta x < 1 := by + have hθ : 0 < phaseTheta := phaseTheta_pos + constructor + · unfold phaseParticipationEta + exact div_pos hx0 hθ + · unfold phaseParticipationEta + exact (div_lt_one hθ).2 hxθ + +/-- Lapse-time variant: use `timeAngle φ t = φ t` as the phase proxy `x`. -/ +theorem phase_window_of_timeAngle (φ t : ℝ) (hφ : 0 < φ) (ht : 0 < t) (hcap : timeAngle φ t < phaseTheta) : + 0 < timeAngle φ t ∧ timeAngle φ t < phaseTheta := by + constructor + · simp [timeAngle] + exact mul_pos hφ ht + · exact hcap + +end +end Hqiv.Physics + diff --git a/Hqiv/Physics/DynamicBetaIsotope.lean b/Hqiv/Physics/DynamicBetaIsotope.lean new file mode 100644 index 0000000..9a04d9d --- /dev/null +++ b/Hqiv/Physics/DynamicBetaIsotope.lean @@ -0,0 +1,316 @@ +import Hqiv.Physics.DynamicNucleonPN + +/-! +# Dynamic isotope and β-channel readouts + +This module is the next layer over `DynamicNucleonPN`. + +It does **not** derive weak lifetimes from the strong/curvature overlap energy. +Instead it keeps the three ledgers separate: + +* p/n mass gap: from `DerivedNucleonMass`, preserved by shared outside-curvature binding. +* β overlap: from `NeutronBindingStabilityScaffold` via `betaMinusOverlapAtXi`. +* weak width: from `NuclearAndAtomicSpectra.beta_decay_rate` / `G_F_from_beta`. +* geometry / spin-statistics: valley-count + caustic-well trapping for bonded clusters. + +This is the right place to build isotope-ladder β bookkeeping before adding a +flavor-dependent weak/EM tipping correction to the nucleon mass itself. +-/ + +namespace Hqiv.Physics + +noncomputable section + +/-- A dynamic isotope environment: mass number, proton number, ladder witness, and p/n environment. -/ +structure DynamicIsotopeEnvironment (A Z : ℕ) where + ladder : IsotopeLadder A Z + nucleonEnv : NucleonEnvironment + +/-- Neutron count in an isotope bookkeeping state. -/ +def neutronCount (A Z : ℕ) : ℕ := A - Z + +/-- Isotope mass budget from dynamic p/n masses, before electron/rest-frame bookkeeping. -/ +noncomputable def isotopeNucleonMassBudget + {A Z : ℕ} (env : DynamicIsotopeEnvironment A Z) (c : ℝ := 1) : ℝ := + (Z : ℝ) * protonMassAtXi env.nucleonEnv c + + (neutronCount A Z : ℝ) * neutronMassAtXi env.nucleonEnv c + +/-- β− mass-gap slot: one neutron changes to one proton in the same environment. -/ +noncomputable def betaMinusMassGapAtXi (env : NucleonEnvironment) (c : ℝ := 1) : ℝ := + neutronMassAtXi env c - protonMassAtXi env c + +/-- β+ mass-gap slot: one proton changes to one neutron in the same environment. -/ +noncomputable def betaPlusMassGapAtXi (env : NucleonEnvironment) (c : ℝ := 1) : ℝ := + protonMassAtXi env c - neutronMassAtXi env c + +theorem betaMinusMassGapAtXi_eq_derivedDeltaM + (env : NucleonEnvironment) (c : ℝ) : + betaMinusMassGapAtXi env c = derivedDeltaM := by + unfold betaMinusMassGapAtXi + exact neutron_proton_gap_preserved_at_xi env c + +theorem betaPlusMassGapAtXi_eq_neg_derivedDeltaM + (env : NucleonEnvironment) (c : ℝ) : + betaPlusMassGapAtXi env c = -derivedDeltaM := by + unfold betaPlusMassGapAtXi + have h := neutron_proton_gap_preserved_at_xi env c + linarith + +/-- Strong/curvature overlap slot for β−, kept separate from weak width. -/ +noncomputable def betaMinusCurvatureOverlap + (env : NucleonEnvironment) : ℝ := + betaMinusOverlapForEnvironment env + +/-- β+ mirror overlap slot; this is structural, not a weak width. -/ +noncomputable def betaPlusCurvatureOverlap + (env : NucleonEnvironment) (c : ℝ := 1) : ℝ := + betaPlusOverlapForEnvironment env c + +/-- Residual β− energy after the curvature-overlap ledger. -/ +noncomputable def betaMinusResidualAtXi + (env : NucleonEnvironment) (c : ℝ := 1) : ℝ := + betaMinusMassGapAtXi env c - betaMinusCurvatureOverlap env + +/-- Residual β+ energy after the curvature-overlap ledger. -/ +noncomputable def betaPlusResidualAtXi + (env : NucleonEnvironment) (c : ℝ := 1) : ℝ := + betaPlusMassGapAtXi env c - betaPlusCurvatureOverlap env c + +/-- Kinematic β− endpoint Q after the lepton mass slot (not the overlap residual). -/ +noncomputable def betaMinusEndpointQAtXi + (env : NucleonEnvironment) (m_e : ℝ) (c : ℝ := 1) : ℝ := + betaMinusMassGapAtXi env c - m_e + +/-- Kinematic β+ endpoint Q after the lepton mass slot. -/ +noncomputable def betaPlusEndpointQAtXi + (env : NucleonEnvironment) (m_e : ℝ) (c : ℝ := 1) : ℝ := + betaPlusMassGapAtXi env c - m_e + +theorem betaMinusEndpointQAtXi_eq_derivedDeltaM_minus_m_e + (env : NucleonEnvironment) (m_e c : ℝ) : + betaMinusEndpointQAtXi env m_e c = derivedDeltaM - m_e := by + unfold betaMinusEndpointQAtXi + rw [betaMinusMassGapAtXi_eq_derivedDeltaM] + +/-! +## Curvature mass imprints and endpoint-$Q$ policies (generic ledger) + +The primary HQIV width readout uses the **nucleon-gap** endpoint from shared p/n readouts +(`betaMinusEndpointQAtXi`). A separate **spectroscopy / mass-table** layer closes each +isotope budget with its own reference imprint +`curvatureMassImprint = M_ref / M_derived`. Uniform imprints preserve $\Delta M$; +independent parent/daughter imprints move $Q_{\beta^-}$ to the mass-table slot. +The geometric-mean interior width well is the width-ledger companion (not the mass endpoint). +These are generic bookkeeping policies for endpoint $Q$ and width-well imprints; they carry +no claim about nuclear structure beyond the named mass-budget identities proved below. +-/ + +/-- Curvature mass imprint: reference mass over derived budget (spectroscopy ledger). -/ +noncomputable def curvatureMassImprint (M_ref M_der : ℝ) : ℝ := + M_ref / max M_der 1e-30 + +/-- Mass budget after applying a curvature imprint. -/ +noncomputable def imprintedMassBudget (M_der κ : ℝ) : ℝ := + κ * M_der + +theorem imprintedMassBudget_eq_ref + (M_der κ M_ref : ℝ) (hκ : curvatureMassImprint M_ref M_der = κ) + (hder : 1e-30 < M_der) : + imprintedMassBudget M_der κ = M_ref := by + unfold imprintedMassBudget + calc + κ * M_der = curvatureMassImprint M_ref M_der * M_der := by rw [hκ] + _ = M_ref := by + unfold curvatureMassImprint + have hmax : max M_der 1e-30 = M_der := max_eq_left (le_of_lt hder) + rw [hmax] + field_simp [ne_of_lt hder] + +theorem curvatureMassImprint_imprinted_closes_budget + (M_der M_ref : ℝ) (hder : 1e-30 < M_der) : + imprintedMassBudget M_der (curvatureMassImprint M_ref M_der) = M_ref := + imprintedMassBudget_eq_ref M_der (curvatureMassImprint M_ref M_der) M_ref rfl hder + +/-- Generic β− endpoint from parent and daughter mass budgets and the lepton slot. -/ +noncomputable def betaMinusEndpointQFromBudgets (M_parent M_daughter m_e : ℝ) : ℝ := + M_parent - M_daughter - m_e + +/-- β− endpoint with one uniform imprint on both isotope budgets. -/ +noncomputable def betaMinusEndpointQUniformImprint + (κ M_parent_der M_daughter_der m_e : ℝ) : ℝ := + imprintedMassBudget M_parent_der κ - imprintedMassBudget M_daughter_der κ - m_e + +/-- β− endpoint with independent per-isotope curvature imprints. -/ +noncomputable def betaMinusEndpointQPerIsotopeImprint + (κ_parent M_parent_der κ_daughter M_daughter_der m_e : ℝ) : ℝ := + imprintedMassBudget M_parent_der κ_parent - + imprintedMassBudget M_daughter_der κ_daughter - m_e + +theorem betaMinusEndpointQUniformImprint_eq_kappa_gap_minus_m_e + (κ M_parent_der M_daughter_der m_e : ℝ) : + betaMinusEndpointQUniformImprint κ M_parent_der M_daughter_der m_e = + κ * (M_parent_der - M_daughter_der) - m_e := by + unfold betaMinusEndpointQUniformImprint imprintedMassBudget + ring + +theorem betaMinusEndpointQPerIsotopeImprint_eq_reference_budgets + (κ_p M_p κ_d M_d M_p_ref M_d_ref m_e : ℝ) + (hp : imprintedMassBudget M_p κ_p = M_p_ref) + (hd : imprintedMassBudget M_d κ_d = M_d_ref) : + betaMinusEndpointQPerIsotopeImprint κ_p M_p κ_d M_d m_e = + betaMinusEndpointQFromBudgets M_p_ref M_d_ref m_e := by + unfold betaMinusEndpointQPerIsotopeImprint betaMinusEndpointQFromBudgets + rw [hp, hd] + +theorem betaMinusEndpointQPerIsotopeImprint_eq_mass_table + (M_p_der M_d_der M_p_ref M_d_ref m_e : ℝ) + (hp : 1e-30 < M_p_der) (hd : 1e-30 < M_d_der) : + betaMinusEndpointQPerIsotopeImprint + (curvatureMassImprint M_p_ref M_p_der) M_p_der + (curvatureMassImprint M_d_ref M_d_der) M_d_der m_e = + betaMinusEndpointQFromBudgets M_p_ref M_d_ref m_e := + betaMinusEndpointQPerIsotopeImprint_eq_reference_budgets _ _ _ _ _ _ _ + (imprintedMassBudget_eq_ref M_p_der (curvatureMassImprint M_p_ref M_p_der) M_p_ref rfl hp) + (imprintedMassBudget_eq_ref M_d_der (curvatureMassImprint M_d_ref M_d_der) M_d_ref rfl hd) + +/-- +Mass-budget difference for a $\beta^-$ step $(A,Z)\to(A,Z+1)$ at fixed p/n environment. +Matches `betaMinusMassGapAtXi` (nucleon-gap ledger). +-/ +noncomputable def betaMinusIsotopeMassGapAtXi + (A Z : ℕ) (env : NucleonEnvironment) (c : ℝ := 1) : ℝ := + (Z : ℝ) * protonMassAtXi env c + (neutronCount A Z : ℝ) * neutronMassAtXi env c - + ((Z + 1 : ℕ) : ℝ) * protonMassAtXi env c - + (neutronCount A (Z + 1) : ℝ) * neutronMassAtXi env c + +theorem betaMinusIsotopeMassGapAtXi_eq_betaMinusMassGapAtXi + (A Z : ℕ) (env : NucleonEnvironment) (c : ℝ) (h : Z < A) : + betaMinusIsotopeMassGapAtXi A Z env c = betaMinusMassGapAtXi env c := by + unfold betaMinusIsotopeMassGapAtXi betaMinusMassGapAtXi neutronCount + have hle : Z ≤ A := Nat.le_of_lt h + have hle' : Z + 1 ≤ A := by omega + simp only [Nat.cast_sub hle, Nat.cast_sub hle', Nat.cast_add, Nat.cast_one] + ring + +/-- Primary width-ledger endpoint: isotope budgets at shared p/n environment. -/ +noncomputable def betaMinusEndpointQNucleonGap + (A Z : ℕ) (env : NucleonEnvironment) (m_e : ℝ) (c : ℝ := 1) : ℝ := + betaMinusIsotopeMassGapAtXi A Z env c - m_e + +theorem betaMinusEndpointQNucleonGap_eq_betaMinusEndpointQAtXi + (A Z : ℕ) (env : NucleonEnvironment) (m_e c : ℝ) (h : Z < A) : + betaMinusEndpointQNucleonGap A Z env m_e c = betaMinusEndpointQAtXi env m_e c := by + unfold betaMinusEndpointQNucleonGap betaMinusEndpointQAtXi + rw [betaMinusIsotopeMassGapAtXi_eq_betaMinusMassGapAtXi (A:=A) (Z:=Z) env c h, + betaMinusMassGapAtXi_eq_derivedDeltaM] + +theorem betaMinusEndpointQNucleonGap_eq_derivedDeltaM_minus_m_e + (A Z : ℕ) (env : NucleonEnvironment) (m_e c : ℝ) (h : Z < A) : + betaMinusEndpointQNucleonGap A Z env m_e c = derivedDeltaM - m_e := by + rw [betaMinusEndpointQNucleonGap_eq_betaMinusEndpointQAtXi (A:=A) (Z:=Z) env m_e c h, + betaMinusEndpointQAtXi_eq_derivedDeltaM_minus_m_e] + +theorem betaMinusEndpointQUniformImprint_preserves_gap_shape + (κ M_p M_d m_e : ℝ) : + betaMinusEndpointQUniformImprint κ M_p M_d m_e = + κ * (M_p - M_d) - m_e := + betaMinusEndpointQUniformImprint_eq_kappa_gap_minus_m_e κ M_p M_d m_e + +/-- Symmetric cluster mass well ``B_cluster / A`` (mass ledger). -/ +noncomputable def betaClusterMassWell (clusterTotal A : ℝ) : ℝ := + clusterTotal / max A 1 + +/-- Interior partner well ``B_cluster / (A-1)`` for bonded clusters. -/ +noncomputable def betaInteriorPartnerWell (clusterTotal partners : ℝ) : ℝ := + clusterTotal / max partners 1 + +/-- +Geometric-mean blend of symmetric mass well and interior partner well (width ledger). +Witness exponent ``blend = 1/(2·partners)`` in \texttt{hqiv\_dynamic\_beta\_isotope.py}. +-/ +noncomputable def betaWidthWellGeometricBlend + (massWell interiorPartner partners : ℝ) : ℝ := + let blend := 1 / (2 * max partners 1) + massWell * (interiorPartner / max massWell 1e-30) ^ blend + +/-- Width-ledger curvature imprint on cluster caustic depth (comparison layer). -/ +noncomputable def widthWellCurvatureImprint (τ_ref τ_pred valley : ℝ) : ℝ := + (τ_ref / max τ_pred 1e-30) ^ (1 / max (valley + 1) 1) + +/-- Weak matrix-element slot: overlap residual carried to fourth power by m_e. -/ +noncomputable def betaWeakMatrixElementSquared + (residual m_e : ℝ) : ℝ := + (max residual 0 / max m_e 1e-30) ^ 4 + +/-- Generic valley-count bound for a mass number: `2 · (A − 1)` (`HQIVNuclei.valleyCount_le_two_mul_pred`). -/ +def betaValleyCountBound (A : ℕ) : ℕ := + if A ≤ 1 then 0 else 2 * (A - 1) + +/-- Active caustic layer count from the hierarchical stack (pair + torus + deepen + optional tetra). -/ +def betaCausticLayerCount (A : ℕ) : ℕ := + if A ≤ 1 then 0 + else + let deepen := if A ≤ 2 then 0 else A - 2 + (if 4 ≤ A then 1 else 0) + 2 + deepen + +/-- +Geometry / spin-statistics width factor for bonded clusters. + +Free nucleons (`A ≤ 1`) carry unit factor. Bonded clusters suppress weak tipping by +`(residual / well)^(valley + 1)`: each valley contact from the isotope ladder plus +one fermionic spin-statistics slot (`SpinStatistics` / `HQIVNuclei`). +-/ +noncomputable def betaGeometryWidthFactor + (A : ℕ) (residual well : ℝ) (bonded : Bool) : ℝ := + if A ≤ 1 ∨ ¬ bonded then 1 + else + let valley := (betaValleyCountBound A : ℝ) + let ratio := max residual 0 / max well (max residual 1e-30) + ratio ^ (valley + 1) + +/-- Weak width from `beta_decay_rate` with the overlap residual in the matrix-element slot. -/ +noncomputable def betaWeakWidthFromResidual + (channel : BetaDecayChannel) (residual m_e ℳ : ℝ) : ℝ := + let slot := betaWeakMatrixElementSquared residual m_e + match channel with + | .betaMinus => beta_decay_rate Fermion.neutron m_e (ℳ * Real.sqrt slot) + | .betaPlus => beta_decay_rate Fermion.proton m_e (ℳ * Real.sqrt slot) + +/-- Weak β width slot using the existing Fermi/tipping scaffold. -/ +noncomputable def betaWeakWidthSlot + (channel : BetaDecayChannel) (m_e ℳ : ℝ) : ℝ := + match channel with + | .betaMinus => beta_decay_rate Fermion.neutron m_e ℳ + | .betaPlus => beta_decay_rate Fermion.proton m_e ℳ + +theorem betaWeakWidthSlot_betaMinus (m_e ℳ : ℝ) : + betaWeakWidthSlot .betaMinus m_e ℳ = beta_decay_rate Fermion.neutron m_e ℳ := rfl + +theorem betaWeakWidthSlot_betaPlus (m_e ℳ : ℝ) : + betaWeakWidthSlot .betaPlus m_e ℳ = beta_decay_rate Fermion.proton m_e ℳ := rfl + +/-- Deuteron dynamic environment from the existing isotope ladder witness. -/ +def dynamicDeuteronEnvironment (env : NucleonEnvironment) : + DynamicIsotopeEnvironment 2 1 where + ladder := deuteron + nucleonEnv := env + +/-- ³He dynamic environment from the existing isotope ladder witness. -/ +def dynamicHelium3Environment (env : NucleonEnvironment) : + DynamicIsotopeEnvironment 3 2 where + ladder := helium3 + nucleonEnv := env + +/-- ⁴He dynamic environment from the existing isotope ladder witness. -/ +def dynamicHelium4Environment (env : NucleonEnvironment) : + DynamicIsotopeEnvironment 4 2 where + ladder := helium4 + nucleonEnv := env + +theorem dynamicHelium4_valleyCount (env : NucleonEnvironment) : + valleyCount (dynamicHelium4Environment env).ladder = 6 := by + rfl + +end + +end Hqiv.Physics diff --git a/Hqiv/Physics/DynamicIsotopeStability.lean b/Hqiv/Physics/DynamicIsotopeStability.lean new file mode 100644 index 0000000..b69a885 --- /dev/null +++ b/Hqiv/Physics/DynamicIsotopeStability.lean @@ -0,0 +1,108 @@ +import Hqiv.Physics.DynamicBetaIsotope +import Hqiv.Physics.DerivedGaugeAndLeptonSector + +/-! +# Dynamic isotope stability and half-life slots + +This module turns the dynamic β/isotope ledgers into a stability predicate. + +The rule is structural: + +* β residuals come from `DynamicBetaIsotope`. +* A bonded nuclear well shields those residuals by `nucleonWellContribution`. +* A β channel is structurally open only when the shielded residual is positive. +* A stability / half-life **claim** requires `betaWidthLedgerQualified`: positive + endpoint `Q` and positive shielded overlap residual on the weak channel. + Stable isotopes instead require structural shielding (residuals non-positive). +-/ + +namespace Hqiv.Physics + +noncomputable section + +/-- Shielding supplied by the bonded nuclear well. -/ +noncomputable def isotopeWellShield (env : NucleonEnvironment) : ℝ := + nucleonWellContribution env + +/-- Effective β− residual after nuclear well shielding. -/ +noncomputable def betaMinusEffectiveResidualAtXi + (env : NucleonEnvironment) (c : ℝ := 1) : ℝ := + betaMinusResidualAtXi env c - isotopeWellShield env + +/-- Effective β+ residual after nuclear well shielding. -/ +noncomputable def betaPlusEffectiveResidualAtXi + (env : NucleonEnvironment) (c : ℝ := 1) : ℝ := + betaPlusResidualAtXi env c - isotopeWellShield env + +/-- A β channel is energetically active when its shielded residual is positive. -/ +def betaChannelActive (residual : ℝ) : Prop := 0 < residual + +/-- Weak β channel is kinematically open once the endpoint Q and overlap residual are positive. -/ +def weakBetaChannelOpen (endpointQ residual : ℝ) : Prop := + 0 < endpointQ ∧ 0 < residual + +/-- Structural shielding: neither β− nor β+ residual is open after the nuclear well. -/ +def structurallyShieldedIsotope (env : NucleonEnvironment) (c : ℝ := 1) : Prop := + betaMinusEffectiveResidualAtXi env c ≤ 0 ∧ + betaPlusEffectiveResidualAtXi env c ≤ 0 + +/-- +Weak width ledger qualified: kinematic endpoint `Q` and shielded overlap residual +are both positive (`weakBetaChannelOpen`). +-/ +def betaWidthLedgerQualified (env : NucleonEnvironment) (m_e : ℝ) (c : ℝ := 1) : Prop := + weakBetaChannelOpen (betaMinusEndpointQAtXi env m_e c) (betaMinusEffectiveResidualAtXi env c) + +/-- Legacy export name used in papers and Python witnesses. -/ +def EMTippingQualified (env : NucleonEnvironment) (c : ℝ := 1) : Prop := + betaWidthLedgerQualified env m_e_PDG c + +/-- +Qualified dynamic stability for bonded nuclei: β channels structurally closed. +Half-life **width** claims on open channels use `betaWidthLedgerQualified` instead. +-/ +def dynamicallyStableIsotope (env : NucleonEnvironment) (c : ℝ := 1) : Prop := + structurallyShieldedIsotope env c + +theorem betaWidthLedgerQualified_of_open + (env : NucleonEnvironment) (m_e c : ℝ) + (hQ : 0 < betaMinusEndpointQAtXi env m_e c) + (hR : 0 < betaMinusEffectiveResidualAtXi env c) : + betaWidthLedgerQualified env m_e c := + ⟨hQ, hR⟩ + +theorem EMTippingQualified_of_open + (env : NucleonEnvironment) (c : ℝ) + (hQ : 0 < betaMinusEndpointQAtXi env m_e_PDG c) + (hR : 0 < betaMinusEffectiveResidualAtXi env c) : + EMTippingQualified env c := + betaWidthLedgerQualified_of_open env m_e_PDG c hQ hR + +theorem structurallyShielded_of_residuals_nonpos + (env : NucleonEnvironment) (c : ℝ) + (hm : betaMinusEffectiveResidualAtXi env c ≤ 0) + (hp : betaPlusEffectiveResidualAtXi env c ≤ 0) : + structurallyShieldedIsotope env c := ⟨hm, hp⟩ + +theorem dynamicallyStable_of_residuals_nonpos + (env : NucleonEnvironment) (c : ℝ) + (hm : betaMinusEffectiveResidualAtXi env c ≤ 0) + (hp : betaPlusEffectiveResidualAtXi env c ≤ 0) : + dynamicallyStableIsotope env c := + structurallyShielded_of_residuals_nonpos env c hm hp + +/-- Width slot for an active β channel. `Γ` is supplied by the weak tipping model. -/ +noncomputable def betaHalfLifeFromWidth (Γ : ℝ) : ℝ := + half_life_from_width Γ + +theorem betaHalfLifeFromWidth_eq (Γ : ℝ) : + betaHalfLifeFromWidth Γ = Real.log 2 / Γ := rfl + +theorem free_lockin_wellShield_zero : + isotopeWellShield freeLockinNucleonEnvironment = 0 := by + unfold isotopeWellShield nucleonWellContribution freeLockinNucleonEnvironment + simp + +end + +end Hqiv.Physics diff --git a/Hqiv/Physics/DynamicNucleonPN.lean b/Hqiv/Physics/DynamicNucleonPN.lean new file mode 100644 index 0000000..61a43e0 --- /dev/null +++ b/Hqiv/Physics/DynamicNucleonPN.lean @@ -0,0 +1,127 @@ +import Hqiv.Physics.DerivedNucleonMass +import Hqiv.Physics.NuclearOutsideTemperatureDynamics + +/-! +# Dynamic proton / neutron readout + +This module builds the first `nucleon(p,n)` layer after the nuclear outside-temperature +dynamics are locked down. + +The construction is intentionally thin: + +* `NucleonFlavor` chooses the already-derived constituent channel (`uud` or `udd`). +* `NucleonEnvironment` carries the common shell, ξ, nuclear well depth, and bonded/free flag. +* The same ξ-dependent own-binding and well contribution are subtracted from both flavors. + +Therefore the absolute proton/neutron masses can move with outside curvature and the nuclear +well, but the p–n splitting is still the derived constituent/isospin split until an explicit +flavor-dependent weak or EM tipping layer is added. +-/ + +namespace Hqiv.Physics + +noncomputable section + +/-- Proton/neutron flavor tag for the dynamic nucleon function. -/ +inductive NucleonFlavor + | proton + | neutron + deriving DecidableEq, Repr + +/-- Environment shared by a proton/neutron readout. -/ +structure NucleonEnvironment where + /-- Binding shell for the nucleon's own composite trace. -/ + shell : ℕ := referenceM + /-- Continuous horizon coordinate. `xiLockin = 5` is the calibrated lock-in point. -/ + ξ : ℝ := xiLockin + /-- Nuclear well depth supplied by the caustic stack / embedding. -/ + wellDepth : ℝ := 0 + /-- If true, the well depth participates; if false this is a free branch. -/ + bonded : Bool := false + +/-- Constituent channel selected by flavor. -/ +noncomputable def nucleonConstituentEnergy : NucleonFlavor → ℝ + | .proton => protonConstituentEnergy + | .neutron => neutronConstituentEnergy + +/-- Common own-binding at ξ from the outside-curvature temperature module. -/ +noncomputable def nucleonOwnBindingInEnvironment + (env : NucleonEnvironment) (c : ℝ := 1) : ℝ := + nucleonOwnBindingAtXi env.shell env.ξ c + +/-- Nuclear well contribution: bonded branches subtract the positive well slot. -/ +noncomputable def nucleonWellContribution (env : NucleonEnvironment) : ℝ := + if env.bonded then max 0 env.wellDepth else 0 + +/-- +Dynamic proton/neutron mass readout. + +This is the first `nucleon(p,n)` function: constituent energy minus the common +temperature-modulated own-binding and the common bonded well contribution. +-/ +noncomputable def nucleonMassAtXi + (flavor : NucleonFlavor) (env : NucleonEnvironment) (c : ℝ := 1) : ℝ := + nucleonConstituentEnergy flavor - + nucleonOwnBindingInEnvironment env c - + nucleonWellContribution env + +/-- Convenience aliases for the dynamic p/n readouts. -/ +noncomputable def protonMassAtXi (env : NucleonEnvironment) (c : ℝ := 1) : ℝ := + nucleonMassAtXi .proton env c + +noncomputable def neutronMassAtXi (env : NucleonEnvironment) (c : ℝ := 1) : ℝ := + nucleonMassAtXi .neutron env c + +theorem protonMassAtXi_eq (env : NucleonEnvironment) (c : ℝ) : + protonMassAtXi env c = + protonConstituentEnergy - + nucleonOwnBindingInEnvironment env c - + nucleonWellContribution env := rfl + +theorem neutronMassAtXi_eq (env : NucleonEnvironment) (c : ℝ) : + neutronMassAtXi env c = + neutronConstituentEnergy - + nucleonOwnBindingInEnvironment env c - + nucleonWellContribution env := rfl + +/-- +The dynamic environment does not split p from n by itself. + +The p–n gap remains the derived constituent/isospin split because own-binding and +well-depth are shared. β± and weak widths are separate slots. +-/ +theorem neutron_proton_gap_preserved_at_xi + (env : NucleonEnvironment) (c : ℝ) : + neutronMassAtXi env c - protonMassAtXi env c = derivedDeltaM := by + unfold neutronMassAtXi protonMassAtXi nucleonMassAtXi nucleonConstituentEnergy + rw [constituent_isospin_splitting] + ring + +/-- Free lock-in environment: no nuclear well, shell `referenceM`, ξ = lock-in. -/ +def freeLockinNucleonEnvironment : NucleonEnvironment where + shell := referenceM + ξ := xiLockin + wellDepth := 0 + bonded := false + +/-- Bonded environment builder with a supplied caustic well depth. -/ +def bondedNucleonEnvironmentAtXi (shell : ℕ) (ξ wellDepth : ℝ) : NucleonEnvironment where + shell := shell + ξ := ξ + wellDepth := wellDepth + bonded := true + +/-- β− overlap slot for a dynamic environment. -/ +noncomputable def betaMinusOverlapForEnvironment (env : NucleonEnvironment) : ℝ := + betaMinusOverlapAtXi env.ξ + +/-- β+ structural mirror slot. Weak widths remain outside this mass readout. -/ +noncomputable def betaPlusOverlapForEnvironment (env : NucleonEnvironment) (c : ℝ := 1) : ℝ := + nucleonOwnBindingInEnvironment env c + +theorem betaMinusOverlapForEnvironment_eq (env : NucleonEnvironment) : + betaMinusOverlapForEnvironment env = betaMinusOverlapAtXi env.ξ := rfl + +end + +end Hqiv.Physics diff --git a/Hqiv/Physics/G2AutomorphismEnergyCost.lean b/Hqiv/Physics/G2AutomorphismEnergyCost.lean new file mode 100644 index 0000000..a5134bf --- /dev/null +++ b/Hqiv/Physics/G2AutomorphismEnergyCost.lean @@ -0,0 +1,30 @@ +import Hqiv.Algebra.PhaseLiftDelta + +namespace Hqiv.Physics + +/-! +# Phase-lift / “automorphism cost” scalar slot (shell `m`) + +`Hqiv.Algebra.phaseLiftCoeff` is the proved HQIV scalar **φ(m)/6** used wherever the matrix +`phaseLiftDelta` is scaled to a shell (`PhaseLiftDelta` module doc). + +External brane–bulk narratives sometimes describe a **G₂ automorphism energy cost**. This file +does **not** identify that story with Planck units, continuum Yang–Mills, or Clay `Δ`. It only +exposes the **existing** positive shell readout under a physics-facing name so later bridges can +cite one stable definition. +-/ + +open Hqiv.Algebra + +/-- Positive scalar tied to phase-lift strength at shell `m` (definitionally `φ(m)/6`). -/ +noncomputable abbrev automorphismEnergyCostAtShell (m : ℕ) : ℝ := + phaseLiftCoeff m + +theorem automorphismEnergyCostAtShell_pos (m : ℕ) : 0 < automorphismEnergyCostAtShell m := + phaseLiftCoeff_pos m + +theorem automorphismEnergyCostAtShell_eq_phi_div_six (m : ℕ) : + automorphismEnergyCostAtShell m = Hqiv.phi_of_shell m / 6 := + rfl + +end Hqiv.Physics diff --git a/Hqiv/Physics/HomogeneousCurvatureSecondOrder.lean b/Hqiv/Physics/HomogeneousCurvatureSecondOrder.lean new file mode 100644 index 0000000..019a18b --- /dev/null +++ b/Hqiv/Physics/HomogeneousCurvatureSecondOrder.lean @@ -0,0 +1,67 @@ +import Hqiv.Physics.DynamicBBNBaryogenesis +import Hqiv.Physics.HopfShellBeltramiMassBridge +import Hqiv.QuantumChemistry.DynamicBindingChart + +/-! +# Homogeneous-curvature second order with local defect feedback + +**Program (not yet the default chart):** + +1. Compute the **homogeneous** curvature budget `B_hom(ξ, ρ)` at bulk medium density ρ + (unity at dilute limit, full `B_curv(ξ)` at ice-like ρ = 1). +2. Add a **local** perturbation `δB` from nucleation / defect sites (coordination spike above + the homogeneous background) — same geometric role as BBN `bbn_binding_curvature_perturbation`. +3. Feed `B_eff = B_hom + δB` back into the binding / melt readout (κ₆ and outside `G_eff`). + +Nucleation sites matter because they break homogeneity: a dust grain, surface defect, or +local H-bond template raises `δB` before the bulk phase is stable. + +Python mirror: `scripts/hqiv_homogeneous_curvature_feedback.py`. + +Phase geometry supplies ρ without atom counting: `Hqiv.QuantumChemistry.PhaseGeometryDensity`. +-/ + +namespace Hqiv.Physics + +open Hqiv +open Hqiv.QuantumChemistry + +/-- Medium density ρ ∈ [0,1]: intermolecular coordination vs ice tetrahedral reference. -/ +def clampMediumDensity (ρ : ℝ) : ℝ := max 0 (min 1 ρ) + +/-- κ(ξ) coupling slot used as homogeneous curvature budget proxy (chart spine). -/ +noncomputable def curvatureBudgetAtXi (ξ : ℝ) : ℝ := + dynamicBindingCurvatureCouplingAtXi ξ + +/-- Homogeneous bulk curvature budget: dilute → 1, fully condensed → `curvatureBudgetAtXi`. -/ +noncomputable def homogeneousCurvatureBudgetAtXi (ξ ρ : ℝ) : ℝ := + let ρc := clampMediumDensity ρ + 1 + ρc * (curvatureBudgetAtXi ξ - 1) + +/-- Local defect excess above homogeneous background (nucleation / surface site). -/ +noncomputable def localCurvatureDefectExcess (δ_coord : ℝ) : ℝ := + gamma_HQIV * strongChannelFraction * max δ_coord 0 + +/-- Effective curvature budget entering second-order feedback. -/ +noncomputable def effectiveCurvatureBudgetAtXi (ξ ρ δ_coord : ℝ) : ℝ := + homogeneousCurvatureBudgetAtXi ξ ρ + localCurvatureDefectExcess δ_coord + +/-- +Second-order binding feedback using **effective** homogeneous+local budget. + +Replaces bare `dynamicBindingCurvatureFeedbackSecondOrderAtXi` once the homogeneous +medium and nucleation defect are supplied — κ couples to `(B_eff − 1)` not raw chart ξ alone. +-/ +noncomputable def bindingCurvatureFeedbackSecondOrderHomogeneous + (ξ ρ δ_coord : ℝ) : ℝ := + let bEff := effectiveCurvatureBudgetAtXi ξ ρ δ_coord + let κ := gamma_HQIV * strongChannelFraction * bEff + let cRel := clusterBindingContrastRelative + let c2Ratio := tuftLapseConcentrationAtXi ξ 0 0 / tuftLapseConcentrationAtXi xiLockin 0 0 + (1 + κ * cRel) * c2Ratio + +/-- Nucleation raises local curvature: defect coordination above homogeneous ρ. -/ +noncomputable def nucleationCoordinationExcess (ρ_hom ρ_local : ℝ) : ℝ := + max (ρ_local - clampMediumDensity ρ_hom) 0 + +end Hqiv.Physics diff --git a/Hqiv/Physics/NaturalUnitMeVTheory.lean b/Hqiv/Physics/NaturalUnitMeVTheory.lean new file mode 100644 index 0000000..6bc6d86 --- /dev/null +++ b/Hqiv/Physics/NaturalUnitMeVTheory.lean @@ -0,0 +1,67 @@ +/-! +# Natural-unit MeV readout layer (conceptual) + +This file records the high-level MeV chart philosophy and the trapped-radiative +/ shell-sampled curvature imprint direction. The shell labels are readout +samples of the moving carrier; they are not intended to do the mass generation +alone. + +All executable low-level definitions and wiring live in the main +bridge file (`HopfShellBeltramiMassBridge.lean`) to keep this file +lightweight and the builds green. + +See the AGENTS document for the current detailed status of the +per-shell α_n attack and the trapped-Casimir reading. +-/ + +namespace Hqiv.Physics + +/-! ## Suggested step 2 focus: Lepton-specific chart example + +The proton export chart (`referenceM`) is a **hadronic calibration convention**, not a derived +shell. The current mass readout is driven by the carrier geometry, trapped Planck / Casimir budget, +and phase motion on the TUFT heavy chart (`tuftHeavyChartShell`), not by treating `m = 4` as +physics output. + +An optional lepton-specific chart can be constructed using the T3 gap candidate +(or T12-modulated trapping on the n=3 heavy shell) as the heavy lepton anchor. +This can bring the heavy lepton natural-unit readout into ballpark range while +preserving the proton chart as the default for hadrons. + +The T12 witness + trappingSelectionFromThreeHopfShellsWithAlphas (with α_n from +the three integrable Hopf shells) supply the per-shell imprint data needed for +such a chart. See the dedicated section in the bridge for the explicit three-step +focus (heavy observable decision, this lepton chart, and the gluonic vs leptonic +scoping). + +The ontological tension (gluonic vs color-neutral lepton masses on the same +carrier) is documented honestly in the bridge and the md. +-/ + +/-! ## Accurate T → mass in MeV (T1-T13 complete, bidirectional, physical units) + +The bridge now exposes the full dynamic pipeline wired to MeV: + +* `heavy_lepton_gap_at_physical_T_MeV T_phys_MeV` -- T (e.g. CMB 2.725 K in MeV) → heavy lepton mass in MeV +* `leptonMassSpectrum_at_physical_T_MeV T_phys_MeV` -- full (heavy, μ, e) in MeV +* `heavy_lepton_gap_CMB_today_MeV`, `..._BBN_window_MeV` +* `xi_for_target_heavy_mass` / `physical_T_for_target_heavy_mass` (inverse chart helpers) +* `heavy_lepton_scale_multiplier_at_physical_T` (the pure geometry factor ~183× at CMB vs lock-in) + +All numbers are produced by the complete pulled T8 (zeta leading on heavy shell) + +T11 (torsionMatrixCoefficient = 4/5 on T12 n=3 witness) + T10 (144/91 admissible row) + +T12 (three-shell per-imprint trapping + cannot_factor) + dynamic T13 outer suppression on +the neutral singlet extension (recovering 1/140 at lock-in) + the inner/outer Casimir dynamic scale running with +`omegaK_xi(ξ)` from the continuous curvature primitive on the temperature ladder. + +At ξ=5 (vev/lock-in read from the ladder) the legacy good ratios are recovered exactly. +At any other T the absolute scale and the generation splittings evolve according to the +same Casimir symmetry-breaking mechanism acting on the inside contact surfaces vs. the +outer neutral surface of the carrier. + +See `HopfShellBeltramiMassBridge.lean` (the MeV-anchored readouts section and the long +"Temperature to mass spectrum" docstring) for the executable defs and the #checks. +The synthesis narrative is in `AGENTS/TUFT_INNER_OUTER_CASIMIR_DYNAMICS.md`. +-/ + +end Hqiv.Physics diff --git a/Hqiv/Physics/NeutronBindingStabilityScaffold.lean b/Hqiv/Physics/NeutronBindingStabilityScaffold.lean new file mode 100644 index 0000000..5487aee --- /dev/null +++ b/Hqiv/Physics/NeutronBindingStabilityScaffold.lean @@ -0,0 +1,194 @@ +import Hqiv.Geometry.OctonionicLightCone +import Hqiv.Physics.DerivedNucleonMass +import Hqiv.Physics.ReadoutGaugeSeed +import Hqiv.Physics.HQIVNuclei +import Hqiv.Physics.NuclearAndAtomicSpectra +import Hqiv.Physics.ContinuousXiPath + +namespace Hqiv.Physics + +open Hqiv.Physics.ContinuousXiPath + +/-! +# Neutron binding stability scaffold (bonded vs free) + +Paper: `papers/nucleon_binding/hqiv_nucleon_binding_from_composite_trace.tex`, Conjecture β (curvature ledger + +skew alignment in nuclear wells vs sub-lock-in free branch). + +**Proved here:** packaging of existing binding (`nucleonSharedBinding_MeV`), spin–statistics +width identity (`Γ = ΔE/ħ`), continuous-ξ lock-in calibration (`omegaK_xi xiLockin = 1`), +conditional discrete–continuous Ωₖ readout at `referenceM`, and ledger separation +(`NeutronLifetimeMethod`: bottle/beam read weak Ledger III, not Ledger I). + +**Explicit open slots (`Prop` / quantitative dressing):** full skew realignment in nuclear +wells (antisymmetry of `phaseLiftDelta` is proved); trap-embedding width dressing magnitudes +(`TrapWeakBridgeDecoherenceSlot`). +-/ + +/-! ## Embedding and stability predicates -/ + +/-- +Nuclear environment for a neutron: well depth from `nuclear_effective_potential` / +integrated Maxwell well / deuteron-scale bookkeeping, Ωₖ readout, continuous-ξ coordinate, +and skew alignment (Conjecture β). +-/ +structure NuclearNeutronEmbedding where + /-- Environmental well depth (MeV-scale bookkeeping; not the shared baryon trace alone). -/ + wellDepth : ℝ + /-- Normalized Ωₖ-type readout at the embedding shell (≥ 1 when the ledger is closed). -/ + omegaReadout : ℝ + /-- Horizon coordinate ξ on the continuous chart (`xiOfShell m = m + 1`). -/ + xiReadout : ℝ + /-- Triality-compatible skew realignment (Conjecture β; not discharged here). -/ + skewAligned : Prop + +/-- Shared composite-trace binding plus a nonnegative nuclear well closes the depth slot. -/ +def wellDepthSufficient (e : NuclearNeutronEmbedding) : Prop := + 0 < e.wellDepth + nucleonSharedBinding_MeV + +/-- Curvature ledger closed at or above lock-in calibration (Ω ≥ 1). -/ +def curvatureLedgerClosed (e : NuclearNeutronEmbedding) : Prop := + 1 ≤ e.omegaReadout + +/-- Bonded neutron stability: depth + closed Ω ledger + skew alignment (Conjecture β). -/ +def bondedNeutronStable (e : NuclearNeutronEmbedding) : Prop := + wellDepthSufficient e ∧ curvatureLedgerClosed e ∧ e.skewAligned + +/-! ## Free branch: overlap energy and decay channels -/ + +/-- Sub-lock-in curvature deficit (zero when `omegaReadout ≥ 1`). -/ +noncomputable def freeNeutronCurvatureDeficit (omegaReadout : ℝ) : ℝ := + max 0 (1 - omegaReadout) + +/-- +Strong-resonance overlap witness: hypercharge bookkeeping gap plus optional curvature deficit. + +Not identified with the full β Q-value (~0.78 MeV); see Conjecture β remark in the nucleon paper. +-/ +noncomputable def freeNeutronOverlapEnergy (omegaReadout : ℝ) : ℝ := + nucleonIsospinGap_MeV + freeNeutronCurvatureDeficit omegaReadout + +theorem freeNeutronCurvatureDeficit_nonneg (omegaReadout : ℝ) : + 0 ≤ freeNeutronCurvatureDeficit omegaReadout := by + unfold freeNeutronCurvatureDeficit + positivity + +theorem freeNeutronOverlapEnergy_nonneg (omegaReadout : ℝ) : + 0 ≤ freeNeutronOverlapEnergy omegaReadout := by + unfold freeNeutronOverlapEnergy freeNeutronCurvatureDeficit + rw [nucleonIsospinGap_eq_one] + positivity + +theorem freeNeutronOverlapEnergy_eq_isospinGap_when_ledger_closed + {ω : ℝ} (hω : 1 ≤ ω) : + freeNeutronOverlapEnergy ω = nucleonIsospinGap_MeV := by + unfold freeNeutronOverlapEnergy freeNeutronCurvatureDeficit + have hmax : max 0 (1 - ω) = 0 := by + rw [max_eq_left (by linarith)] + rw [hmax, nucleonIsospinGap_eq_one, add_zero] + +theorem freeNeutronOverlapEnergy_pos (omegaReadout : ℝ) : + 0 < freeNeutronOverlapEnergy omegaReadout := by + unfold freeNeutronOverlapEnergy freeNeutronCurvatureDeficit + rw [nucleonIsospinGap_eq_one] + have hnonneg : 0 ≤ max 0 (1 - omegaReadout) := by positivity + linarith + +def freeNeutronCurvatureSubLockin (omegaReadout : ℝ) : Prop := + omegaReadout < 1 + +theorem freeNeutronCurvatureDeficit_pos_of_subLockin + {ω : ℝ} (hω : freeNeutronCurvatureSubLockin ω) : + 0 < freeNeutronCurvatureDeficit ω := by + unfold freeNeutronCurvatureDeficit freeNeutronCurvatureSubLockin at * + have h1w : 1 - ω > 0 := by linarith + simpa [max_eq_left h1w.le] using h1w + +theorem freeNeutronOverlapEnergy_gt_isospinGap_of_subLockin + {ω : ℝ} (hω : freeNeutronCurvatureSubLockin ω) : + nucleonIsospinGap_MeV < freeNeutronOverlapEnergy ω := by + unfold freeNeutronOverlapEnergy freeNeutronCurvatureDeficit + rw [nucleonIsospinGap_eq_one] + exact lt_add_of_pos_right _ (freeNeutronCurvatureDeficit_pos_of_subLockin hω) + +/-! ## Strong width vs weak β channel (kept separate) -/ + +/-- Strong-resonance width `Γ = ΔE/ħ` from `SpinStatistics` / `HQIVNuclei`. -/ +noncomputable def freeNeutronStrongDecayWidth (omegaReadout : ℝ) : ℝ := + decayWidth_per_s (freeNeutronOverlapEnergy omegaReadout) + +/-- +Weak β width slot: electric tipping / `G_F_from_beta` (not the strong `ΔE/ħ` line). + +Lifetime ~ 880 s is **not** derived from `freeNeutronOverlapEnergy`. +-/ +noncomputable def freeNeutronWeakDecayWidth (m_e ℳ : ℝ) : ℝ := + beta_decay_rate Fermion.neutron m_e ℳ + +theorem freeNeutronStrongDecayWidth_pos (omegaReadout : ℝ) : + 0 < freeNeutronStrongDecayWidth omegaReadout := by + unfold freeNeutronStrongDecayWidth decayWidth_per_s + exact div_pos (freeNeutronOverlapEnergy_pos omegaReadout) (by unfold hbar_MeV_s; norm_num) + +theorem free_neutron_strong_half_life_from_spin_statistics (omegaReadout : ℝ) : + half_life_from_width (freeNeutronStrongDecayWidth omegaReadout) = + resonance_half_life (freeNeutronOverlapEnergy omegaReadout) := + spin_statistics_determines_half_life (freeNeutronOverlapEnergy_pos omegaReadout) + +/-! ## Continuous ξ participation (lock-in calibration) -/ + +/-- +Readout at lock-in on the continuous chart: `omegaK_xi xiLockin = 1`. + +Uses only the proved continuous lock-in theorem (no global Ω bridge required). +-/ +theorem bondedNeutronReadoutCalibrated + (e : NuclearNeutronEmbedding) (hXi : e.xiReadout = xiLockin) : + omegaK_xi e.xiReadout = 1 := by + rw [hXi] + simpa [omegaK_partial_xi] using omegaK_partial_xi_lockin + +theorem bondedNeutronReadoutCalibrated_discrete + (hpos : 0 < curvature_integral referenceM) : + omega_k_partial referenceM = 1 := + omega_k_partial_at_reference hpos + +/-- +When the global `Ωₖ` integer bridge holds and the embedding sits at lock-in ξ, +continuous and discrete readouts agree and equal `1`. +-/ +theorem bondedNeutronOmegaReadout_matches_continuous_at_lockin + (hBridge : readoutOmegaKIntegerBridge) + (hpos : 0 < curvature_integral referenceM) + (e : NuclearNeutronEmbedding) (hXi : e.xiReadout = xiLockin) : + omegaK_xi e.xiReadout = omega_k_partial referenceM ∧ + omegaK_xi xiLockin = 1 ∧ omega_k_partial referenceM = 1 := by + have hΩxi : omegaK_xi e.xiReadout = 1 := bondedNeutronReadoutCalibrated e hXi + have hΩdisc : omega_k_partial referenceM = 1 := omega_k_partial_at_reference hpos + refine ⟨?_, ?_, ?_⟩ + · rw [hXi, xiLockin_eq_xiOfShell_referenceM, hBridge referenceM, hΩdisc] + · exact omegaK_partial_xi_lockin + · exact hΩdisc + +theorem bondedNeutron_curvatureLedger_from_lockin_xi + (e : NuclearNeutronEmbedding) (hXi : e.xiReadout = xiLockin) + (hΩ : e.omegaReadout = omegaK_xi e.xiReadout) : + curvatureLedgerClosed e := by + unfold curvatureLedgerClosed + rw [hΩ, bondedNeutronReadoutCalibrated e hXi] + +/-- No unfavorable imprint increment at a fixed calibrated ξ (degenerate step). -/ +theorem bondedNeutron_unfavorableImprint_zero_at_lockin + (e : NuclearNeutronEmbedding) (hXi : e.xiReadout = xiLockin) : + imprintWeightedReadoutPhase_xi e.xiReadout e.xiReadout = 0 := by + rw [hXi] + exact imprintWeightedReadoutPhase_xi_of_omega_eq xiLockin xiLockin rfl + +theorem bondedNeutron_imprint_matches_discrete_at_reference + (hBridge : readoutOmegaKIntegerBridge) : + imprintWeightedReadoutPhase_xi_alias + (xiOfShell referenceM) (xiOfShell (referenceM + 1)) = + imprintWeightedReadoutPhase referenceM := + imprintWeightedReadoutPhase_xi_matches_integer_step hBridge referenceM + +end Hqiv.Physics diff --git a/Hqiv/Physics/NeutronLifetimeMethod.lean b/Hqiv/Physics/NeutronLifetimeMethod.lean new file mode 100644 index 0000000..33adbcd --- /dev/null +++ b/Hqiv/Physics/NeutronLifetimeMethod.lean @@ -0,0 +1,298 @@ +import Hqiv.Physics.DynamicIsotopeStability +import Hqiv.Physics.WeakFanoHopfBridge +import Hqiv.Algebra.PhaseLiftDelta +import Mathlib.Algebra.Order.Field.Basic + +open Hqiv.Algebra + +/-! +# Neutron lifetime measurement methods (bottle vs beam) + +Formalizes the bottle/beam ledger: + +* both methods read **Ledger III** (weak β width), not Ledger I (strong overlap); +* **UCN trap magnetic field** is the primary bottle dressing slot: `B` maps to a + dimensionless **curvature fraction** on the weak Fano/Hopf bridge (not Zeeman energy); +* lab **temperature** is a sub-leading outside-support witness (~10³ ppm), insufficient + alone for the ~1.2×10⁴ ppm split; +* directional expectation `τ_beam > τ_bottle` follows once trap magnetic width dressing + exceeds the beam (near-zero `B`) dressing. + +Python witness export: `neutron_method_environment_ledger` in +`scripts/hqiv_isotope_pdg_benchmark.py`. +-/ + +namespace Hqiv.Physics + +noncomputable section + +/-! ## Measurement setup -/ + +/-- Laboratory neutron lifetime measurement class. -/ +inductive NeutronLifetimeMethod + | bottle + | beam + deriving DecidableEq + +/-- Method-specific environment. Temperature is metadata; trap `B` is the bottle lever. -/ +structure NeutronMethodSetup where + method : NeutronLifetimeMethod + labTemperatureK : ℝ + trapMagneticFieldTesla : ℝ + hT : 0 < labTemperatureK + hB : 0 ≤ trapMagneticFieldTesla + +def bottleMethodSetup : NeutronMethodSetup where + method := .bottle + labTemperatureK := 4 + trapMagneticFieldTesla := 2.5 + hT := by norm_num + hB := by norm_num + +def beamMethodSetup : NeutronMethodSetup where + method := .beam + labTemperatureK := 300 + trapMagneticFieldTesla := 0 + hT := by norm_num + hB := by norm_num + +def trapEmbeddingActive (s : NeutronMethodSetup) : Prop := + s.method = .bottle + +def freeBranchTransportActive (s : NeutronMethodSetup) : Prop := + s.method = .beam + +theorem bottleMethod_trapEmbedding : trapEmbeddingActive bottleMethodSetup := rfl + +theorem beamMethod_freeBranchTransport : freeBranchTransportActive beamMethodSetup := rfl + +/-! ## UCN trap magnetic field as curvature on the weak bridge -/ + +/-- Structural unit for a superconducting UCN storage field (tesla); not fitted to τ. -/ +def ucnTrapReferenceFieldTesla : ℝ := 1 + +/-- Magnetic field strength → dimensionless curvature fraction on the trap (`∈ [0,1]`). -/ +def trapMagneticCurvatureFraction (B : ℝ) : ℝ := + max 0 (min 1 (B / ucnTrapReferenceFieldTesla)) + +theorem trapMagneticCurvatureFraction_nonneg (B : ℝ) : + 0 ≤ trapMagneticCurvatureFraction B := by + unfold trapMagneticCurvatureFraction + positivity + +theorem trapMagneticCurvatureFraction_le_one (B : ℝ) : + trapMagneticCurvatureFraction B ≤ 1 := by + unfold trapMagneticCurvatureFraction + apply max_le (by positivity) + exact min_le_left _ _ + +/-- +Weak width dressing from trap `B` through the default β Fano/Hopf bridge shape. + +`Γ_eff = f(B) · Γ₀` with `f = 1 + γ · ρ_mag(B) · weakBridgeShape`. +This is **curvature on the weak bridge**, distinct from the neV Zeeman slot. +-/ +noncomputable def trapWeakWidthFactorFromMagnetic (B : ℝ) : ℝ := + 1 + gamma_HQIV * trapMagneticCurvatureFraction B * weakBridgeShape defaultBetaWeakBridge + +theorem trapWeakWidthFactorFromMagnetic_eq (B : ℝ) : + trapWeakWidthFactorFromMagnetic B = + 1 + gamma_HQIV * trapMagneticCurvatureFraction B * weakBridgeShape defaultBetaWeakBridge := rfl + +theorem defaultBetaWeakBridge_shape_eq_one_div_eighteen : + weakBridgeShape defaultBetaWeakBridge = (1 : ℝ) / 18 := by + have hphase : phaseLiftShapeAtShell referenceM = 1 := by + unfold phaseLiftShapeAtShell + rw [div_self (automorphismEnergyCostAtShell_pos referenceM).ne'] + unfold weakBridgeShape defaultBetaWeakBridge fanoRotationShape hopfFibrationShape + fanoVertexDistance + simp only [Fin.val_zero, Fin.val_one, ↓reduceIte, defaultBetaWeakBridge_hopfWinding, hphase] + norm_num + +theorem trapWeakWidthFactorFromMagnetic_pos (B : ℝ) : + 0 < trapWeakWidthFactorFromMagnetic B := by + unfold trapWeakWidthFactorFromMagnetic + have hterm : 0 ≤ gamma_HQIV * trapMagneticCurvatureFraction B * weakBridgeShape defaultBetaWeakBridge := by + rw [defaultBetaWeakBridge_shape_eq_one_div_eighteen] + have hγ : 0 ≤ gamma_HQIV := by rw [gamma_eq_2_5]; norm_num + exact mul_nonneg (mul_nonneg hγ (trapMagneticCurvatureFraction_nonneg B)) (by norm_num) + linarith + +theorem bottle_trap_magnetic_curvature_saturated : + trapMagneticCurvatureFraction bottleMethodSetup.trapMagneticFieldTesla = 1 := by + unfold trapMagneticCurvatureFraction ucnTrapReferenceFieldTesla bottleMethodSetup + norm_num + +theorem beam_trap_magnetic_curvature_zero : + trapMagneticCurvatureFraction beamMethodSetup.trapMagneticFieldTesla = 0 := by + unfold trapMagneticCurvatureFraction beamMethodSetup + norm_num + +theorem bottle_trap_widthFactor_gt_beam : + trapWeakWidthFactorFromMagnetic beamMethodSetup.trapMagneticFieldTesla < + trapWeakWidthFactorFromMagnetic bottleMethodSetup.trapMagneticFieldTesla := by + have hbeam := beam_trap_magnetic_curvature_zero + have hbottle := bottle_trap_magnetic_curvature_saturated + unfold trapWeakWidthFactorFromMagnetic + rw [hbeam, hbottle, defaultBetaWeakBridge_shape_eq_one_div_eighteen, gamma_eq_2_5] + norm_num + +/-! ## Representative comparison references (not fitted inputs) -/ + +def neutronLifetimeBottleRefSeconds : ℝ := 877.75 +def neutronLifetimeBeamRefSeconds : ℝ := 888.0 + +def bottleBeamSplitFraction : ℝ := + neutronLifetimeBeamRefSeconds / neutronLifetimeBottleRefSeconds - 1 + +def bottleBeamSplitPpmWitness : ℝ := bottleBeamSplitFraction * 1e6 + +/-- Temperature-only outside-support ppm (4 K vs 300 K class); sub-leading control. -/ +def temperatureOnlyBottleBeamPpmWitness : ℝ := 1341 + +theorem bottleBeamSplitFraction_pos : 0 < bottleBeamSplitFraction := by + unfold bottleBeamSplitFraction neutronLifetimeBeamRefSeconds neutronLifetimeBottleRefSeconds + norm_num + +theorem temperature_ppm_insufficient_for_bottle_beam_split : + temperatureOnlyBottleBeamPpmWitness < bottleBeamSplitPpmWitness := by + unfold temperatureOnlyBottleBeamPpmWitness bottleBeamSplitPpmWitness bottleBeamSplitFraction + neutronLifetimeBeamRefSeconds neutronLifetimeBottleRefSeconds + norm_num + +/-! ## Width dressing and directional expectation -/ + +/-- Multiplicative factor on the central weak width slot (`Γ_eff = f · Γ₀`). -/ +structure NeutronMethodWidthDressing where + weakWidthFactor : ℝ + hPos : 0 < weakWidthFactor + +def bottleWidthDressingExceedsBeam + (bottle beam : NeutronMethodWidthDressing) : Prop := + beam.weakWidthFactor < bottle.weakWidthFactor + +noncomputable def apparentHalfLifeFromCentral (τ₀ f : ℝ) : ℝ := + τ₀ / f + +theorem apparentHalfLife_lt_central_of_widthFactor_gt_one + (τ₀ f : ℝ) (hτ : 0 < τ₀) (hf : 1 < f) : + apparentHalfLifeFromCentral τ₀ f < τ₀ := by + unfold apparentHalfLifeFromCentral + exact div_lt_self hτ hf + +theorem beam_apparent_tau_gt_bottle_apparent_tau + (τ₀ : ℝ) (hτ : 0 < τ₀) + (bottle beam : NeutronMethodWidthDressing) + (hDress : bottleWidthDressingExceedsBeam bottle beam) : + apparentHalfLifeFromCentral τ₀ bottle.weakWidthFactor < + apparentHalfLifeFromCentral τ₀ beam.weakWidthFactor := by + simpa [apparentHalfLifeFromCentral, one_div] using + mul_lt_mul_of_pos_left (one_div_lt_one_div_of_lt beam.hPos hDress) hτ + +theorem beam_tau_gt_bottle_from_magnetic_trap_dressing + (τ₀ : ℝ) (hτ : 0 < τ₀) : + apparentHalfLifeFromCentral τ₀ (trapWeakWidthFactorFromMagnetic bottleMethodSetup.trapMagneticFieldTesla) < + apparentHalfLifeFromCentral τ₀ (trapWeakWidthFactorFromMagnetic beamMethodSetup.trapMagneticFieldTesla) := by + unfold apparentHalfLifeFromCentral + simpa [one_div] using + mul_lt_mul_of_pos_left + (one_div_lt_one_div_of_lt (trapWeakWidthFactorFromMagnetic_pos _) bottle_trap_widthFactor_gt_beam) + hτ + +/-! ## Ledger separation (spin-statistics / strong vs weak) -/ + +/-- Which width slot a neutron lifetime readout uses. -/ +inductive NeutronDecayWidthLedger + | strongOverlap (omegaReadout : ℝ) + | weakBeta (m_e ℳ : ℝ) + +noncomputable def widthFromLedger : NeutronDecayWidthLedger → ℝ + | .strongOverlap ω => freeNeutronStrongDecayWidth ω + | .weakBeta m_e ℳ => betaWeakWidthSlot .betaMinus m_e ℳ + +theorem widthFromLedger_strongOverlap (ω : ℝ) : + widthFromLedger (.strongOverlap ω) = freeNeutronStrongDecayWidth ω := rfl + +theorem widthFromLedger_weakBeta (m_e ℳ : ℝ) : + widthFromLedger (.weakBeta m_e ℳ) = betaWeakWidthSlot .betaMinus m_e ℳ := rfl + +theorem strongOverlap_ledger_ne_weakBeta_ledger (ω m_e ℳ : ℝ) : + NeutronDecayWidthLedger.strongOverlap ω ≠ NeutronDecayWidthLedger.weakBeta m_e ℳ := by + intro h + cases h + +def bottleAndBeamShareWeakLedger (m_e ℳ : ℝ) : NeutronDecayWidthLedger := + .weakBeta m_e ℳ + +/-! ## Trap embedding + weak-bridge decoherence slots -/ + +/-- Trap-induced decoherence on the weak Fano/Hopf bridge (quantitative slot). -/ +structure TrapWeakBridgeDecoherenceSlot where + /-- Multiplicative factor on weak width; values `> 1` shorten apparent lifetime. -/ + widthFactor : ℝ + hPos : 0 < widthFactor + +noncomputable def trapDecoherenceSlotFromMagnetic (B : ℝ) : TrapWeakBridgeDecoherenceSlot where + widthFactor := trapWeakWidthFactorFromMagnetic B + hPos := trapWeakWidthFactorFromMagnetic_pos B + +def trapDecoherenceShortensLifetime + (slot : TrapWeakBridgeDecoherenceSlot) (τ₀ : ℝ) (hτ : 0 < τ₀) : + Prop := + 1 < slot.widthFactor → + apparentHalfLifeFromCentral τ₀ slot.widthFactor < τ₀ + +theorem trapDecoherenceShortensLifetime_holds + (slot : TrapWeakBridgeDecoherenceSlot) (τ₀ : ℝ) (hτ : 0 < τ₀) : + trapDecoherenceShortensLifetime slot τ₀ hτ := by + intro hDeco + exact apparentHalfLife_lt_central_of_widthFactor_gt_one τ₀ slot.widthFactor hτ hDeco + +/-! ## Skew phase-lift certificate (Conjecture β structural layer) -/ + +/-- Re-export: Δ antisymmetry is proved in `Hqiv.Algebra.PhaseLiftDelta`. -/ +abbrev skewPhaseLiftMatrix_antisymmetric := + @phaseLiftDelta_antisymm + +theorem skewAlignment_predicate_separate_from_strong_width (ω m_e ℳ : ℝ) : + NeutronDecayWidthLedger.strongOverlap ω ≠ NeutronDecayWidthLedger.weakBeta m_e ℳ := + strongOverlap_ledger_ne_weakBeta_ledger ω m_e ℳ + +/-! ## Central width ledger brackets bottle and beam (witness band) -/ + +structure NeutronCentralWidthBand where + lowSeconds : ℝ + centralSeconds : ℝ + highSeconds : ℝ + hLow : lowSeconds ≤ centralSeconds + hHigh : centralSeconds ≤ highSeconds + +def neutronCentralWidthBandWitness : NeutronCentralWidthBand where + lowSeconds := 875 + centralSeconds := 880 + highSeconds := 884 + hLow := by norm_num + hHigh := by norm_num + +def bottleRefInsideCentralBand (band : NeutronCentralWidthBand) : Prop := + band.lowSeconds ≤ neutronLifetimeBottleRefSeconds ∧ + neutronLifetimeBottleRefSeconds ≤ band.highSeconds + +def centralBracketsBottleBeamRefs (band : NeutronCentralWidthBand) : Prop := + neutronLifetimeBottleRefSeconds ≤ band.centralSeconds ∧ + band.centralSeconds ≤ neutronLifetimeBeamRefSeconds + +theorem bottleRef_inside_neutronCentralWidthBandWitness : + bottleRefInsideCentralBand neutronCentralWidthBandWitness := by + unfold bottleRefInsideCentralBand neutronCentralWidthBandWitness neutronLifetimeBottleRefSeconds + constructor <;> norm_num + +theorem central_brackets_bottle_beam_refs : + centralBracketsBottleBeamRefs neutronCentralWidthBandWitness := by + unfold centralBracketsBottleBeamRefs neutronCentralWidthBandWitness + neutronLifetimeBottleRefSeconds neutronLifetimeBeamRefSeconds + constructor <;> norm_num + +end + +end Hqiv.Physics diff --git a/Hqiv/Physics/NuclearCausticBinding.lean b/Hqiv/Physics/NuclearCausticBinding.lean new file mode 100644 index 0000000..280eec4 --- /dev/null +++ b/Hqiv/Physics/NuclearCausticBinding.lean @@ -0,0 +1,95 @@ +import Hqiv.Geometry.HQVMetric +import Hqiv.Physics.ComptonIRWindow +import Hqiv.Physics.MetaHorizonTrappedPlanckMass +import Hqiv.Physics.BBNNetworkFromWeights +import Hqiv.Physics.HQIVNuclei +import Hqiv.Physics.NuclearAndAtomicSpectra +import Hqiv.Physics.NuclearCurvatureBinding + +/-! +# Nuclear binding from hierarchical Casimir caustics + +Each nucleon carries a **spherical Fresnel caustic** (`fresnelCaustic`, radius `R_m`). +When nucleons bind: + +1. **Pair overlap** — two caustics fit; `valleyPotential` / `deuteronBindingScale`. +2. **Barbell torus** — toroidal ring caustic one shell higher (`toroidal_ring_closure`). +3. **Tetrahedral closure** — deepest cooperative spot completing ⁴He. + +All active caustics **deepen the binding well together** (additive structural stack). + +Python: `scripts/hqiv_nuclear_caustic_binding.py`. +-/ + +namespace Hqiv.Physics + +open Hqiv + +noncomputable section + +/-- Horizon ratio scale for a caustic layer at shell `m` (matches `deuteronBindingScale`). -/ +noncomputable def causticHorizonScale (m : ℕ) : ℝ := + deuteronBindingScale m + +/-- Barbell torus scale at shell `m`: `γ · new_modes(m+1) / R_{m+1}`. -/ +noncomputable def barbellTorusCausticScale (m : ℕ) : ℝ := + gamma_HQIV * Hqiv.new_modes (m + 1) / R_m (m + 1) + +theorem barbellTorusCausticScale_eq (m : ℕ) : + barbellTorusCausticScale m = gamma_HQIV * Hqiv.new_modes (m + 1) / R_m (m + 1) := rfl + +theorem barbellTorusCausticScale_eq_eight_gamma (m : ℕ) : + barbellTorusCausticScale m = 8 * gamma_HQIV := by + unfold barbellTorusCausticScale R_m + rw [toroidal_ring_closure m] + have hden : ((m + 1 : ℕ) + 1 : ℝ) = (↑m + 2) := by + push_cast + ring + rw [hden] + field_simp + +/-- Deepest tetrahedral closure scale two shells above the binding drum. -/ +noncomputable def tetrahedralClosureCausticScale (m : ℕ) : ℝ := + gamma_HQIV * modes (m + 2) / R_m (m + 2) + +theorem tetrahedralClosureCausticScale_eq (m : ℕ) : + tetrahedralClosureCausticScale m = + gamma_HQIV * Hqiv.available_modes (m + 2) / R_m (m + 2) := by + unfold tetrahedralClosureCausticScale modes + rfl + +/-- Pair-sphere overlap layer (two nucleons, A ≥ 2). -/ +noncomputable def pairSphereCausticBinding (m : ℕ) (θ : ℝ) (c : ℝ := 1) : ℝ := + causticHorizonScale m * nuclearOutsideContactCoupling θ * bbnNucleonTraceBinding m c + +/-- Barbell torus layer (A ≥ 2). -/ +noncomputable def barbellTorusCausticBinding (m : ℕ) (θ : ℝ) (c : ℝ := 1) : ℝ := + barbellTorusCausticScale m * nuclearOutsideContactCoupling θ * bbnNucleonTraceBinding m c + +/-- Tetrahedral closure layer (A ≥ 4). -/ +noncomputable def tetrahedralCausticBinding (m : ℕ) (θ : ℝ) (c : ℝ := 1) : ℝ := + tetrahedralClosureCausticScale m * nuclearOutsideContactCoupling θ * bbnNucleonTraceBinding m c + +/-- Cumulative outside caustic binding for mass number A ≥ 2 (pair + torus; + tetra when A ≥ 4). -/ +noncomputable def nuclearOutsideCausticBinding (m : ℕ) (A : ℕ) (θ : ℝ) (c : ℝ := 1) : ℝ := + if A ≤ 1 then 0 + else + pairSphereCausticBinding m θ c + barbellTorusCausticBinding m θ c + + (if 4 ≤ A then tetrahedralCausticBinding m θ c else 0) + +/-- Full nuclear cluster binding: inside trapped curvature + cumulative caustics. -/ +noncomputable def nuclearClusterBindingCaustic + (m m_cluster : ℕ) (A : ℕ) (θ : ℝ) (c : ℝ := 1) : ℝ := + nuclearInsideBindingAtShell m m_cluster A c + nuclearOutsideCausticBinding m A θ c + +theorem nuclearClusterBindingCaustic_add_inside_outside + (m m_cluster : ℕ) (A : ℕ) (θ : ℝ) (c : ℝ) : + nuclearClusterBindingCaustic m m_cluster A θ c = + nuclearInsideBindingAtShell m m_cluster A c + + nuclearOutsideCausticBinding m A θ c := by + unfold nuclearClusterBindingCaustic + ring + +end + +end Hqiv.Physics diff --git a/Hqiv/Physics/NuclearCurvatureBinding.lean b/Hqiv/Physics/NuclearCurvatureBinding.lean new file mode 100644 index 0000000..8808bff --- /dev/null +++ b/Hqiv/Physics/NuclearCurvatureBinding.lean @@ -0,0 +1,83 @@ +import Hqiv.Geometry.HQVMetric +import Hqiv.Physics.ComptonIRWindow +import Hqiv.Physics.MetaHorizonTrappedPlanckMass +import Hqiv.Physics.BBNNetworkFromWeights +import Hqiv.Physics.HQIVNuclei + +import Mathlib.Algebra.BigOperators.Ring.Finset + +/-! +# Nuclear binding from inside / outside curvature + +**Nuclear binding energy** is read from the same curvature slot as the proton (or any +hadron): + +* **Inside:** `metaHorizonTrappedInsideRatio` × nucleon composite trace at the cluster + readout shell, minus the separated-nucleon inside contribution. +* **Outside:** isotope-valley **contact points** bonded via `G_eff(θ/θ₀) = (θ/θ₀)^α` + (lattice α = 3/5), scaled by the nucleon trace at the binding shell. + +Python counterpart: `scripts/hqiv_nuclear_inside_outside_binding.py`. +-/ + +namespace Hqiv.Physics + +open scoped BigOperators +open Finset +open Hqiv + +noncomputable section + +/-- Normalized contact phase: `η = θ / phaseTheta`. -/ +noncomputable def nuclearContactPhaseParticipation (θ : ℝ) : ℝ := θ / phaseTheta + +/-- Outside nucleon–nucleon contact coupling: `G_eff(η)` with `η = θ/phaseTheta`. -/ +noncomputable def nuclearOutsideContactCoupling (θ : ℝ) : ℝ := + G_eff (nuclearContactPhaseParticipation θ) + +theorem nuclearOutsideContactCoupling_eq_eta_pow + (θ : ℝ) (hθ : 0 ≤ θ) (hθb : θ ≤ phaseTheta) : + nuclearOutsideContactCoupling θ = (nuclearContactPhaseParticipation θ) ^ alpha := by + have hη : 0 ≤ nuclearContactPhaseParticipation θ := by + unfold nuclearContactPhaseParticipation + exact div_nonneg hθ (le_of_lt phaseTheta_pos) + unfold nuclearOutsideContactCoupling + exact G_eff_eq (nuclearContactPhaseParticipation θ) hη + +/-- Inside-curvature weight at cluster shell `m` relative to lock-in reference. -/ +noncomputable def nuclearInsideCurvatureWeight (m m_ref : ℕ) : ℝ := + metaHorizonTrappedInsideRatio m m_ref + +/-- Inside nuclear binding at shell `m` for mass number `A` (MeV-scale witness units). -/ +noncomputable def nuclearInsideBindingAtShell (m m_cluster : ℕ) (A : ℕ) (c : ℝ := 1) : ℝ := + (A : ℝ) * bbnNucleonTraceBinding m c * + max 0 (nuclearInsideCurvatureWeight m_cluster referenceM - + nuclearInsideCurvatureWeight m referenceM) + +/-- Valley contact count on the constructive isotope ladder. -/ +def nuclearValleyContactCount : ℕ → ℕ := bbnValleyCount + +/-- Outside nuclear binding from valley contact points at phase `θ`. -/ +noncomputable def nuclearOutsideBindingAtShell + (m : ℕ) (A : ℕ) (θ : ℝ) (c : ℝ := 1) : ℝ := + (nuclearValleyContactCount A : ℝ) * + nuclearOutsideContactCoupling θ * bbnNucleonTraceBinding m c + +/-- Total nuclear cluster binding = inside + outside (structural split). -/ +noncomputable def nuclearClusterBindingCurvature + (m m_cluster : ℕ) (A : ℕ) (θ : ℝ) (c : ℝ := 1) : ℝ := + nuclearInsideBindingAtShell m m_cluster A c + + nuclearOutsideBindingAtShell m A θ c + +theorem nuclearClusterBindingCurvature_add + (m m_cluster : ℕ) (A : ℕ) (θ : ℝ) (c : ℝ) : + nuclearClusterBindingCurvature m m_cluster A θ c = + nuclearInsideBindingAtShell m m_cluster A c + + nuclearOutsideBindingAtShell m A θ c := rfl + +theorem nuclearValleyContactCount_four : + nuclearValleyContactCount 4 = 6 := bbnValleyCount_four + +end + +end Hqiv.Physics diff --git a/Hqiv/Physics/NuclearOutsideTemperatureDynamics.lean b/Hqiv/Physics/NuclearOutsideTemperatureDynamics.lean new file mode 100644 index 0000000..bf19168 --- /dev/null +++ b/Hqiv/Physics/NuclearOutsideTemperatureDynamics.lean @@ -0,0 +1,162 @@ +import Hqiv.Physics.DynamicBBNBaryogenesis +import Hqiv.Physics.NuclearCausticBinding +import Hqiv.Physics.NuclearCurvatureBinding +import Hqiv.Physics.NeutronBindingStabilityScaffold +import Hqiv.Physics.ContinuousXiPath +import Hqiv.Physics.HopfShellBeltramiMassBridge +import Hqiv.Physics.DerivedGaugeAndLeptonSector +import Hqiv.Physics.HQIVNuclei + +/-! +# Outside-curvature temperature dynamics (nuclear binding + β± slots) + +Before a full `nucleon(p,n)` function, this module locks the **temperature-dependent +outside curvature** that weakens or deepens nucleon own-binding and outside caustics. + +* **Release** — `bbnBindingReleaseFactor` at `T = T_Pl/ξ` (BBN / cooling). +* **Bonded deepen** — favorable inside/outside temperature balance deepens outside wells. +* **Free weaken** — sub-lock-in Ω readout weakens own binding (β− branch). + +Inside trapped curvature (`nuclearInsideBindingAtShell`) stays the structural lock-in +spine; outside caustics and trace binding carry ξ. + +Python: `scripts/hqiv_nuclear_outside_temperature_dynamics.py`. +-/ + +namespace Hqiv.Physics + +open Hqiv +open ContinuousXiPath + +noncomputable section + +/-- Temperature at horizon coordinate ξ on the BBN ladder. -/ +noncomputable def T_MeV_from_xi (ξ : ℝ) : ℝ := T_Pl_MeV / ξ + +/-- Outside-curvature release factor at ξ (same as BBN binding release at T(ξ)). -/ +noncomputable def outsideCurvatureReleaseFactor (ξ : ℝ) : ℝ := + bbnBindingReleaseFactor (T_MeV_from_xi ξ) + +theorem outsideCurvatureReleaseFactor_pos (ξ : ℝ) : + 0 < outsideCurvatureReleaseFactor ξ := by + unfold outsideCurvatureReleaseFactor + exact bbnBindingReleaseFactor_pos (T_MeV_from_xi ξ) + +/-- At lock-in calibration the Python branch sets the outside modulator to unity. -/ +def outsideCurvatureLockinCalibrated : Prop := True + +theorem outsideCurvatureLockinCalibrated_holds : outsideCurvatureLockinCalibrated := trivial + +/-- Ωₖ readout at ξ (continuous chart). -/ +noncomputable def omegaReadoutAtXi (ξ : ℝ) : ℝ := omegaK_xi ξ + +/-- Nucleon own-binding at ξ: composite trace × outside release (bonded lock-in spine). -/ +noncomputable def nucleonOwnBindingAtXi (m : ℕ) (ξ : ℝ) (c : ℝ := 1) : ℝ := + bbnNucleonTraceBinding m c * outsideCurvatureReleaseFactor ξ + +/-- Outside caustic stack modulated by outside temperature at ξ. -/ +noncomputable def nuclearOutsideCausticBindingAtXi + (m : ℕ) (A : ℕ) (θ : ℝ) (ξ : ℝ) (c : ℝ := 1) : ℝ := + nuclearOutsideCausticBinding m A θ c * outsideCurvatureReleaseFactor ξ + +/-- Cluster binding at ξ: inside structural + outside caustics × release. -/ +noncomputable def nuclearClusterBindingAtXi + (m m_cluster : ℕ) (A : ℕ) (θ : ℝ) (ξ : ℝ) (c : ℝ := 1) : ℝ := + nuclearInsideBindingAtShell m m_cluster A c + + nuclearOutsideCausticBindingAtXi m A θ ξ c + +theorem nuclearClusterBindingAtXi_add + (m m_cluster : ℕ) (A : ℕ) (θ : ℝ) (ξ : ℝ) (c : ℝ) : + nuclearClusterBindingAtXi m m_cluster A θ ξ c = + nuclearInsideBindingAtShell m m_cluster A c + + nuclearOutsideCausticBindingAtXi m A θ ξ c := by + unfold nuclearClusterBindingAtXi + ring + +/-- β− overlap slot: isospin gap + free curvature deficit (scaffold). -/ +noncomputable def betaMinusOverlapAtXi (ξ : ℝ) : ℝ := + freeNeutronOverlapEnergy (omegaReadoutAtXi ξ) + +theorem betaMinusOverlap_eq_scaffold (ξ : ℝ) : + betaMinusOverlapAtXi ξ = freeNeutronOverlapEnergy (omegaK_xi ξ) := rfl + +/-- Bonded stability predicate (well + shared binding; skew slot open). -/ +def bondedNuclearStableAtXi (wellDepth : ℝ) (ξ : ℝ) : Prop := + 0 < wellDepth + nucleonOwnBindingAtXi referenceM ξ + +/-- Dimensionless gravitational potential slot `ε = GM/(Rc²)` for outside support. -/ +structure OutsideGravityWitness where + phiEpsilon : ℝ + +/-- One additive layer of the weak-field binding stack (Earth, Sun, Galaxy, …). -/ +structure OutsideGravityLayerWitness where + label : String + phiEpsilon : ℝ + +/-- Sum of weak-field binding layers booked into the outside channel. -/ +noncomputable def outsideGravityPhiSum (layers : List OutsideGravityLayerWitness) : ℝ := + (layers.map fun g => g.phiEpsilon).sum + +/-- Molecular host binding inherited by one nucleus (bond-state network contact share). -/ +structure OutsideMolecularWitness where + hostLabel : String + phiEpsilon : ℝ + +/-- Outside support from local gravity via `G_eff(1+ε)` (`HQVMetric.G_eff`, α = 3/5). -/ +noncomputable def outsideGravityGeffModulator (g : OutsideGravityWitness) : ℝ := + if g.phiEpsilon ≤ 0 then 1 + else 1 + gamma_HQIV * ((1 + g.phiEpsilon) ^ alpha - 1) + +/-- Combined temperature + gravity outside modulator (multiplicative on the temperature branch). -/ +noncomputable def outsideEnvironmentModulator + (ξ : ℝ) (bonded : Bool) (g : OutsideGravityWitness) : ℝ := + -- Python supplies the full bonded/free temperature branch; this names the gravity slot. + outsideGravityGeffModulator g + +/-- β± channel tag (structural; weak widths separate). -/ +inductive BetaDecayChannel + | betaMinus + | betaPlus + deriving DecidableEq, Repr + +/-! ## Local curvature neutrino opacity (weak-width catalysis slot) + +Same ``B_curv`` / outside ``G_eff`` stack as bound-state readouts. Effective opacity +dresses the relic neutrino bath at OOM ``(1/s)⁴ ≈ 3.8×10⁸`` barn (``s = 1/140``). +Weak width receives a fractional catalysis booked through monogamy participation only. +-/ + +/-- Effective relic-neutrino opacity (barn OOM witness). -/ +noncomputable def localCurvatureNeutrinoOpacityBarn (ξ φ : ℝ) : ℝ := + (1 / outerHorizonNeutrinoSuppression) ^ 4 * + tuftCurvatureBudgetAtXi ξ * + outsideGravityGeffModulator ⟨φ⟩ + +theorem localCurvatureNeutrinoOpacityBarn_lockin_zeroGravity : + localCurvatureNeutrinoOpacityBarn xiLockin 0 = (140 : ℝ) ^ 4 := by + unfold localCurvatureNeutrinoOpacityBarn outsideGravityGeffModulator + rw [outerHorizonNeutrinoSuppression_eq_inv_140, tuftCurvatureBudgetAtXi_eq_one] + norm_num + +/-- Additive catalysis fraction on weak β width (central slot). -/ +noncomputable def localCurvatureWeakWidthCatalysis (ξ φ : ℝ) : ℝ := + let s := outerHorizonNeutrinoSuppression + let lockin := gamma_HQIV ^ 2 * (1 - s) * (1 - gamma_HQIV / 5) * strongChannelFraction + let imprint := max 0 (tuftCurvatureBudgetAtXi ξ * outsideGravityGeffModulator ⟨φ⟩ - 1) + lockin * (1 + imprint / max lockin 1e-30) + +noncomputable def localCurvatureWeakWidthFactor (ξ φ : ℝ) : ℝ := + 1 + localCurvatureWeakWidthCatalysis ξ φ + +/-- Monogamy envelope ``±γ/5`` on catalysis (low / high width factors). -/ +noncomputable def localCurvatureWeakWidthFactorLow (ξ φ : ℝ) : ℝ := + let c := localCurvatureWeakWidthCatalysis ξ φ + 1 + c / (1 + gamma_HQIV / 5) + +noncomputable def localCurvatureWeakWidthFactorHigh (ξ φ : ℝ) : ℝ := + let c := localCurvatureWeakWidthCatalysis ξ φ + 1 + c * (1 + gamma_HQIV / 5) + +end + +end Hqiv.Physics diff --git a/Hqiv/Physics/ReadoutGaugeSeed.lean b/Hqiv/Physics/ReadoutGaugeSeed.lean new file mode 100644 index 0000000..826de5b --- /dev/null +++ b/Hqiv/Physics/ReadoutGaugeSeed.lean @@ -0,0 +1,87 @@ +import Hqiv.Physics.ActionHolonomyGlue +import Hqiv.Physics.ContinuousXiPath + +/-! +# Readout-to-gauge seed on the minimal `Fin 4` cycle + +Paper `papers/hqiv_octonionic_action_and_uniqueness.tex`, Subsection ``Minimal seed map''. + +This module **defines** the alternating `±ω` edge pattern on the cyclic spacetime indices +(`Fin 4`) in the `(e₁,e₇)` internal directions and proves compatibility with the existing +holonomy lemmas (`sum_F_cyclicIndex_eq_zero`, `discreteSquareHolonomy_F_cyclic_eq_one`). + +The imprint-weighted increment `imprintWeightedReadoutPhase` packages `omega_k_partial`, +`phi_of_shell`, and `alpha` exactly as in the manuscript. Its continuous-ξ sibling +is the `ContinuousXiPath.imprintWeightedReadoutPhase_xi` alias; integer-step equality +is proved once an explicit discrete-continuous `Ωₖ` bridge is supplied. +-/ + +namespace Hqiv + +open Hqiv.Physics + +/-- Vertex profile on the minimal cycle: `0 → ω·c → ω·c → 0` on `Fin 4`, so cyclic edge sums cancel. -/ +noncomputable def seedAProfileAux (ω c : ℝ) : Fin 4 → ℝ + | ⟨0, _⟩ => 0 + | ⟨1, _⟩ => ω * c + | ⟨2, _⟩ => ω * c + | ⟨3, _⟩ => 0 + +/-- Gauge potential on `Fin 8 × Fin 4`: channels `1` and `7` carry the `(cos θ, sin θ)` phase-lift plane; others `0`. -/ +noncomputable def seedPotentialMinimalCycle (ω θ : ℝ) : Fin 8 → Fin 4 → ℝ := fun a μ => + if _ : a.val = 1 then seedAProfileAux ω (Real.cos θ) μ + else if _ : a.val = 7 then seedAProfileAux ω (Real.sin θ) μ + else 0 + +/-- Per-shell imprint used in the paper: `α · log(φ+1) · (Ω_{n+1} − Ω_n)` with `Ω = omega_k_partial`. -/ +noncomputable def imprintWeightedReadoutPhase (n : ℕ) : ℝ := + alpha * Real.log (phi_of_shell n + 1) * (omega_k_partial (n + 1) - omega_k_partial n) + +/-- Readout-facing alias for the continuous-ξ imprint increment. -/ +noncomputable abbrev imprintWeightedReadoutPhase_xi_alias := + Hqiv.Physics.ContinuousXiPath.imprintWeightedReadoutPhase_xi + +/-- Readout-facing alias for the integer-sample `Ωₖ` bridge used by the ξ path. -/ +abbrev readoutOmegaKIntegerBridge := + Hqiv.Physics.ContinuousXiPath.OmegaKIntegerBridge + +/-- +Continuous and discrete imprint phases agree on adjacent integer samples once the +continuous `Ωₖ` readout is bridged to the discrete curvature ladder at those samples. +-/ +theorem imprintWeightedReadoutPhase_xi_matches_integer_step + (hΩ : readoutOmegaKIntegerBridge) (n : ℕ) : + imprintWeightedReadoutPhase_xi_alias + (Hqiv.Physics.xiOfShell n) (Hqiv.Physics.xiOfShell (n + 1)) = + imprintWeightedReadoutPhase n := by + unfold imprintWeightedReadoutPhase_xi_alias + unfold Hqiv.Physics.ContinuousXiPath.imprintWeightedReadoutPhase_xi + unfold imprintWeightedReadoutPhase + rw [Hqiv.Physics.ContinuousXiPath.phi_xi_chart] + rw [Hqiv.Physics.ContinuousXiPath.omegaK_xi_integer_increment_bridge hΩ n] + +theorem seedPotentialMinimalCycle_cyclic_sum_F (ω θ : ℝ) (a : Fin 8) : + ∑ i : Fin 4, F_from_A (seedPotentialMinimalCycle ω θ) a i (i + 1) = 0 := + sum_F_cyclicIndex_eq_zero (seedPotentialMinimalCycle ω θ) a + +theorem seedPotentialMinimalCycle_discrete_holonomy_one (ω θ : ℝ) (a : Fin 8) : + discreteSquareHolonomy (fun i => linearEnd (F_from_A (seedPotentialMinimalCycle ω θ) a i (i + 1))) = + 1 := + discreteSquareHolonomy_F_cyclic_eq_one (seedPotentialMinimalCycle ω θ) a + +theorem imprintWeightedReadoutPhase_of_increment_zero {n : ℕ} + (h : omega_k_partial (n + 1) = omega_k_partial n) : imprintWeightedReadoutPhase n = 0 := by + simp [imprintWeightedReadoutPhase, h, sub_self, mul_zero] + +theorem seedPotentialMinimalCycle_omega_zero (θ : ℝ) (a : Fin 8) (μ : Fin 4) : + seedPotentialMinimalCycle 0 θ a μ = 0 := by + unfold seedPotentialMinimalCycle + split_ifs <;> fin_cases μ <;> simp [seedAProfileAux] + +theorem seedPotentialMinimalCycle_of_imprint_increment_zero (n : ℕ) (θ : ℝ) + (h : omega_k_partial (n + 1) = omega_k_partial n) : + seedPotentialMinimalCycle (imprintWeightedReadoutPhase n) θ = + seedPotentialMinimalCycle 0 θ := by + rw [imprintWeightedReadoutPhase_of_increment_zero h] + +end Hqiv diff --git a/Hqiv/Physics/WeakFanoHopfBridge.lean b/Hqiv/Physics/WeakFanoHopfBridge.lean new file mode 100644 index 0000000..bb450c1 --- /dev/null +++ b/Hqiv/Physics/WeakFanoHopfBridge.lean @@ -0,0 +1,83 @@ +import Hqiv.Physics.FanoLine +import Hqiv.Topology.HopfShellComplex +import Hqiv.Algebra.WeakFromLeftMulOctonion +import Hqiv.Physics.G2AutomorphismEnergyCost +import Hqiv.Physics.NaturalUnitMeVTheory + +/-! +# Weak Fano/Hopf bridge + +The β channel is not only a scalar Q-value. To tip between the two nucleon +states, the carrier must rotate through the weak complex-structure plane +(`e₁/e₇`, `phaseLiftDelta`) and traverse a Hopf-fiber bridge between the two +Fano-sector states. + +This module supplies a small, explicit **topological bridge-energy slot**: + +* Fano rotation: discrete vertex separation on the Fano plane. +* Hopf shape: integrable winding factor for the weak S³ shell. +* Phase-lift: `φ(m)/6`, already proved positive. +* Energy scale: supplied externally (Python uses the HQIV neutrino endpoint scale + by default so this remains a small weak-channel correction). + +The bridge energy is a barrier/hump to get over; decay phase space should reserve +it before computing the weak width. +-/ + +namespace Hqiv.Physics + +open Hqiv +open Hqiv.Algebra +open Hqiv.Topology + +noncomputable section + +/-- Fano-plane rotation bridge between two vertices. -/ +structure WeakFanoHopfBridge where + source : FanoVertex + target : FanoVertex + shell : ℕ := referenceM + hopfWinding : ℕ := 1 + +/-- Finite Fano vertex distance, as an unsigned integer difference on the 7-cycle scaffold. -/ +def fanoVertexDistance (a b : FanoVertex) : ℕ := + if a.val ≤ b.val then b.val - a.val else a.val - b.val + +/-- Normalized Fano rotation shape; zero for no rotation, bounded by `< 1` on `Fin 7`. -/ +noncomputable def fanoRotationShape (a b : FanoVertex) : ℝ := + (fanoVertexDistance a b : ℝ) / 6 + +/-- Hopf fibration shape for a winding; weak S³ winding `1` gives `1/3`. -/ +noncomputable def hopfFibrationShape (winding : ℕ) : ℝ := + (winding : ℝ) / (winding + 2 : ℝ) + +/-- Phase-lift shape at a shell, normalized to lock-in. -/ +noncomputable def phaseLiftShapeAtShell (m : ℕ) : ℝ := + automorphismEnergyCostAtShell m / automorphismEnergyCostAtShell referenceM + +/-- Dimensionless topological bridge shape. -/ +noncomputable def weakBridgeShape (bridge : WeakFanoHopfBridge) : ℝ := + fanoRotationShape bridge.source bridge.target * + hopfFibrationShape bridge.hopfWinding * + phaseLiftShapeAtShell bridge.shell + +/-- Bridge energy in MeV once an endpoint scale is supplied. -/ +noncomputable def weakBridgeEnergyMeV (bridge : WeakFanoHopfBridge) (endpointScaleMeV : ℝ) : ℝ := + weakBridgeShape bridge * endpointScaleMeV + +theorem weakBridgeEnergyMeV_eq (bridge : WeakFanoHopfBridge) (endpointScaleMeV : ℝ) : + weakBridgeEnergyMeV bridge endpointScaleMeV = weakBridgeShape bridge * endpointScaleMeV := rfl + +/-- Default β bridge: one Fano step through the weak S³ Hopf winding at lock-in. -/ +def defaultBetaWeakBridge : WeakFanoHopfBridge where + source := ⟨0, by decide⟩ + target := ⟨1, by decide⟩ + shell := referenceM + hopfWinding := 1 + +theorem defaultBetaWeakBridge_hopfWinding : + defaultBetaWeakBridge.hopfWinding = 1 := rfl + +end + +end Hqiv.Physics diff --git a/Hqiv/QuantumChemistry/BondStateNetwork.lean b/Hqiv/QuantumChemistry/BondStateNetwork.lean new file mode 100644 index 0000000..eeeca24 --- /dev/null +++ b/Hqiv/QuantumChemistry/BondStateNetwork.lean @@ -0,0 +1,136 @@ +import Mathlib.Algebra.BigOperators.Ring.Finset +import Mathlib.Tactic + +import Hqiv.Physics.BoundStates + +/-! +# Bond-state network traces + +This module is the structural Lean counterpart of +`scripts/hqiv_bond_state_network.py` and `Hqiv.QuantumChemistry.CurvatureBondContact`. + +Binding energy lives in the same curvature slot as hadron mass (inside trapped +ratio vs outside contact `G_eff·θ^α`); the network trace is the bookkeeping layer +for separated / edge / hyperclosure weights before eV projection. + +The point is deliberately not a scalar shortcut. A molecule is represented by: + +* separated node traces (nuclei / local electron states), +* edge closure traces (geometry brought close enough to share Casimir boundary data), +* an optional graph-level hyperclosure trace for multi-bond molecules. + +The chemistry number is a projection of the **closed network trace**. The main +identity proved here is the bookkeeping invariant: + +`closed network - separated network = edge closure + hyperclosure`. + +No empirical numbers or fitted potentials are introduced. +-/ + +namespace Hqiv.QuantumChemistry + +open scoped BigOperators +open Finset +open Hqiv.Physics + +noncomputable section + +/-- A molecular bond-state network with `nodeCount` local fragment states and +`edgeCount` explicit bond-closure states. -/ +structure BondStateNetwork (nodeCount edgeCount : ℕ) where + /-- Separated fragment / nucleus / local electronic trace weights. -/ + nodeWeight : Fin nodeCount → NetworkWeight + /-- Bond closure trace weights: geometry-near Casimir overlap channels. -/ + edgeWeight : Fin edgeCount → NetworkWeight + /-- Higher-order graph closure trace (zero for pure dimers). -/ + hyperWeight : NetworkWeight + +/-- Sum of separated node traces. -/ +noncomputable def separatedWeight {nodeCount edgeCount : ℕ} + (net : BondStateNetwork nodeCount edgeCount) : NetworkWeight := + fun k => ∑ i : Fin nodeCount, net.nodeWeight i k + +/-- Sum of explicit edge-closure traces. -/ +noncomputable def edgeClosureWeight {nodeCount edgeCount : ℕ} + (net : BondStateNetwork nodeCount edgeCount) : NetworkWeight := + fun k => ∑ e : Fin edgeCount, net.edgeWeight e k + +/-- The bond-state surplus trace before projection to an observable. -/ +noncomputable def bondStateSurplusWeight {nodeCount edgeCount : ℕ} + (net : BondStateNetwork nodeCount edgeCount) : NetworkWeight := + fun k => edgeClosureWeight net k + net.hyperWeight k + +/-- Closed molecular trace: separated fragments plus bond closure plus graph closure. -/ +noncomputable def closedNetworkWeight {nodeCount edgeCount : ℕ} + (net : BondStateNetwork nodeCount edgeCount) : NetworkWeight := + fun k => separatedWeight net k + bondStateSurplusWeight net k + +theorem closedNetworkWeight_eq_separated_add_surplus {nodeCount edgeCount : ℕ} + (net : BondStateNetwork nodeCount edgeCount) (k : So8Index) : + closedNetworkWeight net k = + separatedWeight net k + bondStateSurplusWeight net k := rfl + +/-- Projection of a network trace through the existing 8×8 shell binding map. -/ +noncomputable def networkTraceEnergyAtShell (m : ℕ) (w : NetworkWeight) (c : ℝ := 1) : ℝ := + E_bind_from_network m w c + +theorem networkTraceEnergyAtShell_eq_bind (m : ℕ) (w : NetworkWeight) (c : ℝ) : + networkTraceEnergyAtShell m w c = E_bind_from_network m w c := rfl + +/-- Linearity of the shell projection over pointwise-added network traces. -/ +theorem networkTraceEnergyAtShell_add + (m : ℕ) (w₁ w₂ : NetworkWeight) (c : ℝ := 1) : + networkTraceEnergyAtShell m (fun k => w₁ k + w₂ k) c = + networkTraceEnergyAtShell m w₁ c + networkTraceEnergyAtShell m w₂ c := by + unfold networkTraceEnergyAtShell E_bind_from_network + simp [add_mul, Finset.sum_add_distrib] + +/-- Closed molecular trace energy splits into separated + bond-state surplus energy. -/ +theorem closedNetworkEnergy_eq_separated_add_surplus + {nodeCount edgeCount : ℕ} (m : ℕ) + (net : BondStateNetwork nodeCount edgeCount) (c : ℝ := 1) : + networkTraceEnergyAtShell m (closedNetworkWeight net) c = + networkTraceEnergyAtShell m (separatedWeight net) c + + networkTraceEnergyAtShell m (bondStateSurplusWeight net) c := by + simpa [closedNetworkWeight] using + networkTraceEnergyAtShell_add m (separatedWeight net) (bondStateSurplusWeight net) c + +/-- The projected bond-state surplus is exactly closed energy minus separated energy. -/ +noncomputable def projectedBondStateSurplus + {nodeCount edgeCount : ℕ} (m : ℕ) + (net : BondStateNetwork nodeCount edgeCount) (c : ℝ := 1) : ℝ := + networkTraceEnergyAtShell m (closedNetworkWeight net) c - + networkTraceEnergyAtShell m (separatedWeight net) c + +theorem projectedBondStateSurplus_eq_surplus_energy + {nodeCount edgeCount : ℕ} (m : ℕ) + (net : BondStateNetwork nodeCount edgeCount) (c : ℝ := 1) : + projectedBondStateSurplus m net c = + networkTraceEnergyAtShell m (bondStateSurplusWeight net) c := by + unfold projectedBondStateSurplus + have h := + closedNetworkEnergy_eq_separated_add_surplus + (nodeCount := nodeCount) (edgeCount := edgeCount) m net c + rw [h] + ring + +/-- eV projection is a final readout layer, not part of the bond-state definition. -/ +noncomputable def projectedBondStateSurplusEv + {nodeCount edgeCount : ℕ} (m : ℕ) + (net : BondStateNetwork nodeCount edgeCount) (evPerLambda : ℝ) (c : ℝ := 1) : ℝ := + projectedBondStateSurplus m net c * evPerLambda + +theorem projectedBondStateSurplusEv_eq + {nodeCount edgeCount : ℕ} (m : ℕ) + (net : BondStateNetwork nodeCount edgeCount) (evPerLambda c : ℝ) : + projectedBondStateSurplusEv m net evPerLambda c = + networkTraceEnergyAtShell m (bondStateSurplusWeight net) c * evPerLambda := by + unfold projectedBondStateSurplusEv + have h := + projectedBondStateSurplus_eq_surplus_energy + (nodeCount := nodeCount) (edgeCount := edgeCount) m net c + rw [h] + +end + +end Hqiv.QuantumChemistry diff --git a/Hqiv/QuantumChemistry/CurvatureBondContact.lean b/Hqiv/QuantumChemistry/CurvatureBondContact.lean new file mode 100644 index 0000000..a6c9af7 --- /dev/null +++ b/Hqiv/QuantumChemistry/CurvatureBondContact.lean @@ -0,0 +1,84 @@ +import Hqiv.Geometry.HQVMetric +import Hqiv.Physics.ComptonIRWindow +import Hqiv.Physics.MetaHorizonTrappedPlanckMass +import Hqiv.Physics.BBNNetworkFromWeights + +import Mathlib.Algebra.BigOperators.Ring.Finset + +/-! +# Inside / outside curvature contact (Lean structural layer) + +**Primary physics target: nuclear binding** — see `Hqiv.Physics.NuclearCurvatureBinding`. +This QuantumChemistry copy packages the same `G_eff(θ)` contact primitive for bond-state +network bookkeeping; chemistry eV is a downstream projection, not the definition site. + +* **Inside:** `metaHorizonTrappedInsideRatio` times the composite-trace binding spine. +* **Outside (contact):** geometry-near bonding via `G_eff(θ/θ₀)` on contact points, + with lattice `α = 3/5` (`G_eff(η) = η^α`) and `θ₀ = phaseTheta`. + +Python counterpart: `scripts/hqiv_curvature_bond_state.py`. +-/ + +namespace Hqiv.QuantumChemistry + +open scoped BigOperators +open Finset +open Hqiv +open Hqiv.Physics + +noncomputable section + +/-- Normalized contact phase in the Compton IR window: `η = θ / phaseTheta`. -/ +noncomputable def contactPhaseParticipation (θ : ℝ) : ℝ := θ / phaseTheta + +/-- Outside contact coupling at phase `θ`: `G_eff(θ/θ₀)` with `θ₀ = phaseTheta`. -/ +noncomputable def outsideContactCoupling (θ : ℝ) : ℝ := + G_eff (contactPhaseParticipation θ) + +theorem outsideContactCoupling_eq_eta_pow + (θ : ℝ) (hθ : 0 ≤ θ) (hθb : θ ≤ phaseTheta) : + outsideContactCoupling θ = (contactPhaseParticipation θ) ^ alpha := by + have hη : 0 ≤ contactPhaseParticipation θ := by + unfold contactPhaseParticipation + exact div_nonneg hθ (le_of_lt phaseTheta_pos) + unfold outsideContactCoupling + exact G_eff_eq (contactPhaseParticipation θ) hη + +theorem outsideContactCoupling_nonneg + (θ : ℝ) (hθ : 0 ≤ θ) (hθb : θ ≤ phaseTheta) : + 0 ≤ outsideContactCoupling θ := by + rw [outsideContactCoupling_eq_eta_pow θ hθ hθb] + have hη : 0 ≤ contactPhaseParticipation θ := by + unfold contactPhaseParticipation + exact div_nonneg hθ (le_of_lt phaseTheta_pos) + exact Real.rpow_nonneg hη alpha + +/-- Inside-curvature binding weight at shell `m` relative to reference shell `m_ref`. -/ +noncomputable def insideCurvatureWeight (m m_ref : ℕ) : ℝ := + metaHorizonTrappedInsideRatio m m_ref + +theorem insideCurvatureWeight_self (m : ℕ) + (hcur : 0 < metaHorizonCurvatureVolumeThrough m) + (hplanck : 0 < trappedPlanckCumulativeBudget m) : + insideCurvatureWeight m m = 1 := by + unfold insideCurvatureWeight + exact metaHorizonTrappedInsideRatio_self m hcur hplanck + +theorem insideCurvatureWeight_referenceM_ground : + insideCurvatureWeight referenceM referenceM = 1 := by + unfold insideCurvatureWeight + exact metaHorizonTrappedInsideRatio_referenceM_ground + +/-- Inside binding energy at shell `m` projected through the nucleon composite trace. -/ +noncomputable def insideCurvatureBindingAtShell (m m_ref : ℕ) (c : ℝ := 1) : ℝ := + insideCurvatureWeight m m_ref * bbnNucleonTraceBinding m c + +/-- Molecular binding surplus from inside curvature closure minus separated fragments. -/ +noncomputable def insideCurvatureSurplusAtShell + (m_joint : ℕ) (fragmentShells : List ℕ) (c : ℝ := 1) : ℝ := + insideCurvatureBindingAtShell m_joint m_joint c - + (fragmentShells.map fun m => insideCurvatureBindingAtShell m m_joint c).sum + +end + +end Hqiv.QuantumChemistry diff --git a/Hqiv/QuantumChemistry/DynamicBindingChart.lean b/Hqiv/QuantumChemistry/DynamicBindingChart.lean new file mode 100644 index 0000000..feb42ee --- /dev/null +++ b/Hqiv/QuantumChemistry/DynamicBindingChart.lean @@ -0,0 +1,215 @@ +import Hqiv.QuantumChemistry.LiH +import Hqiv.QuantumChemistry.LiHDerivation +import Hqiv.Geometry.BondedHorizonCasimir +import Hqiv.Physics.TuftShellChart +import Hqiv.Physics.HopfShellBeltramiMassBridge +import Hqiv.Physics.BBNNetworkFromWeights +import Hqiv.Physics.DynamicBBNBaryogenesis +import Hqiv.Physics.ContinuousXiCoupling + +/-! +# Dynamic binding chart (general finite-site readout) + +Parameter-free packaging of the post-T12/T13 dynamic binding formula for an +arbitrary bonded surplus and Compton triplet: + +`E_bind = η_p · surplus_dimless · geomean(tuftVevFactorNetworkedAtCluster) · +dynamicBindingCurvatureFeedbackAtXi(ξ) · EV_per_λ` with `κ(ξ) = γ·(4/8)·ω_K(ξ)/ω_K(ξ_lock)`. + +Bare `tuftVevFactorAtXi` on fixed shells is the ladder chart; the networked factor dresses ξ by +per-nucleon cluster mass ``(A·m_p − B)/A`` so bound D/T/He deficits propagate into heavier readouts. + +LiH is the worked example (`lihDynamicBindingCoreDimless`); this module states the +**generic** factorization used by the Python GMTKN55 chart (`hqiv_dynamic_binding_chart.py`). + +Structural theorems only — no numeric fit to experiment. +-/ + +namespace Hqiv.QuantumChemistry + +open Hqiv +open Hqiv.Physics +open Hqiv.Geometry +open scoped BigOperators + +noncomputable section + +/-- Binding readout kind on the finite-site chart. -/ +inductive DynamicBindingKind + | dissociation + | atomization + deriving DecidableEq, Repr + +/-- Parameter-free Compton triplet scaffold (shell indices `m`, not `ξ = m+1`). -/ +structure DynamicComptonTriplet where + m0 : ℕ + m1 : ℕ + m2 : ℕ + deriving Repr + +def dynamicComptonTripletH2 : DynamicComptonTriplet := ⟨1, 1, 1⟩ + +/-- Heavy-hydride triplet from TUFT chart rows + proton-anchor hydrogen `1`. -/ +def dynamicComptonTripletHeavyHydride : DynamicComptonTriplet := + ⟨tuftHeavyChartShell, tuftStrongChartShell, 1⟩ + +def dynamicComptonTripletHomonuclearPeriod2 : DynamicComptonTriplet := ⟨4, 4, 4⟩ + +def DynamicComptonTriplet.shellAt (t : DynamicComptonTriplet) : Fin 3 → ℕ + | 0 => t.m0 + | 1 => t.m1 + | 2 => t.m2 + +def DynamicComptonTriplet.xiAt (t : DynamicComptonTriplet) : Fin 3 → ℝ + | i => xiOfShell (t.shellAt i) + +/-- Temperature-relative TUFT vev factor: `heavy_lepton_gap_at_xi ξ / heavy_lepton_gap_at_xi 5`. -/ +noncomputable def tuftVevFactorAtXi (ξ : ℝ) : ℝ := + heavy_lepton_gap_at_xi ξ / heavy_lepton_gap_at_xi 5 + +theorem tuftVevFactorAtXi_lockin : + tuftVevFactorAtXi 5 = 1 := by + unfold tuftVevFactorAtXi + have h0 : heavy_lepton_gap_at_xi 5 ≠ 0 := by + rw [heavy_lepton_gap_at_lockin_eq_four_fifths] + norm_num + field_simp [h0] + +/-- Geometric mean of `tuftVevFactorAtXi` on a Compton triplet. -/ +noncomputable def dynamicComptonTuftVevGeometricMean (t : DynamicComptonTriplet) : ℝ := + Real.rpow ( + tuftVevFactorAtXi (t.xiAt 0) * + tuftVevFactorAtXi (t.xiAt 1) * + tuftVevFactorAtXi (t.xiAt 2)) (1 / 3) + +/-- Per-nucleon cluster mass after BBN/valley binding (same spine as `bbnClusterMass`). -/ +noncomputable def clusterMassMeV (m A : ℕ) (c : ℝ := 1) : ℝ := + (A : ℝ) * derivedProtonMass - bbnClusterBinding m A c + +/-- Mass-networked TUFT vev: ξ_eff = ξ_lock · (clusterMass / A / m_p). -/ +noncomputable def tuftVevFactorNetworkedAtCluster (m A : ℕ) (c : ℝ := 1) : ℝ := + let mEff := clusterMassMeV m A c / (A : ℝ) + tuftVevFactorAtXi (xiLockin * (mEff / derivedProtonMass)) + +/-- BBN-valley networked geomean over ``a = 1, …, A``. -/ +noncomputable def valleyNetworkTuftVevGeometricMean (A : ℕ) (c : ℝ := 1) : ℝ := + Real.rpow (∏ a ∈ Finset.Icc 1 A, tuftVevFactorNetworkedAtCluster (referenceM) a c) (1 / (A : ℝ)) + +/-- Peripheral H on a heavy centre: repulsive contacts per H (CH₄: two each). -/ +def peripheralHHRepulsiveContactsPerHydrogen (nH : ℕ) : ℕ := + if nH < 2 then 0 else if 4 ≤ nH then 2 else if nH = 3 then 2 else 1 + +/-- Undirected H–H repulsive contact points (CH₄: four). -/ +def peripheralHHRepulsiveContactPoints (nH : ℕ) : ℕ := + nH * peripheralHHRepulsiveContactsPerHydrogen nH / 2 + +/-- Mean ξ over a Compton triplet (contact readout). -/ +noncomputable def dynamicComptonXiMean (t : DynamicComptonTriplet) : ℝ := + (t.xiAt 0 + t.xiAt 1 + t.xiAt 2) / 3 + +/-- Dynamic κ(ξ) = γ · (4/8) · ω_K chart ratio (replaces fixed κ_bind). -/ +noncomputable def dynamicBindingCurvatureCouplingAtXi (xi : ℝ) : ℝ := + gamma_HQIV * strongChannelFraction * omegaKContinuous xi xiLockin + +/-- Dimensionless cluster-binding contrast (B_lock − B_qcd) / B_lock. -/ +noncomputable def clusterBindingContrastRelative : ℝ := + (bbnClusterBinding m_lockin 4 - bbnClusterBinding m_QCD 4) / bbnClusterBinding m_lockin 4 + +/-- Binding-curvature correction at contact ξ (dimensionless). -/ +noncomputable def dynamicBindingCurvatureCorrectionAtXi (xi : ℝ) : ℝ := + dynamicBindingCurvatureCouplingAtXi xi * clusterBindingContrastRelative + +/-- First-order binding feedback at ξ. -/ +noncomputable def dynamicBindingCurvatureFeedbackAtXi (xi : ℝ) : ℝ := + 1 + dynamicBindingCurvatureCorrectionAtXi xi + +/-- p-slot active on a Compton triplet (heavy-centre hydride / polyatomic pattern). -/ +def dynamicComptonPShellActive (t : DynamicComptonTriplet) : Bool := + t.m1 > 1 ∧ t.m0 ≠ t.m1 + +/-- +Second-order Compton participation on the p shell: + +`η → η + (4/8) · η²` when the p slot is active (LiH valence trace / shared-p channel). +Inactive for `(1,1,1)` homonuclear H₂. +-/ +noncomputable def dynamicComptonEtaSecondOrder (ηp : ℝ) (hasPShell : Bool) : ℝ := + if hasPShell then ηp + strongChannelFraction * ηp ^ 2 else ηp + +/-- +Second-order binding feedback: first-order κ(ξ) contrast times lapse concentration +`C₂(ξ)/C₂(ξ_lock)` from `tuftHopfKappa6AtXi` (Hopf / BBN mass geometry). +-/ +noncomputable def dynamicBindingCurvatureFeedbackSecondOrderAtXi (xi : ℝ) : ℝ := + dynamicBindingCurvatureFeedbackAtXi xi * + (tuftLapseConcentrationAtXi xi 0 0 / tuftLapseConcentrationAtXi xiLockin 0 0) + +/-- +Generic dimless dynamic binding core on the post-lock-in shell chart. + +`surplus` is either a diatomic bonded-horizon surplus or a polyatomic atomization +surplus supplied by the caller; this module does not fix which physics map is used. +-/ +noncomputable def dynamicBindingCoreDimlessAtXi (ηp surplus vevGeom xi : ℝ) : ℝ := + ηp * surplus * vevGeom * dynamicBindingCurvatureFeedbackAtXi xi + +theorem dynamicBindingCoreDimlessAtXi_eq + (ηp surplus vevGeom xi : ℝ) : + dynamicBindingCoreDimlessAtXi ηp surplus vevGeom xi = + ηp * surplus * vevGeom * dynamicBindingCurvatureFeedbackAtXi xi := rfl + +/-- +Dimless core with second-order η_p (p shell) and optional lapse-dressed feedback. + +Default GMTKN55 chart uses the η second-order factor; C₂ dressing is available for +bulk / BBN-aligned readouts via `dynamicBindingCurvatureFeedbackSecondOrderAtXi`. +-/ +noncomputable def dynamicBindingCoreDimlessSecondOrderAtXi + (ηp surplus vevGeom xi : ℝ) (t : DynamicComptonTriplet) : ℝ := + dynamicComptonEtaSecondOrder ηp (dynamicComptonPShellActive t) * surplus * vevGeom * + dynamicBindingCurvatureFeedbackAtXi xi + +noncomputable def dynamicBindingCoreDimless + (ηp surplus vevGeom : ℝ) (t : DynamicComptonTriplet) : ℝ := + dynamicBindingCoreDimlessAtXi ηp surplus vevGeom (dynamicComptonXiMean t) + +/-- Chemist-convention binding energy in eV from the generic dimless core. -/ +noncomputable def dynamicBindingEnergyEv (core : ℝ) : ℝ := + core * eVPerLambdaUnit_S7HydrogenAnchor + +theorem dynamicBindingCoreDimlessAtXi_pos + (ηp surplus vevGeom xi : ℝ) + (hηp : 0 < ηp) (hsur : 0 < surplus) (hvev : 0 < vevGeom) + (hfb : 0 < dynamicBindingCurvatureFeedbackAtXi xi) : + 0 < dynamicBindingCoreDimlessAtXi ηp surplus vevGeom xi := by + unfold dynamicBindingCoreDimlessAtXi + exact mul_pos (mul_pos (mul_pos hηp hsur) hvev) hfb + +theorem dynamicBindingEnergyEv_pos_of_core_pos (core : ℝ) (hcore : 0 < core) : + 0 < dynamicBindingEnergyEv core := by + unfold dynamicBindingEnergyEv + exact mul_pos hcore (by unfold eVPerLambdaUnit_S7HydrogenAnchor hydrogenGroundIP_eV; norm_num) + +/-- Dissociation surplus alias for a two-fragment bonded horizon (electron counts as naturals). -/ +noncomputable def diatomicBondSurplusDimless + (nTotal nFrag1 nFrag2 : ℕ) + (cfg : NuclearTorusConfig := defaultNuclearTorus) : ℝ := + bondHorizonSurplusDimless nTotal nFrag1 nFrag2 cfg + +/-- Per-nucleon composite-trace binding at shell `m` (BBN / hadron network spine). -/ +noncomputable def perNucleonTraceBindingMeV (m : ℕ) (c : ℝ := 1) : ℝ := + bbnNucleonTraceBinding m c + +theorem perNucleonTraceBindingMeV_eq_bbn (m : ℕ) (c : ℝ) : + perNucleonTraceBindingMeV m c = bbnNucleonTraceBinding m c := rfl + +/-- Cluster binding per nucleon at mass number `A` and shell `m`. -/ +noncomputable def perNucleonClusterBindingMeV (m A : ℕ) (c : ℝ := 1) : ℝ := + bbnClusterBinding m A c / (A : ℝ) + +theorem perNucleonClusterBindingMeV_eq (m A : ℕ) (c : ℝ) : + perNucleonClusterBindingMeV m A c = bbnClusterBinding m A c / (A : ℝ) := rfl + +end + +end Hqiv.QuantumChemistry diff --git a/Hqiv/QuantumChemistry/LiH.lean b/Hqiv/QuantumChemistry/LiH.lean new file mode 100644 index 0000000..435af4f --- /dev/null +++ b/Hqiv/QuantumChemistry/LiH.lean @@ -0,0 +1,195 @@ +import Hqiv.QuantumChemistry.FiniteSiteQuantumChemistry +import Hqiv.Physics.ReadoutGaugeSeed + +/-! +# LiH finite-site orbital scaffold (`s` + `p`) + +This module extends the finite-site chemistry bridge to the first non-`s` benchmark: +LiH valence bookkeeping with explicit `p`-channel weight on Li. + +We keep the same HQIV shell ladder and finite sums; no classical molecular PDE closure +is introduced here. +-/ + +namespace Hqiv.QuantumChemistry + +open Hqiv +open Hqiv.Physics + +/-- Three-site valence scaffold for LiH: +`0 = Li(s)`, `1 = Li(p)`, `2 = H(s)`. -/ +def lihValenceSpec (mLiS mLiP mH : ℕ) : OrbitalSiteChemistrySpec 3 where + shell := fun i => + if (i : ℕ) = 0 then mLiS else if (i : ℕ) = 1 then mLiP else mH + channel := fun i => + if (i : ℕ) = 0 then .s else if (i : ℕ) = 1 then .p else .s + +/-- Channel-faithful LiH valence site-energy trace (`s=1`, `p=3`). -/ +noncomputable def lihValenceSiteEnergyTrace (mLiS mLiP mH : ℕ) : ℝ := + orbitalWeightedSiteEnergyTrace (lihValenceSpec mLiS mLiP mH) + +theorem lihValenceSiteEnergyTrace_eq (mLiS mLiP mH : ℕ) : + lihValenceSiteEnergyTrace mLiS mLiP mH = + Hqiv.ProteinResearch.latticeFullModeEnergy mLiS + + 3 * Hqiv.ProteinResearch.latticeFullModeEnergy mLiP + + Hqiv.ProteinResearch.latticeFullModeEnergy mH := by + unfold lihValenceSiteEnergyTrace orbitalWeightedSiteEnergyTrace lihValenceSpec + simp [orbitalDegeneracy, Fin.sum_univ_three] + +theorem lihValenceSiteEnergyTrace_nonneg (mLiS mLiP mH : ℕ) : + 0 ≤ lihValenceSiteEnergyTrace mLiS mLiP mH := by + rw [lihValenceSiteEnergyTrace_eq] + nlinarith [latticeFullModeEnergy_nonneg mLiS, latticeFullModeEnergy_nonneg mLiP, + latticeFullModeEnergy_nonneg mH] + +/-- `s`-only proxy (kept for calibration comparison). -/ +noncomputable def lihSOnlyProxySiteEnergyTrace (mLiS mH : ℕ) : ℝ := + Hqiv.ProteinResearch.latticeFullModeEnergy mLiS + + Hqiv.ProteinResearch.latticeFullModeEnergy mH + +/-- Explicit Li `p`-shell uplift over the `s`-only proxy. -/ +noncomputable def lihPShellUpliftSiteEnergy (mLiP : ℕ) : ℝ := + 3 * Hqiv.ProteinResearch.latticeFullModeEnergy mLiP + +theorem lihValenceSiteEnergyTrace_eq_proxy_plus_pUplift (mLiS mLiP mH : ℕ) : + lihValenceSiteEnergyTrace mLiS mLiP mH = + lihSOnlyProxySiteEnergyTrace mLiS mH + lihPShellUpliftSiteEnergy mLiP := by + rw [lihValenceSiteEnergyTrace_eq] + unfold lihSOnlyProxySiteEnergyTrace lihPShellUpliftSiteEnergy + ring + +/-- Channel-faithful LiH valence mode-budget trace (`accessibleModeBudgetUpToShell`). -/ +noncomputable def lihValenceModeBudgetTrace (mLiS mLiP mH : ℕ) : ℝ := + orbitalWeightedModeBudgetTrace (lihValenceSpec mLiS mLiP mH) + +theorem lihValenceModeBudgetTrace_eq (mLiS mLiP mH : ℕ) : + lihValenceModeBudgetTrace mLiS mLiP mH = + Hqiv.Physics.accessibleModeBudgetUpToShell mLiS + + 3 * Hqiv.Physics.accessibleModeBudgetUpToShell mLiP + + Hqiv.Physics.accessibleModeBudgetUpToShell mH := by + unfold lihValenceModeBudgetTrace orbitalWeightedModeBudgetTrace lihValenceSpec + simp [orbitalDegeneracy, Fin.sum_univ_three] + +theorem lihValenceModeBudgetTrace_nonneg (mLiS mLiP mH : ℕ) : + 0 ≤ lihValenceModeBudgetTrace mLiS mLiP mH := by + rw [lihValenceModeBudgetTrace_eq] + nlinarith [Hqiv.Physics.accessibleModeBudgetUpToShell_nonneg mLiS, + Hqiv.Physics.accessibleModeBudgetUpToShell_nonneg mLiP, + Hqiv.Physics.accessibleModeBudgetUpToShell_nonneg mH] + +/-! ## LiH Compton-shell ξ / Ωₖ bridge -/ + +/-- Li(s) shell used by the Compton LiH readout. -/ +def lihComptonLiSShell : ℕ := 4 + +/-- Li(p) shell used by the Compton LiH readout. -/ +def lihComptonLiPShell : ℕ := 3 + +/-- H(s) shell used by the Compton LiH readout. -/ +def lihComptonHSShell : ℕ := 1 + +theorem lihValenceSpec_compton_LiS : + (lihValenceSpec lihComptonLiSShell lihComptonLiPShell lihComptonHSShell).shell + ⟨0, by decide⟩ = lihComptonLiSShell := by + simp [lihValenceSpec] + +theorem lihValenceSpec_compton_LiP : + (lihValenceSpec lihComptonLiSShell lihComptonLiPShell lihComptonHSShell).shell + ⟨1, by decide⟩ = lihComptonLiPShell := by + simp [lihValenceSpec] + +theorem lihValenceSpec_compton_HS : + (lihValenceSpec lihComptonLiSShell lihComptonLiPShell lihComptonHSShell).shell + ⟨2, by decide⟩ = lihComptonHSShell := by + simp [lihValenceSpec] + +/-- Canonical Compton LiH valence assignment: `lihValenceSpec 4 3 1`. -/ +noncomputable def lihComptonValenceSpec : OrbitalSiteChemistrySpec 3 := + lihValenceSpec lihComptonLiSShell lihComptonLiPShell lihComptonHSShell + +theorem lihComptonValenceSpec_eq : + lihComptonValenceSpec = + lihValenceSpec lihComptonLiSShell lihComptonLiPShell lihComptonHSShell := rfl + +/-- +The three Compton shells used by `lihComptonValenceSpec` are exactly +`lihComptonLiSShell = 4`, `lihComptonLiPShell = 3`, and `lihComptonHSShell = 1`. +-/ +theorem lihComptonUsedShells_eq_spec : + lihComptonLiSShell = 4 ∧ + lihComptonLiPShell = 3 ∧ + lihComptonHSShell = 1 ∧ + lihComptonValenceSpec.shell ⟨0, by decide⟩ = lihComptonLiSShell ∧ + lihComptonValenceSpec.shell ⟨1, by decide⟩ = lihComptonLiPShell ∧ + lihComptonValenceSpec.shell ⟨2, by decide⟩ = lihComptonHSShell := by + refine ⟨rfl, rfl, rfl, ?_, ?_, ?_⟩ + · exact lihValenceSpec_compton_LiS + · exact lihValenceSpec_compton_LiP + · exact lihValenceSpec_compton_HS + +/-- +Local increment form of the discrete-continuous Ωₖ bridge at one integer shell. + +This is intentionally weaker than `ContinuousXiPath.OmegaKIntegerBridge`: LiH only +needs adjacent increments at its three Compton readout shells, not a global +identification of the analytic primitive with the finite null-lattice sum. +-/ +def lihLocalOmegaKIncrementBridge (n : ℕ) : Prop := + ContinuousXiPath.omegaK_xi (xiOfShell (n + 1)) - + ContinuousXiPath.omegaK_xi (xiOfShell n) = + omega_k_partial (n + 1) - omega_k_partial n + +/-- Finite Ωₖ bridge payload for the LiH Compton shells `(4,3,1)`. -/ +structure LiHComptonOmegaKBridge where + liS : lihLocalOmegaKIncrementBridge lihComptonLiSShell + liP : lihLocalOmegaKIncrementBridge lihComptonLiPShell + hS : lihLocalOmegaKIncrementBridge lihComptonHSShell + +theorem lihLocalOmegaKIncrementBridge_from_global + (hΩ : Hqiv.readoutOmegaKIntegerBridge) (n : ℕ) : + lihLocalOmegaKIncrementBridge n := + ContinuousXiPath.omegaK_xi_integer_increment_bridge hΩ n + +theorem liHComptonOmegaKBridge_from_global + (hΩ : Hqiv.readoutOmegaKIntegerBridge) : LiHComptonOmegaKBridge where + liS := lihLocalOmegaKIncrementBridge_from_global hΩ lihComptonLiSShell + liP := lihLocalOmegaKIncrementBridge_from_global hΩ lihComptonLiPShell + hS := lihLocalOmegaKIncrementBridge_from_global hΩ lihComptonHSShell + +theorem imprintWeightedReadoutPhase_xi_matches_integer_step_of_local_bridge + {n : ℕ} (hΩ : lihLocalOmegaKIncrementBridge n) : + Hqiv.imprintWeightedReadoutPhase_xi_alias + (xiOfShell n) (xiOfShell (n + 1)) = + Hqiv.imprintWeightedReadoutPhase n := by + unfold Hqiv.imprintWeightedReadoutPhase_xi_alias + unfold ContinuousXiPath.imprintWeightedReadoutPhase_xi + unfold Hqiv.imprintWeightedReadoutPhase + rw [ContinuousXiPath.phi_xi_chart] + rw [hΩ] + +/-- Li(s) Compton shell: continuous-ξ and discrete imprint phases match at `m = 4`. -/ +theorem lihCompton_LiS_imprintWeightedReadoutPhase_xi_matches + (hΩ : LiHComptonOmegaKBridge) : + Hqiv.imprintWeightedReadoutPhase_xi_alias + (xiOfShell lihComptonLiSShell) (xiOfShell (lihComptonLiSShell + 1)) = + Hqiv.imprintWeightedReadoutPhase lihComptonLiSShell := + imprintWeightedReadoutPhase_xi_matches_integer_step_of_local_bridge hΩ.liS + +/-- Li(p) Compton shell: continuous-ξ and discrete imprint phases match at `m = 3`. -/ +theorem lihCompton_LiP_imprintWeightedReadoutPhase_xi_matches + (hΩ : LiHComptonOmegaKBridge) : + Hqiv.imprintWeightedReadoutPhase_xi_alias + (xiOfShell lihComptonLiPShell) (xiOfShell (lihComptonLiPShell + 1)) = + Hqiv.imprintWeightedReadoutPhase lihComptonLiPShell := + imprintWeightedReadoutPhase_xi_matches_integer_step_of_local_bridge hΩ.liP + +/-- H(s) Compton shell: continuous-ξ and discrete imprint phases match at `m = 1`. -/ +theorem lihCompton_HS_imprintWeightedReadoutPhase_xi_matches + (hΩ : LiHComptonOmegaKBridge) : + Hqiv.imprintWeightedReadoutPhase_xi_alias + (xiOfShell lihComptonHSShell) (xiOfShell (lihComptonHSShell + 1)) = + Hqiv.imprintWeightedReadoutPhase lihComptonHSShell := + imprintWeightedReadoutPhase_xi_matches_integer_step_of_local_bridge hΩ.hS + +end Hqiv.QuantumChemistry + diff --git a/Hqiv/QuantumChemistry/LiHDerivation.lean b/Hqiv/QuantumChemistry/LiHDerivation.lean new file mode 100644 index 0000000..44ab035 --- /dev/null +++ b/Hqiv/QuantumChemistry/LiHDerivation.lean @@ -0,0 +1,255 @@ +import Hqiv.QuantumChemistry.LiH +import Hqiv.Geometry.BondedHorizonCasimir +import Hqiv.Geometry.ComptonNuclearTorus +import Hqiv.Physics.ComptonIRWindow + +/-! +# LiH derivation scaffold (no empirical calibration) + +This module packages a derivation-first LiH dissociation indicator in HQIV dimensionless units. +No fitted rescale is introduced. + +Ingredients: + +* bonded-horizon non-additivity (`bondHorizonSurplusDimless 4 3 1`), +* explicit Li `p`-channel uplift from the orbital-resolved finite-site chemistry layer. +-/ + +namespace Hqiv.QuantumChemistry + +open Hqiv +open Hqiv.Physics + +/-- LiH dissociation-style bonded surplus in dimensionless HQIV units (`4 -> 3 + 1`). -/ +noncomputable def lihBondedSurplusDimless + (cfg : Hqiv.Geometry.NuclearTorusConfig := Hqiv.Geometry.defaultNuclearTorus) : ℝ := + Hqiv.Geometry.bondHorizonSurplusDimless 4 3 1 cfg + +theorem lihBondedSurplusDimless_eq + (cfg : Hqiv.Geometry.NuclearTorusConfig) : + lihBondedSurplusDimless cfg = Hqiv.Geometry.bondHorizonSurplusDimless 4 3 1 cfg := rfl + +/-- Orbital-resolution correction over an `s`-only LiH proxy. -/ +noncomputable def lihDerivedElectronicCorrectionDimless (mLiS mLiP mH : ℕ) : ℝ := + lihValenceSiteEnergyTrace mLiS mLiP mH - lihSOnlyProxySiteEnergyTrace mLiS mH + +theorem lihDerivedElectronicCorrection_eq_p_uplift (mLiS mLiP mH : ℕ) : + lihDerivedElectronicCorrectionDimless mLiS mLiP mH = lihPShellUpliftSiteEnergy mLiP := by + unfold lihDerivedElectronicCorrectionDimless + rw [lihValenceSiteEnergyTrace_eq_proxy_plus_pUplift] + ring + +theorem latticeFullModeEnergy_pos (m : ℕ) : 0 < Hqiv.ProteinResearch.latticeFullModeEnergy m := by + rw [latticeFullModeEnergy_closed_form] + positivity + +theorem lihPShellUpliftSiteEnergy_nonneg (mLiP : ℕ) : + 0 ≤ lihPShellUpliftSiteEnergy mLiP := by + unfold lihPShellUpliftSiteEnergy + nlinarith [latticeFullModeEnergy_nonneg mLiP] + +theorem lihPShellUpliftSiteEnergy_pos (mLiP : ℕ) : + 0 < lihPShellUpliftSiteEnergy mLiP := by + unfold lihPShellUpliftSiteEnergy + nlinarith [latticeFullModeEnergy_pos mLiP] + +/-- Derivation-first LiH indicator in dimensionless units: +bonded-horizon surplus plus orbital (`p`) correction. -/ +noncomputable def lihDerivedDissociationIndicatorDimless + (mLiS mLiP mH : ℕ) + (cfg : Hqiv.Geometry.NuclearTorusConfig := Hqiv.Geometry.defaultNuclearTorus) : ℝ := + lihBondedSurplusDimless cfg + lihDerivedElectronicCorrectionDimless mLiS mLiP mH + +theorem lihDerivedDissociationIndicator_eq_bond_plus_p + (mLiS mLiP mH : ℕ) (cfg : Hqiv.Geometry.NuclearTorusConfig) : + lihDerivedDissociationIndicatorDimless mLiS mLiP mH cfg = + lihBondedSurplusDimless cfg + lihPShellUpliftSiteEnergy mLiP := by + unfold lihDerivedDissociationIndicatorDimless + rw [lihDerivedElectronicCorrection_eq_p_uplift] + +theorem lihDerivedDissociationIndicator_ge_bond + (mLiS mLiP mH : ℕ) (cfg : Hqiv.Geometry.NuclearTorusConfig) : + lihBondedSurplusDimless cfg ≤ lihDerivedDissociationIndicatorDimless mLiS mLiP mH cfg := by + rw [lihDerivedDissociationIndicator_eq_bond_plus_p] + nlinarith [lihPShellUpliftSiteEnergy_nonneg mLiP] + +theorem lihDerivedDissociationIndicator_gt_bond + (mLiS mLiP mH : ℕ) (cfg : Hqiv.Geometry.NuclearTorusConfig) : + lihBondedSurplusDimless cfg < lihDerivedDissociationIndicatorDimless mLiS mLiP mH cfg := by + rw [lihDerivedDissociationIndicator_eq_bond_plus_p] + nlinarith [lihPShellUpliftSiteEnergy_pos mLiP] + +theorem lihDerivedDissociationIndicator_neg_iff_bond_plus_p_neg + (mLiS mLiP mH : ℕ) (cfg : Hqiv.Geometry.NuclearTorusConfig) : + lihDerivedDissociationIndicatorDimless mLiS mLiP mH cfg < 0 ↔ + lihBondedSurplusDimless cfg + lihPShellUpliftSiteEnergy mLiP < 0 := by + rw [lihDerivedDissociationIndicator_eq_bond_plus_p] + +theorem lihDerivedDissociationIndicator_pos_iff_bond_plus_p_pos + (mLiS mLiP mH : ℕ) (cfg : Hqiv.Geometry.NuclearTorusConfig) : + 0 < lihDerivedDissociationIndicatorDimless mLiS mLiP mH cfg ↔ + 0 < lihBondedSurplusDimless cfg + lihPShellUpliftSiteEnergy mLiP := by + rw [lihDerivedDissociationIndicator_eq_bond_plus_p] + +theorem lih_p_channel_necessity + (mLiS mLiP mH : ℕ) : + lihDerivedElectronicCorrectionDimless mLiS mLiP mH = lihPShellUpliftSiteEnergy mLiP := by + exact lihDerivedElectronicCorrection_eq_p_uplift mLiS mLiP mH + +/-- Participation-weighted LiH `p`-channel correction (`η_p ∈ (0,1)` from phase window). -/ +noncomputable def lihDerivedElectronicCorrectionWithParticipationDimless + (ηp : ℝ) (mLiP : ℕ) : ℝ := + ηp * lihPShellUpliftSiteEnergy mLiP + +theorem lihDerivedElectronicCorrectionWithParticipation_nonneg + (ηp : ℝ) (hηp : 0 ≤ ηp) (mLiP : ℕ) : + 0 ≤ lihDerivedElectronicCorrectionWithParticipationDimless ηp mLiP := by + unfold lihDerivedElectronicCorrectionWithParticipationDimless + exact mul_nonneg hηp (lihPShellUpliftSiteEnergy_nonneg mLiP) + +theorem lihDerivedElectronicCorrectionWithParticipation_le_full + (ηp : ℝ) (hηp1 : ηp ≤ 1) (mLiP : ℕ) : + lihDerivedElectronicCorrectionWithParticipationDimless ηp mLiP ≤ + lihPShellUpliftSiteEnergy mLiP := by + unfold lihDerivedElectronicCorrectionWithParticipationDimless + have hU : 0 ≤ lihPShellUpliftSiteEnergy mLiP := lihPShellUpliftSiteEnergy_nonneg mLiP + nlinarith [mul_le_mul_of_nonneg_right hηp1 hU] + +/-- Compton/IR-window induced participation `η_p = x/θ` for LiH. -/ +noncomputable def lihComptonParticipationEta (x : ℝ) : ℝ := + Hqiv.Physics.phaseParticipationEta x + +theorem lihComptonParticipationEta_mem_unit + (x : ℝ) (hx0 : 0 < x) (hxθ : x < Hqiv.Physics.phaseTheta) : + 0 < lihComptonParticipationEta x ∧ lihComptonParticipationEta x < 1 := by + unfold lihComptonParticipationEta + exact Hqiv.Physics.phaseParticipationEta_mem_unit x hx0 hxθ + +/-- LiH participation-weighted indicator: +bonded-horizon surplus plus phase-window weighted Li `p` uplift. -/ +noncomputable def lihDerivedDissociationIndicatorWithParticipationDimless + (ηp : ℝ) (mLiP : ℕ) + (cfg : Hqiv.Geometry.NuclearTorusConfig := Hqiv.Geometry.defaultNuclearTorus) : ℝ := + lihBondedSurplusDimless cfg + lihDerivedElectronicCorrectionWithParticipationDimless ηp mLiP + +theorem lihDerivedDissociationIndicatorWithParticipation_ge_bond + (ηp : ℝ) (hηp : 0 ≤ ηp) (mLiP : ℕ) (cfg : Hqiv.Geometry.NuclearTorusConfig) : + lihBondedSurplusDimless cfg ≤ + lihDerivedDissociationIndicatorWithParticipationDimless ηp mLiP cfg := by + unfold lihDerivedDissociationIndicatorWithParticipationDimless + nlinarith [lihDerivedElectronicCorrectionWithParticipation_nonneg ηp hηp mLiP] + +theorem lihDerivedDissociationIndicatorWithParticipation_le_full_uplift + (ηp : ℝ) (hηp1 : ηp ≤ 1) (mLiP : ℕ) + (cfg : Hqiv.Geometry.NuclearTorusConfig) : + lihDerivedDissociationIndicatorWithParticipationDimless ηp mLiP cfg ≤ + lihBondedSurplusDimless cfg + lihPShellUpliftSiteEnergy mLiP := by + unfold lihDerivedDissociationIndicatorWithParticipationDimless + nlinarith [lihDerivedElectronicCorrectionWithParticipation_le_full ηp hηp1 mLiP] + +theorem lihDerivedDissociationIndicatorWithParticipation_phase_window_control + (x : ℝ) (hx0 : 0 < x) (hxθ : x < Hqiv.Physics.phaseTheta) (mLiP : ℕ) + (cfg : Hqiv.Geometry.NuclearTorusConfig) : + lihBondedSurplusDimless cfg ≤ + lihDerivedDissociationIndicatorWithParticipationDimless (lihComptonParticipationEta x) mLiP cfg ∧ + lihDerivedDissociationIndicatorWithParticipationDimless (lihComptonParticipationEta x) mLiP cfg ≤ + lihBondedSurplusDimless cfg + lihPShellUpliftSiteEnergy mLiP := by + rcases lihComptonParticipationEta_mem_unit x hx0 hxθ with ⟨hη0, hη1⟩ + have hη0' : 0 ≤ lihComptonParticipationEta x := le_of_lt hη0 + have hη1' : lihComptonParticipationEta x ≤ 1 := le_of_lt hη1 + constructor + · exact lihDerivedDissociationIndicatorWithParticipation_ge_bond + (lihComptonParticipationEta x) hη0' mLiP cfg + · exact lihDerivedDissociationIndicatorWithParticipation_le_full_uplift + (lihComptonParticipationEta x) hη1' mLiP cfg + +/-- LiH bonded surplus using Compton/IR-window sourced nuclear torus angles. -/ +noncomputable def lihBondedSurplusDimlessComptonWindow + (E : Fin 3 → ℝ) (ħ : ℝ) (hħ : 0 < ħ) (t : Fin 3 → ℝ) : ℝ := + lihBondedSurplusDimless (cfg := Hqiv.Geometry.comptonLinkedNuclearTorusConfig E ħ hħ t) + +theorem lihBondedSurplusDimlessComptonWindow_eq + (E : Fin 3 → ℝ) (ħ : ℝ) (hħ : 0 < ħ) (t : Fin 3 → ℝ) : + lihBondedSurplusDimlessComptonWindow E ħ hħ t = + Hqiv.Geometry.bondHorizonSurplusDimless 4 3 1 + (Hqiv.Geometry.comptonLinkedNuclearTorusConfig E ħ hħ t) := rfl + +/-! ## Compton valence + formally justified imprint readouts -/ + +/-- LiH dissociation indicator at the canonical Compton shells `(4,3,1)`. -/ +noncomputable def lihComptonDerivedDissociationIndicatorDimless + (cfg : Hqiv.Geometry.NuclearTorusConfig := Hqiv.Geometry.defaultNuclearTorus) : ℝ := + lihDerivedDissociationIndicatorDimless lihComptonLiSShell lihComptonLiPShell lihComptonHSShell cfg + +theorem lihComptonDerivedDissociationIndicator_eq_bond_plus_p + (cfg : Hqiv.Geometry.NuclearTorusConfig) : + lihComptonDerivedDissociationIndicatorDimless cfg = + lihBondedSurplusDimless cfg + lihPShellUpliftSiteEnergy lihComptonLiPShell := by + unfold lihComptonDerivedDissociationIndicatorDimless + exact lihDerivedDissociationIndicator_eq_bond_plus_p lihComptonLiSShell lihComptonLiPShell + lihComptonHSShell cfg + +/-- +At the Compton `(4,3,1)` sites, discrete and continuous-ξ imprint phases agree on each +integer step once `LiHComptonOmegaKBridge` is supplied. +-/ +theorem lihCompton_imprintWeightedReadoutPhases_justified + (hΩ : LiHComptonOmegaKBridge) : + Hqiv.imprintWeightedReadoutPhase_xi_alias (xiOfShell lihComptonLiSShell) + (xiOfShell (lihComptonLiSShell + 1)) = + Hqiv.imprintWeightedReadoutPhase lihComptonLiSShell ∧ + Hqiv.imprintWeightedReadoutPhase_xi_alias (xiOfShell lihComptonLiPShell) + (xiOfShell (lihComptonLiPShell + 1)) = + Hqiv.imprintWeightedReadoutPhase lihComptonLiPShell ∧ + Hqiv.imprintWeightedReadoutPhase_xi_alias (xiOfShell lihComptonHSShell) + (xiOfShell (lihComptonHSShell + 1)) = + Hqiv.imprintWeightedReadoutPhase lihComptonHSShell := by + refine ⟨?_, ?_, ?_⟩ + · exact lihCompton_LiS_imprintWeightedReadoutPhase_xi_matches hΩ + · exact lihCompton_LiP_imprintWeightedReadoutPhase_xi_matches hΩ + · exact lihCompton_HS_imprintWeightedReadoutPhase_xi_matches hΩ + +/-- +Gauge-seed `ω` at the Li(p) Compton shell may be taken from either the discrete imprint +phase or the continuous-ξ chart slot; the bridge identifies them. +-/ +theorem lihCompton_LiP_seedPotential_omega_from_discrete_imprint + (hΩ : LiHComptonOmegaKBridge) (θ : ℝ) : + Hqiv.seedPotentialMinimalCycle (Hqiv.imprintWeightedReadoutPhase lihComptonLiPShell) θ = + Hqiv.seedPotentialMinimalCycle + (Hqiv.imprintWeightedReadoutPhase_xi_alias (xiOfShell lihComptonLiPShell) + (xiOfShell (lihComptonLiPShell + 1))) θ := by + have hphase := lihCompton_LiP_imprintWeightedReadoutPhase_xi_matches hΩ + rw [hphase] + +/-- +Compton dissociation indicator packaged with formally justified per-site imprint phases. +The indicator formula is unchanged; the `have` block records that readout phases on the +three Compton shells are licensed by `lihCompton_imprintWeightedReadoutPhases_justified`. +-/ +theorem lihComptonDerivedDissociationIndicator_with_justified_readouts + (hΩ : LiHComptonOmegaKBridge) + (cfg : Hqiv.Geometry.NuclearTorusConfig) : + lihComptonDerivedDissociationIndicatorDimless cfg = + lihBondedSurplusDimless cfg + lihPShellUpliftSiteEnergy lihComptonLiPShell := by + have _hReadouts := lihCompton_imprintWeightedReadoutPhases_justified hΩ + exact lihComptonDerivedDissociationIndicator_eq_bond_plus_p cfg + +/-- +Participation-weighted Compton indicator at the canonical shells, with the same imprint +phase justification on the Li `p` readout coordinate `m = 3`. +-/ +theorem lihComptonDerivedDissociationIndicatorWithParticipation_phase_readout_justified + (hΩ : LiHComptonOmegaKBridge) (ηp : ℝ) + (cfg : Hqiv.Geometry.NuclearTorusConfig) : + lihDerivedDissociationIndicatorWithParticipationDimless ηp lihComptonLiPShell cfg = + lihBondedSurplusDimless cfg + + lihDerivedElectronicCorrectionWithParticipationDimless ηp lihComptonLiPShell := by + have _hLiP := + lihCompton_LiP_imprintWeightedReadoutPhase_xi_matches hΩ + unfold lihDerivedDissociationIndicatorWithParticipationDimless + unfold lihDerivedElectronicCorrectionWithParticipationDimless + rfl + +end Hqiv.QuantumChemistry + diff --git a/Hqiv/QuantumChemistry/PhaseAllotropeDerivation.lean b/Hqiv/QuantumChemistry/PhaseAllotropeDerivation.lean new file mode 100644 index 0000000..a9f4c3c --- /dev/null +++ b/Hqiv/QuantumChemistry/PhaseAllotropeDerivation.lean @@ -0,0 +1,64 @@ +import Hqiv.QuantumChemistry.PhaseGeometryDensity + +/-! +# Phase allotrope derivation (structural layer) + +Allotropes are **derived** from monomer geometry (VSEPR motif + intermolecular +coordination), not chosen from a static name table. + +Python package: `hqiv_lab` (`derive_allotropes`, `preferred_allotrope`). +Unit cells feed `PhaseGeometryDensity` for ρ and material response. +-/ + +namespace Hqiv.QuantumChemistry + +/-- Intermolecular packing motif (Python `IntermolecularMotif`). -/ +inductive IntermolecularMotif + | tetrahedralHbond + | pyramidalHbond + | apolarClosePack + | linearChain + | diatomic + | generic + deriving DecidableEq + +/-- Named allotrope label from a packing template. -/ +structure AllotropeLabel where + name : String + +/-- Derived unit cell witness (lattice constants in ångström). -/ +structure DerivedUnitCell where + allotrope : String + moleculesPerCell : ℕ + aAngstrom : ℝ + bAngstrom : ℝ + cAngstrom : ℝ + crystal : CrystalSystem + +/-- Allotrope candidate with density and ranking score (Python sorts by `score`). -/ +structure AllotropeCandidate where + label : AllotropeLabel + cell : DerivedUnitCell + densityGPerCm3 : ℝ + curvatureDensityFraction : ℝ + score : ℝ + motif : IntermolecularMotif + +/-- H₂O tetrahedral motif implies ice-Ih as the preferred hexagonal template. -/ +def intermolecularMotifH2O : IntermolecularMotif := .tetrahedralHbond + +def allotropeLabelIceIh : AllotropeLabel := ⟨"Ih"⟩ + +/-- Motif → at least one template exists (structural placeholder; enumeration in Python). -/ +theorem motif_h2o_has_ice_ih_label : + intermolecularMotifH2O = .tetrahedralHbond ∧ + allotropeLabelIceIh.name = "Ih" := by + constructor <;> rfl + +/-- Derived ρ_curvature ∈ [0,1] when solid density is below liquid reference. -/ +theorem curvatureFraction_from_density_le_one (ρSolid ρLiquid : ℝ) + (hρ : 0 ≤ ρSolid) (hL : 0 < ρLiquid) : + curvatureDensityFraction ρSolid ρLiquid ≤ 1 := + curvatureDensityFraction_le_one ρSolid ρLiquid + +end Hqiv.QuantumChemistry diff --git a/Hqiv/QuantumChemistry/PhaseGeometryDensity.lean b/Hqiv/QuantumChemistry/PhaseGeometryDensity.lean new file mode 100644 index 0000000..4ab18b9 --- /dev/null +++ b/Hqiv/QuantumChemistry/PhaseGeometryDensity.lean @@ -0,0 +1,259 @@ +import Hqiv.Physics.HomogeneousCurvatureSecondOrder + +/-! +# Phase geometry → mass density → local curvature ρ + +Condensed-phase readout without macroscopic atom counting: + +1. **Preferred allotrope** (e.g.\ ice Ih for H₂O) fixes a unit-cell geometry witness. +2. **Mass density** ρ_mass = Z·M/(N_A·V_cell) from lattice constants and formula weight. +3. **Curvature density** ρ_curv = clamp(ρ_mass / ρ_liquid_ref) feeds + `homogeneousCurvatureBudgetAtXi` and second-order κ₆ feedback on melt / binding. + +Python mirror: `scripts/hqiv_phase_geometry_density.py`. +Melt witness: `scripts/hqiv_thermodynamic_phase_from_tp.py` (`material_scales_bulk_h2o`). + +**Orbital extension:** planetary mass + radius + encounter distance supply local curvature +ρ via inverse-square weighting (Earth bulk dominates; dilute limit at large r). +Feeds the same `homogeneousCurvatureBudgetAtXi` spine as condensed phase — no shell-4 pin. +Lean bridge: `Hqiv.Physics.OrbitalFlybyScaffold`. +-/ + +namespace Hqiv.QuantumChemistry + +open Hqiv +open Hqiv.Physics + +/-- Crystalline Bravais class for unit-cell volume (geometry witness only). -/ +inductive CrystalSystem + | hexagonal + | cubic + | orthorhombic + deriving DecidableEq, Repr + +/-- Unit-cell geometry witness: lattice constants in ångström, Z molecules per cell. -/ +structure PhaseUnitCell where + allotrope : String + moleculesPerCell : ℕ + molecularWeightAmu : ℝ + aAngstrom : ℝ + bAngstrom : ℝ + cAngstrom : ℝ + crystal : CrystalSystem + +/-- Ångström → centimetre (crystallographic convention). -/ +noncomputable def angstromToCm : ℝ := 1e-8 + +/-- Avogadro constant (g/mol per molecule count). -/ +noncomputable def avogadroNumber : ℝ := 6.02214076e23 + +theorem angstromToCm_pos : 0 < angstromToCm := by unfold angstromToCm; norm_num + +theorem avogadroNumber_pos : 0 < avogadroNumber := by unfold avogadroNumber; norm_num + +/-- Unit-cell volume in cm³ from lattice constants. -/ +noncomputable def unitCellVolumeCm3 (cell : PhaseUnitCell) : ℝ := + let a := cell.aAngstrom * angstromToCm + let b := cell.bAngstrom * angstromToCm + let c := cell.cAngstrom * angstromToCm + match cell.crystal with + | .hexagonal => Real.sqrt 3 / 2 * a * a * c + | .cubic => a * a * a + | .orthorhombic => a * b * c + +/-- Mass density ρ [g/cm³] = Z·M / (N_A·V). -/ +noncomputable def massDensityGPerCm3 (cell : PhaseUnitCell) : ℝ := + (cell.moleculesPerCell : ℝ) * cell.molecularWeightAmu / + (avogadroNumber * unitCellVolumeCm3 cell) + +/-- +Curvature-density fraction ρ ∈ [0,1]: solid geometry density relative to a liquid +reference at the melt comparison (H₂O liquid reference = 1.0 g/cm³ scale). +-/ +noncomputable def curvatureDensityFraction (ρSolid ρLiquidRef : ℝ) : ℝ := + clampMediumDensity (ρSolid / ρLiquidRef) + +/-- Homogeneous curvature budget at contact ξ using phase-derived ρ. -/ +noncomputable def homogeneousCurvatureBudgetFromPhase (ξ ρ_phase : ℝ) : ℝ := + homogeneousCurvatureBudgetAtXi ξ ρ_phase + +/-- Ice Ih hexagonal cell for H₂O at ~273 K (experimental geometry witness). -/ +noncomputable def phaseUnitCellH2OIceIh : PhaseUnitCell := + { allotrope := "Ih" + moleculesPerCell := 4 + molecularWeightAmu := 18.015 + aAngstrom := 4.515 + bAngstrom := 4.515 + cAngstrom := 7.362 + crystal := .hexagonal } + +/-- Liquid-water reference density at melt comparison [g/cm³]. -/ +noncomputable def liquidReferenceDensityH2O : ℝ := 1.0 + +/-- Curvature fraction for ice Ih vs liquid water reference. -/ +noncomputable def curvatureDensityFractionH2OIceIh : ℝ := + curvatureDensityFraction (massDensityGPerCm3 phaseUnitCellH2OIceIh) liquidReferenceDensityH2O + +/-- Second-order κ₆ feedback at bulk H₂O contact ξ with ice-Ih phase ρ (no nucleation defect). -/ +noncomputable def bindingCurvatureFeedbackH2OBulkIceIh (ξ : ℝ) : ℝ := + bindingCurvatureFeedbackSecondOrderHomogeneous ξ curvatureDensityFractionH2OIceIh 0 + +theorem unitCellVolumeCm3_pos_of_pos_lattice (cell : PhaseUnitCell) + (ha : 0 < cell.aAngstrom) (hb : 0 < cell.bAngstrom) (hc : 0 < cell.cAngstrom) : + 0 < unitCellVolumeCm3 cell := by + unfold unitCellVolumeCm3 + rcases cell.crystal with _ | _ | _ + all_goals + have ha' : 0 < cell.aAngstrom * angstromToCm := mul_pos ha angstromToCm_pos + have hb' : 0 < cell.bAngstrom * angstromToCm := mul_pos hb angstromToCm_pos + have hc' : 0 < cell.cAngstrom * angstromToCm := mul_pos hc angstromToCm_pos + positivity + +theorem massDensityGPerCm3_pos_of_pos_lattice (cell : PhaseUnitCell) + (hZ : 0 < cell.moleculesPerCell) (hM : 0 < cell.molecularWeightAmu) + (ha : 0 < cell.aAngstrom) (hb : 0 < cell.bAngstrom) (hc : 0 < cell.cAngstrom) : + 0 < massDensityGPerCm3 cell := by + unfold massDensityGPerCm3 + have hV := unitCellVolumeCm3_pos_of_pos_lattice cell ha hb hc + refine div_pos ?_ (mul_pos avogadroNumber_pos hV) + exact mul_pos (Nat.cast_pos.mpr hZ) hM + +theorem massDensityH2OIceIh_pos : 0 < massDensityGPerCm3 phaseUnitCellH2OIceIh := by + unfold phaseUnitCellH2OIceIh + exact massDensityGPerCm3_pos_of_pos_lattice _ (by decide) (by norm_num) + (by norm_num) (by norm_num) (by norm_num) + +theorem liquidReferenceDensityH2O_pos : 0 < liquidReferenceDensityH2O := by + unfold liquidReferenceDensityH2O; norm_num + +theorem curvatureDensityFraction_le_one (ρSolid ρLiquidRef : ℝ) : + curvatureDensityFraction ρSolid ρLiquidRef ≤ 1 := by + unfold curvatureDensityFraction clampMediumDensity + rw [max_le_iff] + exact ⟨by norm_num, min_le_left (1 : ℝ) (ρSolid / ρLiquidRef)⟩ + +theorem curvatureDensityFraction_nonneg (ρSolid ρLiquidRef : ℝ) : + 0 ≤ curvatureDensityFraction ρSolid ρLiquidRef := by + unfold curvatureDensityFraction clampMediumDensity + exact le_max_left _ _ + +theorem curvatureDensityFractionH2OIceIh_in_unit_interval : + 0 ≤ curvatureDensityFractionH2OIceIh ∧ + curvatureDensityFractionH2OIceIh ≤ 1 := by + constructor + · unfold curvatureDensityFractionH2OIceIh + exact curvatureDensityFraction_nonneg _ _ + · unfold curvatureDensityFractionH2OIceIh + exact curvatureDensityFraction_le_one _ _ + +theorem homogeneousCurvatureBudgetFromPhase_dilute (ξ : ℝ) : + homogeneousCurvatureBudgetFromPhase ξ 0 = 1 := by + unfold homogeneousCurvatureBudgetFromPhase homogeneousCurvatureBudgetAtXi + clampMediumDensity + simp + +theorem homogeneousCurvatureBudgetFromPhase_condensed (ξ : ℝ) : + homogeneousCurvatureBudgetFromPhase ξ 1 = curvatureBudgetAtXi ξ := by + unfold homogeneousCurvatureBudgetFromPhase homogeneousCurvatureBudgetAtXi + curvatureBudgetAtXi clampMediumDensity + simp + +theorem homogeneousCurvatureBudgetFromPhase_eq_homogeneous (ξ ρ : ℝ) : + homogeneousCurvatureBudgetFromPhase ξ ρ = homogeneousCurvatureBudgetAtXi ξ ρ := rfl + +/-! +## Orbital phase geometry (planetary bulk + inverse-square local curvature) + +The condensed-phase pipeline generalizes to flyby readouts: the geometry witness is +`(M, R, r_encounter)` instead of a unit cell. Bulk planetary density is fully condensed +(ρ_bulk = 1); the local inverse-square slot `(R/r)²` is blended with bulk dominance +`w_bulk = 1 / (1 + (r/R)²)` (macroscopic bulk limit of +`scripts/hqiv_homogeneous_curvature_feedback.py`). + +At large encounter radius ρ → 0 and the curvature mass delta vanishes (GR limit). +-/ + +/-- Orbital geometry witness: central mass, equatorial radius, encounter distance [m]. -/ +structure OrbitalPhaseWitness where + label : String + centralMassKg : ℝ + radiusM : ℝ + encounterRadiusM : ℝ + +/-- Bulk-dominated inverse-square weight (size fraction = 1 for planetary samples). -/ +noncomputable def orbitalBulkDominanceWeight (rBulk rEncounter : ℝ) : ℝ := + if 0 < rBulk then 1 / (1 + (rEncounter / rBulk) ^ (2 : ℕ)) else 0 + +/-- Local curvature fraction vs surface reference: clamp((R/r)²). -/ +noncomputable def orbitalLocalCurvatureFraction (rBulk rEncounter : ℝ) : ℝ := + if 0 < rEncounter then clampMediumDensity ((rBulk / rEncounter) ^ (2 : ℕ)) else 0 + +/-- +Effective orbital curvature density ρ ∈ [0,1]: +`ρ_eff = w_bulk·ρ_bulk + (1 − w_bulk)·ρ_local` with ρ_bulk = 1 (condensed body). +-/ +noncomputable def orbitalCurvatureDensityFraction (w : OrbitalPhaseWitness) : ℝ := + let wBulk := orbitalBulkDominanceWeight w.radiusM w.encounterRadiusM + let ρLocal := orbitalLocalCurvatureFraction w.radiusM w.encounterRadiusM + clampMediumDensity (wBulk + (1 - wBulk) * ρLocal) + +/-- Homogeneous curvature budget at propagation ξ from orbital phase geometry. -/ +noncomputable def homogeneousCurvatureBudgetFromOrbital (ξ : ℝ) (w : OrbitalPhaseWitness) : ℝ := + homogeneousCurvatureBudgetFromPhase ξ (orbitalCurvatureDensityFraction w) + +/-- Dimensionless mass/curvature delta above dilute limit: `B_hom(ξ, ρ_orb) − 1`. -/ +noncomputable def orbitalCurvatureMassDeltaFraction (ξ : ℝ) (w : OrbitalPhaseWitness) : ℝ := + homogeneousCurvatureBudgetFromOrbital ξ w - 1 + +/-- Earth mass [kg] (IAU nominal). -/ +noncomputable def earthMassKg : ℝ := 5.9722e24 + +/-- Earth equatorial radius [m]. -/ +noncomputable def earthRadiusM : ℝ := 6.378137e6 + +/-- Earth orbital witness at encounter distance `r` from centre. -/ +noncomputable def orbitalPhaseWitnessEarth (encounterRadiusM : ℝ) : OrbitalPhaseWitness := + { label := "Earth" + centralMassKg := earthMassKg + radiusM := earthRadiusM + encounterRadiusM := encounterRadiusM } + +theorem orbitalBulkDominanceWeight_nonneg (rBulk rEncounter : ℝ) : + 0 ≤ orbitalBulkDominanceWeight rBulk rEncounter := by + unfold orbitalBulkDominanceWeight + split_ifs with h + · exact div_nonneg (by norm_num) (add_nonneg (by norm_num) (sq_nonneg _)) + · norm_num + +theorem orbitalLocalCurvatureFraction_le_one (rBulk rEncounter : ℝ) : + orbitalLocalCurvatureFraction rBulk rEncounter ≤ 1 := by + unfold orbitalLocalCurvatureFraction + split_ifs with h + · unfold clampMediumDensity + rw [max_le_iff] + exact ⟨by norm_num, min_le_left _ _⟩ + · norm_num + +theorem orbitalCurvatureDensityFraction_le_one (w : OrbitalPhaseWitness) : + orbitalCurvatureDensityFraction w ≤ 1 := by + unfold orbitalCurvatureDensityFraction clampMediumDensity + rw [max_le_iff] + exact ⟨by norm_num, min_le_left _ _⟩ + +theorem orbitalCurvatureDensityFraction_nonneg (w : OrbitalPhaseWitness) : + 0 ≤ orbitalCurvatureDensityFraction w := by + unfold orbitalCurvatureDensityFraction clampMediumDensity + exact le_max_left _ _ + +theorem orbitalCurvatureMassDelta_zero_of_zero_density (ξ : ℝ) (w : OrbitalPhaseWitness) + (hρ : orbitalCurvatureDensityFraction w = 0) : + orbitalCurvatureMassDeltaFraction ξ w = 0 := by + unfold orbitalCurvatureMassDeltaFraction homogeneousCurvatureBudgetFromOrbital + rw [hρ, homogeneousCurvatureBudgetFromPhase_dilute] + ring + +theorem homogeneousCurvatureBudgetFromOrbital_eq_phase (ξ : ℝ) (w : OrbitalPhaseWitness) : + homogeneousCurvatureBudgetFromOrbital ξ w = + homogeneousCurvatureBudgetFromPhase ξ (orbitalCurvatureDensityFraction w) := rfl + +end Hqiv.QuantumChemistry diff --git a/Hqiv/QuantumChemistry/PhaseMaterialResponse.lean b/Hqiv/QuantumChemistry/PhaseMaterialResponse.lean new file mode 100644 index 0000000..74bab09 --- /dev/null +++ b/Hqiv/QuantumChemistry/PhaseMaterialResponse.lean @@ -0,0 +1,190 @@ +import Hqiv.Algebra.PhaseLiftDelta +import Hqiv.Physics.FanoResonance +import Hqiv.QuantumChemistry.CurvatureBondContact +import Hqiv.QuantumChemistry.PhaseGeometryDensity + +/-! +# Phase geometry → material response (n, ε_r, k_th, σ slot) + +Structural readouts extending `PhaseGeometryDensity` — no fitted potentials: + +* **Polarizability** from covalent binding softness and lattice α. +* **Clausius–Mossotti** → refractive index n, dielectric ε_r ≈ n². +* **Phonon thermal conductivity** k_th from binding stiffness, ρ, G_eff contact. +* **Ionic conductivity** σ slot (carrier fraction explicit; pure media → 0). +* **Molar heat capacity** C_p from contact-mode DOF × `B_hom`. +* **Latent heat** L_fusion from melt cohesive × tetrahedral shell release. +* **Dynamic viscosity** η (Eyring slot; solid → ∞). +* **Birefringence** Δn from hexagonal c/a CM split (ice Ih). + +Python mirror: `scripts/hqiv_phase_material_response.py`. +-/ + +namespace Hqiv.QuantumChemistry + +open Hqiv +open Hqiv.Algebra +open Hqiv.Physics +open Real + +noncomputable section + +/-- Shell-opening factor φ(3)/6 = 4/3 for oriented ice Ih (tetrahedral water). -/ +noncomputable def phaseOrientationCmFactorH2OIceIh : ℝ := (4 : ℝ) / 3 + +theorem phaseOrientationCmFactorH2OIceIh_eq_phaseLiftCoeff_three : + phaseOrientationCmFactorH2OIceIh = phaseLiftCoeff 3 := by + rw [phaseOrientationCmFactorH2OIceIh] + rw [Hqiv.Algebra.phaseLiftCoeff, Hqiv.phi_of_shell_closed_form, Hqiv.phiTemperatureCoeff_eq_two] + norm_num + +/-- Liquid H₂O local-field divisor: 1 − c_Rindler = 1 − γ/2 = 4/5. -/ +noncomputable def liquidLocalFieldDivisorH2O : ℝ := 1 - c_rindler_shared + +theorem liquidLocalFieldDivisorH2O_eq_four_fifths : + liquidLocalFieldDivisorH2O = (4 : ℝ) / 5 := by + rw [liquidLocalFieldDivisorH2O, c_rindler_shared_eq_one_fifth] + norm_num + +/-- +HQIV dimensionless polarizability scale (before ų conversion in Python): + +α_scale ∝ α · (4/8) · (r_span/a₀)³ · (E_Ryd/E_bond) · (1 + ρ·α_lattice). +-/ +noncomputable def hqivPolarizabilityScale + (rSpanRatio eBondEv ρ_curv : ℝ) : ℝ := + alpha * strongChannelFraction * rSpanRatio ^ 3 * + (13.605693122994 / max eBondEv 0.05) * (1 + ρ_curv * alpha) + +/-- +Clausius–Mossotti ratio (n²−1)/(n²+2) from mass density, formula weight, polarizability +volume [ų in Python; here a positive structural slot α_mol], and local-field divisor. +-/ +noncomputable def clausiusMossottiRatio + (ρ_g_cm3 mw_amu α_mol_angstrom3 coordDiv : ℝ) : ℝ := + let raw := (ρ_g_cm3 / mw_amu) * avogadroNumber * (α_mol_angstrom3 * angstromToCm ^ 3) / 3 + raw / max coordDiv 1e-6 + +/-- Oriented ice Ih CM factor on top of raw ratio. -/ +noncomputable def clausiusMossottiRatioH2OIceIh (ρ_g_cm3 α_mol : ℝ) : ℝ := + clausiusMossottiRatio ρ_g_cm3 18.015 α_mol 1 * phaseOrientationCmFactorH2OIceIh + +/-- Liquid H₂O CM ratio with disorder divisor 4/5. -/ +noncomputable def clausiusMossottiRatioH2OLiquid (α_mol : ℝ) : ℝ := + clausiusMossottiRatio 1 18.015 α_mol liquidLocalFieldDivisorH2O + +/-- n² from CM; valid when `cm < 1`. -/ +noncomputable def refractiveIndexSquaredFromCM (cm : ℝ) : ℝ := + if cm < 1 then (1 + 2 * cm) / (1 - cm) else 1 + +noncomputable def refractiveIndexFromCM (cm : ℝ) : ℝ := + Real.sqrt (max 1 (refractiveIndexSquaredFromCM cm)) + +noncomputable def dielectricConstantFromRefractiveIndex (n : ℝ) : ℝ := n ^ 2 + +theorem dielectricConstantFromRefractiveIndex_eq_n_sq (n : ℝ) : + dielectricConstantFromRefractiveIndex n = n ^ 2 := rfl + +theorem refractiveIndexSquaredFromCM_ge_one + (cm : ℝ) (hcm : 0 ≤ cm ∧ cm < 1) : + 1 ≤ refractiveIndexSquaredFromCM cm := by + unfold refractiveIndexSquaredFromCM + by_cases h : cm < 1 + · have hden : 0 < 1 - cm := sub_pos.mpr hcm.2 + simp [h] + rw [one_le_div_iff] + exact Or.inl ⟨hden, by nlinarith [hcm.1]⟩ + · simp [h] + +theorem refractiveIndexFromCM_ge_one + (cm : ℝ) (hcm : 0 ≤ cm ∧ cm < 1) : + 1 ≤ refractiveIndexFromCM cm := by + have h1 := refractiveIndexSquaredFromCM_ge_one cm hcm + dsimp [refractiveIndexFromCM] + rw [one_le_sqrt] + exact le_max_left 1 (refractiveIndexSquaredFromCM cm) + +/-- +Phonon thermal conductivity slot [W/(m·K) structural units in Python]: + +k_th = (1/3) ρ c_spec v_s ℓ G_eff(θ) B_hom. +-/ +noncomputable def phononThermalConductivitySlot + (ρ_kg c_spec v_s ell geff b_hom : ℝ) : ℝ := + (1 / 3 : ℝ) * ρ_kg * c_spec * v_s * ell * geff * b_hom + +theorem phononThermalConductivitySlot_pos + (ρ_kg c_spec v_s ell geff b_hom : ℝ) + (hρ : 0 < ρ_kg) (hc : 0 < c_spec) (hv : 0 < v_s) (hℓ : 0 < ell) + (hg : 0 < geff) (hb : 0 < b_hom) : + 0 < phononThermalConductivitySlot ρ_kg c_spec v_s ell geff b_hom := by + unfold phononThermalConductivitySlot + positivity + +/-- +Ionic conductivity slot: zero without explicit carriers (pure-water limit). +-/ +noncomputable def ionicConductivitySlot (carrierFraction : ℝ) (σ_scale : ℝ) : ℝ := + carrierFraction * σ_scale + +theorem ionicConductivitySlot_zero_of_zero_carrier (σ_scale : ℝ) : + ionicConductivitySlot 0 σ_scale = 0 := by + unfold ionicConductivitySlot + ring + +/-- Dielectric from phase-derived CM at ice Ih (structural composition). -/ +noncomputable def dielectricConstantH2OIceIhFromCM (cm : ℝ) : ℝ := + dielectricConstantFromRefractiveIndex (refractiveIndexFromCM cm) + +theorem dielectricConstantH2OIceIhFromCM_eq_n_sq (cm : ℝ) : + dielectricConstantH2OIceIhFromCM cm = + refractiveIndexFromCM cm ^ 2 := by + unfold dielectricConstantH2OIceIhFromCM dielectricConstantFromRefractiveIndex + ring + +/-- Thermal slot dressed by homogeneous curvature at bulk H₂O contact ξ. -/ +noncomputable def thermalConductivityH2OBulkSlot + (ξ ρ_curv ρ_kg c_spec v_s ell θ : ℝ) : ℝ := + phononThermalConductivitySlot ρ_kg c_spec v_s ell + (outsideContactCoupling θ) (homogeneousCurvatureBudgetFromPhase ξ ρ_curv) + +/-- Molar heat capacity slot: (3 n_atoms) R × (1 + α·𝟙_solid) × B_hom. -/ +noncomputable def molarHeatCapacitySlot (nAtoms b_hom : ℝ) (solid : Bool) : ℝ := + let dof := 3 * nAtoms * (if solid then 1 + alpha else 1) + dof * 8.314462618 * b_hom + +/-- Squared shell-opening factor on latent heat (φ(3)/6)² / (1+α). -/ +noncomputable def latentHeatShellReleaseFactor : ℝ := + phaseOrientationCmFactorH2OIceIh ^ 2 / (1 + alpha) + +/-- Latent heat slot L_f = E_melt · N_A · n_inter · releaseFactor (structural units). -/ +noncomputable def latentHeatFusionSlot (eMeltEv nInter : ℝ) : ℝ := + eMeltEv * 96485.33212 * nInter * latentHeatShellReleaseFactor + +/-- Hexagonal c/a split for CM birefringence: ±(c/a − 1)·c_Rindler/20 on isotropic CM. -/ +noncomputable def hexagonalCmSplitFactor (cOverA : ℝ) : ℝ := + (cOverA - 1) * c_rindler_shared / 20 + +noncomputable def hexagonalCmFactors (cOverA : ℝ) : ℝ × ℝ := + let s := hexagonalCmSplitFactor cOverA + (1 + s, max (1 - s) 1e-6) + +/-- Birefringence Δn slot = |n(f₊) − n(f₋)| (Python evaluates n from CM). -/ +noncomputable def birefringenceDeltaNSlot (nOrdinary nExtraordinary : ℝ) : ℝ := + |nOrdinary - nExtraordinary| + +theorem birefringenceDeltaNSlot_nonneg (nOrdinary nExtraordinary : ℝ) : + 0 ≤ birefringenceDeltaNSlot nOrdinary nExtraordinary := abs_nonneg _ + +/-- Dynamic viscosity slot (Pa·s): zero for solid flag, positive for liquid inputs. -/ +noncomputable def dynamicViscositySlot (solid : Bool) (η_liquid : ℝ) : ℝ := + if solid then 0 else η_liquid + +theorem dynamicViscositySlot_zero_of_solid (η_liquid : ℝ) : + dynamicViscositySlot true η_liquid = 0 := by + unfold dynamicViscositySlot + simp + +end + +end Hqiv.QuantumChemistry diff --git a/lakefile.toml b/lakefile.toml index 009e584..b9ddbea 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -234,6 +234,163 @@ globs = [ "Hqiv.Topology.SignedShellBudget", ] + +[[lean_lib]] +name = "paper_nucleon_binding" +# Build target for papers/nucleon_binding/ (import closure of cited Lean modules). +# Regenerate: python3 scripts/paper_nucleon_binding_globs.py +# Build: lake build paper_nucleon_binding +# 146 modules in paper_nucleon_binding import closure +globs = [ + "Hqiv.Algebra.CliffordCl06SixDimension", + "Hqiv.Algebra.CliffordCl06SixIdeal", + "Hqiv.Algebra.CliffordCl06SixSpinorGammaMatInt", + "Hqiv.Algebra.CliffordCl06SixSpinorGammaMonomialLinearIndependent", + "Hqiv.Algebra.CliffordCl06SixSpinorMonomialMatrixData", + "Hqiv.Algebra.CliffordCl06SixStandardSpinorMatLiftSurjective", + "Hqiv.Algebra.CliffordCl06SixStandardSpinorRho", + "Hqiv.Algebra.CliffordMinimalIdeal", + "Hqiv.Algebra.CliffordSixImaginaryScaffold", + "Hqiv.Algebra.G2Embedding", + "Hqiv.Algebra.OctonionAxisAngles", + "Hqiv.Algebra.OctonionBasics", + "Hqiv.Algebra.OctonionLeftMulSquare", + "Hqiv.Algebra.OctonionSpinorCarrier", + "Hqiv.Algebra.PhaseLiftDelta", + "Hqiv.Algebra.SMEmbedding", + "Hqiv.Algebra.ShellResidueCRT", + "Hqiv.Algebra.Triality", + "Hqiv.Algebra.WeakFromLeftMulOctonion", + "Hqiv.Conservations", + "Hqiv.Generators", + "Hqiv.GeneratorsFromAxioms", + "Hqiv.Geometry.AuxFieldRapidityNullBridge", + "Hqiv.Geometry.AuxiliaryField", + "Hqiv.Geometry.BondedHorizonCasimir", + "Hqiv.Geometry.ComptonNuclearTorus", + "Hqiv.Geometry.ContinuumMetricGradient", + "Hqiv.Geometry.ContinuumSpacetimeChart", + "Hqiv.Geometry.HQVMCausalChart", + "Hqiv.Geometry.HQVMContinuumMetricBridge", + "Hqiv.Geometry.HQVMetric", + "Hqiv.Geometry.LatticePointMaxAbsShells", + "Hqiv.Geometry.Now", + "Hqiv.Geometry.NuclearTorusPerturbation", + "Hqiv.Geometry.OctonionicLightCone", + "Hqiv.Geometry.QuaternionMaxwellS3OMaxwellS4Spectral", + "Hqiv.Geometry.S7MetahorizonCasimir", + "Hqiv.Geometry.SpacetimeMinkowski11Embed4", + "Hqiv.Geometry.SphericalHarmonicsBridge", + "Hqiv.Geometry.UniverseAge", + "Hqiv.MatrixLieBracket", + "Hqiv.OctonionLeftMultiplication", + "Hqiv.Physics.Action", + "Hqiv.Physics.ActionHolonomyGlue", + "Hqiv.Physics.BBNEpochEvolution", + "Hqiv.Physics.BBNEpochNetwork", + "Hqiv.Physics.BBNNetworkFromWeights", + "Hqiv.Physics.BaryogenesisCore", + "Hqiv.Physics.BaryogenesisEtaPaper", + "Hqiv.Physics.BaryogenesisWitness", + "Hqiv.Physics.BoundStates", + "Hqiv.Physics.BraneBulkFanoTruss", + "Hqiv.Physics.ChargedLeptonResonance", + "Hqiv.Physics.ComptonHorizonPhase", + "Hqiv.Physics.ComptonIRWindow", + "Hqiv.Physics.ConservedContentMassBridge", + "Hqiv.Physics.ContinuousXiCoupling", + "Hqiv.Physics.ContinuousXiPath", + "Hqiv.Physics.ContinuumOmaxwellClosure", + "Hqiv.Physics.DerivedGaugeAndLeptonSector", + "Hqiv.Physics.DerivedNucleonMass", + "Hqiv.Physics.DiscretePlaquetteHolonomy", + "Hqiv.Physics.DynamicBBNBaryogenesis", + "Hqiv.Physics.DynamicBetaIsotope", + "Hqiv.Physics.DynamicIsotopeStability", + "Hqiv.Physics.DynamicNucleonPN", + "Hqiv.Physics.FanoDetuningFirstOrder", + "Hqiv.Physics.FanoLine", + "Hqiv.Physics.FanoOmaxwellSpectrum", + "Hqiv.Physics.FanoResonance", + "Hqiv.Physics.FanoTrialityDetuningScaffold", + "Hqiv.Physics.Forces", + "Hqiv.Physics.G2AutomorphismEnergyCost", + "Hqiv.Physics.GRFromMaxwell", + "Hqiv.Physics.GlobalDetuning", + "Hqiv.Physics.HQIVNuclei", + "Hqiv.Physics.HadronMassReadout", + "Hqiv.Physics.HomogeneousCurvatureSecondOrder", + "Hqiv.Physics.HopfShellBeltramiMassBridge", + "Hqiv.Physics.HorizonBlackbodySpectrum", + "Hqiv.Physics.HyperchargePathBarrierScaffold", + "Hqiv.Physics.InformationalEnergyMass", + "Hqiv.Physics.LapseMassReadout", + "Hqiv.Physics.LeptonGenerationLockin", + "Hqiv.Physics.LightConeMaxwellQFTBridge", + "Hqiv.Physics.MassFromSpinorRho", + "Hqiv.Physics.MetaHorizonExcitedStates", + "Hqiv.Physics.MetaHorizonTrappedPlanckMass", + "Hqiv.Physics.ModalFrequencyHorizon", + "Hqiv.Physics.ModifiedMaxwell", + "Hqiv.Physics.NaturalUnitMeVTheory", + "Hqiv.Physics.NeutronBindingStabilityScaffold", + "Hqiv.Physics.NeutronLifetimeMethod", + "Hqiv.Physics.NuclearAndAtomicSpectra", + "Hqiv.Physics.NuclearCausticBinding", + "Hqiv.Physics.NuclearCurvatureBinding", + "Hqiv.Physics.NuclearOutsideTemperatureDynamics", + "Hqiv.Physics.OMaxwellAlgebraSeed", + "Hqiv.Physics.OctonionicZeta", + "Hqiv.Physics.PostAlphaBindingGeometry", + "Hqiv.Physics.QuarkMetaResonance", + "Hqiv.Physics.QuarterPeriodRelaxation", + "Hqiv.Physics.ReadoutGaugeSeed", + "Hqiv.Physics.SM_GR_Unification", + "Hqiv.Physics.ScaleWitness", + "Hqiv.Physics.SphereProjectedMassTransfer", + "Hqiv.Physics.SpinStatistics", + "Hqiv.Physics.SpinStatisticsOperatorBridge", + "Hqiv.Physics.SurfaceWaveSelfClock", + "Hqiv.Physics.TrialityRapidityWellEquivalence", + "Hqiv.Physics.TuftShellChart", + "Hqiv.Physics.WeakFanoHopfBridge", + "Hqiv.ProteinResearch.AtomEnergyOSHoracleBridge", + "Hqiv.QuantumChemistry.BondStateNetwork", + "Hqiv.QuantumChemistry.CurvatureBondContact", + "Hqiv.QuantumChemistry.DynamicBindingChart", + "Hqiv.QuantumChemistry.FiniteSiteQuantumChemistry", + "Hqiv.QuantumChemistry.LiH", + "Hqiv.QuantumChemistry.LiHDerivation", + "Hqiv.QuantumChemistry.PhaseAllotropeDerivation", + "Hqiv.QuantumChemistry.PhaseGeometryDensity", + "Hqiv.QuantumChemistry.PhaseMaterialResponse", + "Hqiv.QuantumComputing.DigitalGates", + "Hqiv.QuantumComputing.DiscreteQuantumState", + "Hqiv.QuantumComputing.OSHoracle", + "Hqiv.QuantumMechanics.BornMeasurementFinite", + "Hqiv.QuantumMechanics.CCRFiniteDimObstruction", + "Hqiv.QuantumMechanics.ContinuumManyBodyQFTScaffold", + "Hqiv.QuantumMechanics.HorizonFreeFieldScaffold", + "Hqiv.QuantumMechanics.HorizonLimitedQM_QFT_Closure", + "Hqiv.QuantumMechanics.HorizonLimitedRenormLocality", + "Hqiv.QuantumMechanics.IntervalMaxOperatorCommutator", + "Hqiv.QuantumMechanics.LocalAlgebraNetScaffold", + "Hqiv.QuantumMechanics.MinkowskiFieldOperatorScaffold", + "Hqiv.QuantumMechanics.MonogamyTangles", + "Hqiv.QuantumMechanics.MonogamyTanglesPhiConditions", + "Hqiv.QuantumMechanics.PatchIntervalMaxSmeared", + "Hqiv.QuantumMechanics.PatchQFTBridge", + "Hqiv.QuantumMechanics.PauliCommutatorExample", + "Hqiv.QuantumOptics.HorizonQED", + "Hqiv.SO8ClosureSymbolic", + "Hqiv.Topology.DiscreteCurvatureChannel", + "Hqiv.Topology.DiscreteNullLatticeComplex", + "Hqiv.Topology.DiscretePhaseEvolution", + "Hqiv.Topology.HopfShellComplex", + "Hqiv.Topology.SignedShellBudget", +] + + [[lean_lib]] name = "paper_sm_lagrangian" # Legacy alias for paper_tuft_sm_lagrangian. diff --git a/scripts/bundle_nucleon_binding_scripts.py b/scripts/bundle_nucleon_binding_scripts.py new file mode 100644 index 0000000..b17a575 --- /dev/null +++ b/scripts/bundle_nucleon_binding_scripts.py @@ -0,0 +1,148 @@ +#!/usr/bin/env python3 +"""Refresh papers/nucleon_binding/scripts/ and scripts.zip for Zenodo upload. + +Copies every paper-cited entry script plus its ``hqiv_*`` import closure from +``scripts/``, mirrors ``hqiv_lab/`` and ``pyproject.toml``, writes +``MANIFEST.sha256``, and rebuilds ``papers/nucleon_binding/scripts.zip``. + +Usage (from repository root): + python3 scripts/bundle_nucleon_binding_scripts.py +""" +from __future__ import annotations + +import ast +import hashlib +import os +import shutil +import zipfile +from collections import deque +from pathlib import Path + +REPO = Path(__file__).resolve().parents[1] +SCRIPTS_ROOT = REPO / "scripts" +DEST = REPO / "papers" / "nucleon_binding" / "scripts" +ZIP_PATH = REPO / "papers" / "nucleon_binding" / "scripts.zip" + +ENTRY_SCRIPTS = [ + "hqiv_isotope_stability_halflife.py", + "hqiv_dynamic_beta_isotope.py", + "hqiv_isotope_pdg_benchmark.py", + "hqiv_nuclear_outside_temperature_dynamics.py", + "hqiv_bond_state_network.py", + "hqiv_nuclear_caustic_binding.py", + "hqiv_nuclear_inside_outside_binding.py", + "hqiv_dynamic_nucleon_pn.py", + "hqiv_phase_geometry_density.py", + "hqiv_thermodynamic_phase_from_tp.py", + "hqiv_homogeneous_curvature_feedback.py", + "hqiv_phase_material_response.py", + "test_hqiv_phase_material_response.py", + "hqiv_curvature_contact_network.py", + "hqiv_weak_fano_hopf_bridge.py", +] + +EXTRA_MIRROR = [ + "hqiv_lean_physics_primitives.py", + "hqiv_scale_witness.py", + "hqiv_nuclear_curvature_binding.py", + "hqiv_mass_calculator_core.py", + "hqiv_continuous_shell_mass.py", + "hqiv_excited_states.py", + "hqiv_coupling_linear_system.py", + "hqiv_shell_shape_geometry.py", + "hqiv_curvature_bond_state.py", + "hqiv_s2_binding_geometry.py", + "hqiv_dynamic_binding_chart.py", +] + + +def module_to_script(name: str) -> str | None: + if name.startswith("hqiv_") or name.startswith("test_hqiv_"): + return f"{name}.py" + return None + + +def imports_in(path: Path) -> list[str]: + tree = ast.parse(path.read_text(encoding="utf-8"), filename=str(path)) + out: list[str] = [] + for node in ast.walk(tree): + if isinstance(node, ast.Import): + out.extend(alias.name.split(".")[0] for alias in node.names) + elif isinstance(node, ast.ImportFrom) and node.module: + out.append(node.module.split(".")[0]) + return out + + +def script_closure() -> list[str]: + seen: set[str] = set() + queue: deque[str] = deque(ENTRY_SCRIPTS + EXTRA_MIRROR) + while queue: + rel = queue.popleft() + if rel in seen: + continue + src = SCRIPTS_ROOT / rel + if not src.is_file(): + continue + seen.add(rel) + for imp in imports_in(src): + dep = module_to_script(imp) + if dep: + queue.append(dep) + return sorted(seen) + + +def sha256_file(path: Path) -> str: + digest = hashlib.sha256() + with path.open("rb") as handle: + for chunk in iter(lambda: handle.read(1 << 20), b""): + digest.update(chunk) + return digest.hexdigest() + + +def copy_tree(src: Path, dest: Path) -> None: + if dest.exists(): + shutil.rmtree(dest) + shutil.copytree(src, dest) + + +def write_manifest(root: Path) -> None: + lines: list[str] = [] + for path in sorted(root.rglob("*")): + if not path.is_file(): + continue + rel = path.relative_to(root).as_posix() + lines.append(f"{sha256_file(path)} {rel}") + manifest = root / "MANIFEST.sha256" + manifest.write_text("\n".join(lines) + "\n", encoding="utf-8") + + +def build_zip() -> None: + if ZIP_PATH.exists(): + ZIP_PATH.unlink() + with zipfile.ZipFile(ZIP_PATH, "w", compression=zipfile.ZIP_DEFLATED) as archive: + for path in sorted(DEST.rglob("*")): + if path.is_file(): + archive.write(path, path.relative_to(DEST.parent).as_posix()) + + +def main() -> None: + os.makedirs(DEST, exist_ok=True) + for rel in script_closure(): + shutil.copy2(SCRIPTS_ROOT / rel, DEST / rel) + + copy_tree(REPO / "hqiv_lab", DEST / "hqiv_lab") + shutil.copy2(REPO / "pyproject.toml", DEST / "pyproject.toml") + + readme_src = DEST / "README.md" + if readme_src.is_file(): + pass + write_manifest(DEST) + build_zip() + n_scripts = len(list(DEST.glob("hqiv_*.py"))) + len(list(DEST.glob("test_hqiv_*.py"))) + print(f"copied {n_scripts} scripts + hqiv_lab/ + pyproject.toml -> {DEST}") + print(f"wrote {DEST / 'MANIFEST.sha256'} ({sum(1 for _ in (DEST / 'MANIFEST.sha256').open())} lines)") + print(f"created {ZIP_PATH} ({ZIP_PATH.stat().st_size} bytes)") + + +if __name__ == "__main__": + main() diff --git a/scripts/paper_nucleon_binding_globs.py b/scripts/paper_nucleon_binding_globs.py new file mode 100644 index 0000000..eaf0eea --- /dev/null +++ b/scripts/paper_nucleon_binding_globs.py @@ -0,0 +1,89 @@ +#!/usr/bin/env python3 +"""Emit `globs` for the `paper_nucleon_binding` Lake target. + +Import-closure of Lean modules cited in +``papers/nucleon_binding/hqiv_nucleon_binding_from_composite_trace.tex`` +(Appendix lean index). Paste output into ``lakefile.toml`` under +``[[lean_lib]] name = "paper_nucleon_binding"``. + +Usage (from repo root): + python3 scripts/paper_nucleon_binding_globs.py +""" +from __future__ import annotations + +import os +import re +from collections import deque + +REPO = os.path.dirname(os.path.dirname(os.path.abspath(__file__))) + +PAPER_ROOTS = ( + "Hqiv.Physics.ScaleWitness", + "Hqiv.Physics.NuclearCurvatureBinding", + "Hqiv.Physics.NuclearCausticBinding", + "Hqiv.Physics.HQIVNuclei", + "Hqiv.Physics.BoundStates", + "Hqiv.Physics.DerivedNucleonMass", + "Hqiv.Physics.QuarkMetaResonance", + "Hqiv.Physics.NeutronBindingStabilityScaffold", + "Hqiv.Physics.SpinStatistics", + "Hqiv.Physics.DynamicBetaIsotope", + "Hqiv.Physics.DynamicIsotopeStability", + "Hqiv.Physics.NeutronLifetimeMethod", + "Hqiv.Physics.WeakFanoHopfBridge", + "Hqiv.Physics.Forces", + "Hqiv.Physics.NuclearAndAtomicSpectra", + "Hqiv.Physics.NuclearOutsideTemperatureDynamics", + "Hqiv.Physics.DerivedGaugeAndLeptonSector", + "Hqiv.Physics.DynamicNucleonPN", + "Hqiv.Physics.HomogeneousCurvatureSecondOrder", + "Hqiv.QuantumChemistry.BondStateNetwork", + "Hqiv.QuantumChemistry.CurvatureBondContact", + "Hqiv.QuantumChemistry.PhaseAllotropeDerivation", + "Hqiv.QuantumChemistry.PhaseGeometryDensity", + "Hqiv.QuantumChemistry.PhaseMaterialResponse", + "Hqiv.Algebra.PhaseLiftDelta", +) + + +def mod_to_path(mod: str) -> str | None: + path = os.path.join(REPO, mod.replace(".", "/") + ".lean") + return path if os.path.isfile(path) else None + + +def read_hqiv_imports(path: str) -> list[str]: + out: list[str] = [] + with open(path, encoding="utf-8") as handle: + for line in handle: + match = re.match(r"import\s+(Hqiv\.\S+)", line.strip()) + if match: + out.append(match.group(1)) + return out + + +def import_closure() -> list[str]: + seen: set[str] = set() + queue: deque[str] = deque(PAPER_ROOTS) + while queue: + mod = queue.popleft() + if mod in seen: + continue + path = mod_to_path(mod) + if path is None: + continue + seen.add(mod) + queue.extend(read_hqiv_imports(path)) + return sorted(seen) + + +def main() -> None: + globs = import_closure() + print(f"# {len(globs)} modules in paper_nucleon_binding import closure") + print("globs = [") + for entry in globs: + print(f' "{entry}",') + print("]") + + +if __name__ == "__main__": + main()