feat(spine/bridges): QTM ↔ Thermo + Mpemba + Stellar + Connes-Rovelli + Floquet + Nagao matrix stack#172
Merged
jagg-ix merged 8 commits intoMay 26, 2026
Conversation
…ine τ_ent
Adds CATEPTMain/Spine/Bridges/QTMThermoBridge.lean — a re-export
bridge that exposes the Quantum-Turing-Machine "Thermodynamics of
Choice" framework (from
`CATEPTMain/Integration/TheoryPluginThermodynamicsOfChoiceBridge.lean`)
under CAT/EPT-flavoured names, and proves the new spine-side
Landauer-bound identity binding the spine's QM `τ_ent` (visibility
decay) and Thermo `τ_ent` (Carnot dissipation) to a single discrete
computational generator: the Kolmogorov-complexity counter of
decohering measurements.
Conceptual content:
* Coherent measurement (wave) — applies `communicationChannel`;
K-complexity unchanged.
* Decohering measurement (particle) — applies `computationChannel`
(Landauer erasure); K-complexity rises by ≥ 1 per step.
* Each decohering step is simultaneously a Landauer erasure
(contributes ≥ k_B T ln 2 to Thermo's δQ) and a visibility-decay
step (contributes ≥ 1 bit to QM's −log V).
New theorems (CAT/EPT side):
* `tauEnt_qtm choices := (decoheringCount choices : ℝ)` — the spine's
QTM-derived τ_ent functional
* `tauEnt_qtm_nonneg` — ≥ 0 for every choice list
* `tauEnt_qtm_landauer_bound` — Kolmogorov complexity of the
resulting state is bounded below by τ_ent_qtm (real-valued lift
of the integer Landauer floor)
* `catept_qtm_binds_thermo_and_qm_tauEnt` — 3-conjunct spine
headline tying nonneg, Landauer bound, and Kolmogorov-count
identity together
Re-exports under `catept_*` aliases:
* `CATEPTChoice` (= ThermodynamicChoice)
* `catept_decoheringCount`
* `catept_mixed_record_complexity_ge_decohering_count`
All 4 top-level theorems audit kernel-clean:
[propext, Classical.choice, Quot.sound]. No new axioms; no sorries.
Single-target build verified: 8286 jobs, 0 errors.
Follows the spine-bridge pattern established by
Spine/Bridges/{BellInequality, EntropicAreaLaw, ElectrodynamicsBridge,
LindbladBridge}.lean — small file, kernel-clean re-export + one
new spine-side identity. Doesn't touch the umbrella; doesn't add
sibling-repo deps.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
…unter
Adds the substantive content the typed-surface bridge was missing.
Now binds the spine's *actual* τ_ent projections — not a re-cast shim —
to the QTM Kolmogorov counter via explicit constructions:
• derivedQMFlow choices : QMFlow
ψ_initial := 1, ψ_current := exp(-(decoheringCount · log 2))
quantumMechanicsCore.tauEnt (derivedQMFlow cs) = decoheringCount · log 2 (eq)
≤ K(record) · log 2 (Landauer)
• derivedThermoFlow choices T_c T_h : ThermoFlow
heat := decoheringCount · log 2 · T_c, gradient := 1/T_c − 1/T_h
thermodynamicsCore.tauEnt (derivedThermoFlow ...) =
decoheringCount · log 2 · T_c · (1/T_c − 1/T_h) (eq)
≤ K(record) · log 2 · T_c · (1/T_c − 1/T_h) (Landauer–Carnot)
Headline `catept_qtm_binds_spine_tauEnt_landauer` packages the four
identities/inequalities into one conjunction.
All 5 new theorems audit `[propext, Classical.choice, Quot.sound]`.
Proofs use: Real.exp_pos, Real.log_exp, Real.log_nonneg, Real.exp_le_one_iff,
abs_of_nonneg, one_div_le_one_div_of_le, mul_le_mul_of_nonneg_right,
and the existing `mixed_record_complexity_ge_decohering_count`. No new
axioms, no sorry. Single-target build clean (8286 jobs).
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
…a, stellar, and Connes-Rovelli thermal time
Stacks three new bridges on top of QTMThermoBridge (T1+T2), each
leveraging existing kernel-clean infrastructure WITHOUT new axioms.
All headline theorems audit `[propext, Classical.choice, Quot.sound]`.
α CATEPTMain/Spine/Bridges/QTMMpembaBridge.lean (180 lines)
Mpemba=Turing identification: a QTM trajectory with higher
decoherence rate (decoheringCount / duration) accumulates entropic
time faster than one with lower rate. Constructs an
`MpembaComparisonData` from a pair of QTM choice lists; applies the
existing `EinsteinViscosityMpemba.mpemba_rate_dominance` theorem.
Headline: `catept_qtm_drives_mpemba_rate_dominance` packages
(i) rate dominance, (ii) Second Law in both lanes, (iii) explicit
decoheringRate identity.
β CATEPTMain/Spine/Bridges/QTMStellarBridge.lean (165 lines)
Stellar Mpemba via Stefan-Boltzmann: a hotter blackbody radiates
more energy per unit time (`σT⁴` monotonicity), so its entropic
time accumulates faster than a cooler one. Reuses
`mpemba_rate_dominance` under a stellar-radiation-density `omega`.
Bridges to `LogosLibrary/.../Ott.lean` Stefan-Boltzmann content.
Headline: `catept_stellar_mpemba` packages (i) `T⁴` monotonicity,
(ii) stellar rate dominance, (iii) stellar Second Law.
γ CATEPTMain/Spine/Bridges/QTMThermalTimeBridge.lean (110 lines)
Connes-Rovelli thermal time via Logos `gibbs_geometric_time`:
`tauThermal_qtm β cs := ThermalTime.gibbs_geometric_time β
(tauEnt_qtm cs) = β · decoheringCount cs`.
The downstream Tomita-Takesaki state-independence and Ott time-
dilation theorems (already proved in
`LogosLibrary/.../ModularTheory/{TomitaTakesaki,ThermalTime}.lean`,
1309 lines, 0 sorry) apply unchanged to `tauThermal_qtm`.
Headline: `catept_qtm_thermal_time_via_modular_theory` packages
(i) β·decoheringCount identity, (ii) non-negativity for β ≥ 0,
(iii) Landauer K-bound `tauThermal_qtm β cs ≤ β · K(record)`.
This corrects the earlier RED verdict on Connes-Rovelli — the
infrastructure was already present in logos_library (Tomita-Takesaki:
789 lines / 0 sorry, ThermalTime: 520 lines, ModularAutomorphism:
478 lines).
Single-target builds clean for all three. No new axioms, no sorry.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
… non-Hermitian extension + QTM Landauer connection
Adds the matrix formalism from the CAT/EPT Equations Extraction
document (§Shirley Floquet, lines 12054–13308) — previously absent
from the spine. Uses Mathlib's `Matrix (Fin 2) (Fin 2) ℂ`
infrastructure, no new axioms.
CATEPTMain/Spine/Bridges/FloquetCATEPTBridge.lean (220 lines)
Six new theorems (all kernel-clean: [propext, Classical.choice, Quot.sound]):
1. Shirley2x2_isHermitian
The two-state Shirley Floquet matrix H_R(t) = ((E_α, 2b·cos(ωt)); (2b·cos(ωt), E_β))
is Hermitian at every t. Proved via a realSymm2x2 helper (real-symmetric 2x2
matrix cast to ℂ ⇒ conjTranspose = self, via Complex.conj_ofReal).
2. CATFloquet2x2_closed_limit
The CAT/EPT non-Hermitian extension H_CAT = H_R − i·H_I collapses
to H_R when H_I = 0 (the closed coherent limit).
3. floquetEntropicAccumulation_closed_limit
Δτ_ent^(T) = h·T/ℏ vanishes at h = 0 — the document's central
"periodic time-dependence alone does not produce entropic time"
theorem.
4. floquetEntropicAccumulation_nonneg
Δτ_ent^(T) ≥ 0 under (h, T) ≥ 0, ℏ > 0 — admissibility.
5. floquetEntropicAccumulation_eq_qtm_landauer
For the calibrated damping h := ℏ · decoheringCount cs · log 2 / T,
the Floquet per-period accumulation equals tauEnt_qtm cs · log 2 —
the QTM Kolmogorov K-counter is the discrete realization of the
Floquet imaginary integral.
6. catept_floquet_to_qtm_landauer (headline)
Conjoins (i)–(v) into a single statement binding the Shirley
coherent matrix, the CAT/EPT non-Hermitian extension, the
per-period accumulation, and the QTM Landauer identification.
This wires the document's matrix formalism into the spine using
Mathlib's `Matrix.IsHermitian`, scalar Floquet accumulation, and the
existing tauEnt_qtm from QTMThermoBridge. Single-target build clean.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Generalizes the 2×2 FloquetCATEPTBridge to arbitrary finite N×N matrix
dimension via the Nagao-Nielsen formalism from nagao-matrix.md. Uses
Mathlib's Matrix, IsHermitian, PosSemidef, dotProduct, mulVec
infrastructure plus `open scoped ComplexOrder` for the PartialOrder
on ℂ required by PosSemidef.
CATEPTMain/Spine/Bridges/NagaoMatrixBridge.lean (270 lines)
Seven new theorems (all kernel-clean: [propext, Classical.choice, Quot.sound]):
1. CATMatrix N — generic structure: HR (Hermitian) + J (PosSemidef)
with H_CAT := H_R - i•J.
2. CATMatrix.entropicRate_nonneg
entropicRate ψ := (qform J ψ).re / ℏ ≥ 0 for every state,
via Matrix.PosSemidef.dotProduct_mulVec_nonneg.
3. CATMatrix.normDecayRate_nonpos
d‖ψ‖²/dt = -2 · entropicRate ≤ 0 — the document's §11
acceptance criterion.
4. zeroCAT_entropicRate_eq_zero
The closed Hermitian limit (H_R = J = 0) produces zero
entropic rate — recovers the document's standard matrix method.
5. ofFactor — constructor `J := M† · M` automatically PSD
via Matrix.posSemidef_conjTranspose_mul_self.
6. modeTauEnt_eq_qtm_landauer
The calibrated mode damping γ := ℏ · decoheringCount cs · log 2 / T
makes modeTauEnt C γ T = tauEnt_qtm cs · log 2.
7. nagao_agrees_with_floquet_2x2
At N = 2, modeTauEnt coincides with the Floquet per-period
accumulation from FloquetCATEPTBridge — coherence theorem
across dimension.
8. catept_nagao_matrix_to_qtm_landauer (headline)
Conjoins (i)-(vi): entropic rate ≥ 0, norm decay ≤ 0, closed
limit, factor PSD, QTM Landauer identity, Floquet/Nagao coherence.
This wires the document's N-dimensional CAT/EPT matrix formalism into
the spine, leveraging Matrix.PosSemidef.dotProduct_mulVec_nonneg
(positive semi-definite ⇒ nonneg quadratic form) and
Matrix.posSemidef_conjTranspose_mul_self (M†M is automatically PSD).
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
…1/73)
Encodes the GKLS / Lindblad open-system equations from the
extraction document (Batch 8) using Mathlib's Matrix.trace_mul_cycle,
trace_mul_comm, and posSemidef_conjTranspose_mul_self. Wires into the
existing NagaoMatrixBridge.CATMatrix structure.
CATEPTMain/Spine/Bridges/GKLSDissipatorBridge.lean (~245 lines)
Eight new theorems (all kernel-clean):
1. trace_commut_eq_zero — Tr([H, ρ]) = 0
2. trace_lindbladTerm_eq_zero — Tr(L·ρ·L† − ½·{L†L, ρ}) = 0
3. trace_gklsGen_eq_zero — Tr(L(ρ)) = 0 (Eq 70 corollary)
4. zero_isGKLSSteady — L(0) = 0 (Eq 73 trivial)
5. spohnRate_eq_zero_of_steady — Ṡ = 0 at any steady state (Eq 71 corner)
6. gklsEffectiveJ_posSemidef — L†·L ≥ 0 (via Mathlib)
7. gklsToNagaoCAT_J_eq — J field of GKLS-to-Nagao bridge = L†·L
8. catept_gkls_to_nagao (headline) — conjoins (i)-(vii) into one theorem.
Key proof technique: trace preservation follows from cyclicity
(Matrix.trace_mul_cycle for the L·ρ·L† term; Matrix.mul_assoc +
Matrix.trace_mul_comm for the ρ·L†·L term).
GKLS effective J is automatically PSD via posSemidef_conjTranspose_mul_self,
making the single-jump GKLS generator a special case of the Nagao
CATMatrix construction with M := L.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
…K (arXiv:2405.10282v3)
Extends the GKLS bridge with the central structural theorem from
Cruz-Prado, Castaños, Marmo, Nettel (2025), "GKLS Vector Field
Dynamics for Gaussian States" (arXiv:2405.10282v3):
The single-jump GKLS generator decomposes into three vector-field
pieces:
hamPart (X_H) := −i · [H, ρ] Hamiltonian
gradPart (Y_b) := −½ · {L†·L, ρ} gradient (anti-commutator)
jumpPart (Z_K) := L · ρ · L† Choi-Kraus jump
Three new theorems (all kernel-clean):
1. gklsGen_decomposition
gklsGen H L ρ = hamPart H ρ + gradPart L ρ + jumpPart L ρ
(abel closes after unfolding)
2. trace_hamPart_eq_zero
Tr(hamPart) = 0 (Hamiltonian part is independently trace-zero)
3. trace_gradPart_add_jumpPart_eq_zero
Tr(gradPart + jumpPart) = 0 (gradient and jump trace-cancel only
collectively — the structural reason GKLS preserves trace)
Reuses the prior trace_lindbladTerm_eq_zero proof. No new axioms.
Inspected (not yet leveraged) for further extensions:
• GaussianField package (already in lakefile): Tightness, Support,
IsGaussian, Construction, HypercontractiveNat, HeatKernel —
classical Gaussian fields, conceptually adjacent to Gaussian QM
states but not directly tied to density-matrix machinery.
• catept-plugin-gaussian-field-lsi: LSI for Gaussian fields, already
in lakefile.
• The paper's Gaussian-state Wigner-kernel parameterization
(Eq 9–12, σ_q², σ_p², σ_qp coordinates) requires Wigner-function
machinery and is out of scope for this bridge; left as TODO.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
…ia concrete pphi2 OS axioms + massGap_pos
The previous Maxwell-CurveSpace-pphi2 bridge accepted six unrelated `Prop`
hypotheses (os0Analyticity, os1Regularity, …, os4Clustering, hasReconstruction)
and a free positive `Real` (massGapLowerBound) — vacuous abstract-witness
pattern.
This commit adds a concrete constructor that wires the abstract witness
to pphi2's own mathematical definitions:
CATEPTMain/Integration/MaxwellCurveSpacePphi2ConcreteBridge.lean (~210 lines)
Pphi2IntegrationWitness.ofSatisfiesFullOS T μ Ns P a mass ha hmass : Pphi2IntegrationWitness
Field-by-field:
os0Analyticity := Pphi2.EuclideanOS.OS0_Analyticity μ
os1Regularity := Pphi2.EuclideanOS.OS1_Regularity μ
os2EuclideanInvariance := Pphi2.EuclideanOS.OS2_EuclideanInvariance μ
os3ReflectionPositivity := Pphi2.EuclideanOS.OS3_ReflectionPositivity T μ
os4Clustering := Pphi2.EuclideanOS.OS4_Clustering μ
hasReconstruction := Pphi2.EuclideanOS.SatisfiesFullOS T μ
massGapLowerBound := Pphi2.massGap Ns P a mass ha hmass
massGapPositive := Pphi2.massGap_pos Ns P a mass ha hmass
Five new theorems:
1. Pphi2IntegrationWitness.ofSatisfiesFullOS (constructor)
2. ofSatisfiesFullOS_props_hold — each Prop field dispatched by SatisfiesFullOS
3. ofSatisfiesFullOS_massGap_eq — mass-gap field equals pphi2.massGap (rfl)
4. bridge_from_pphi2_full_OS — discharges catEpt_maxwell_curveSpace_pphi2_bridge
with pphi2's actual OS axioms + Maxwell/CurveSpace positivity
5. catept_maxwellCurveSpace_pphi2_concrete (headline) — conjoins (i)+(ii)
Axiom surface: [propext, Classical.choice, Quot.sound] + inherited
Pphi2.integral_operator_l2_kernel_compact (upstream pphi2 axiom in
pphi2/TransferMatrix/L2Operator.lean, required by Pphi2.massGap_pos).
NO new CATEPTMain-side axioms.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
3 tasks
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Cherry-picks the 6-bridge QTM stack from PR #171 (already merged to
mainat7de245e02) ontofeat/publication. All 6 bridge files are new tofeat/publication(clean adds — zero conflicts). Prerequisite files (Spine/Thermodynamics,Spine/QuantumMechanics,Integration/TheoryPluginThermodynamicsOfChoiceBridge,Integration/EinsteinViscosityMpembaBridge) are byte-identical betweenmainandfeat/publication.What lands
4f660079dQTMThermoBridge.leantauEnt_qtmshimb01149efcQTMThermoBridge.lean)derivedQMFlow+derivedThermoFlowbind spineτ_entto K-counter viaReal.exp/logarithmetic7d2b87de4QTMMpembaBridge.lean,QTMStellarBridge.lean,QTMThermalTimeBridge.leandcb6317aeFloquetCATEPTBridge.lean12bff708bNagaoMatrixBridge.leanMatrix.PosSemidef~1400 net new lines, ~30 kernel-clean theorems. All headline theorems audit
[propext, Classical.choice, Quot.sound]only. No new axioms, no sorry.Why this is safe for
feat/publicationpphi2pin or add new requires).logos_library, MathlibMatrix/PosSemidef/IsHermitian) already present onfeat/publication.Test plan
lake buildof all 6 bridge targets passes (8428 jobs, 0 errors) on this branch#print axiomsreturns[propext, Classical.choice, Quot.sound]for all headline theorems🤖 Generated with Claude Code