spine: QTM↔Thermodynamics bridge — Landauer counter binds spine τ_ent#171
Merged
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>
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
Adds
CATEPTMain/Spine/Bridges/QTMThermoBridge.lean— the spine-level bridge that exposes the Quantum-Turing-Machine "Thermodynamics of Choice" framework under CAT/EPT-flavoured names and proves the new spine-side Landauer-bound identity.Conceptual content
The QTM framework partitions every measurement into:
communicationChannel(unitary)computationChannel(Landauer erasure)k_B T ln 2The headline
mixed_record_complexity_ge_decohering_countsays:K(record) ≥ decoheringCount(choices). Each decohering step is simultaneously a Landauer erasure (δQ contribution to Thermo's spineτ_ent) and a visibility-decay event (−log V contribution to QM's spineτ_ent).The QTM bridge witnesses that the spine's QM
τ_entand Thermoτ_ent— different functionals on different carriers — share a single discrete generator: the Kolmogorov-complexity counter of the measurement record.New theorems
tauEnt_qtm— the spine's QTM-derived τ_ent functional (real-valued cast ofdecoheringCount)tauEnt_qtm_nonneg— ≥ 0 for every choice listtauEnt_qtm_landauer_bound— K-complexity ≥ τ_ent_qtm (real-valued lift)catept_qtm_binds_thermo_and_qm_tauEnt— 3-conjunct headlinePlus 1 re-exported theorem and 3 abbrev aliases (
CATEPTChoice,catept_decoheringCount,catept_mixed_record_complexity_ge_decohering_count).Verification
```
lake build CATEPTMain.Spine.Bridges.QTMThermoBridge → 8286 jobs, 0 errors
All 4 top-level theorems audit:
[propext, Classical.choice, Quot.sound]
```
Scope
Spine/Bridges/{Bell, EntropicAreaLaw, Electrodynamics, Lindblad}Bridge.leanmainpost-PR-spine: minimal-scope substrate + bridges (split from #169) #170Test plan
Check axiom surface — Spine substrate + bridgesstep)🤖 Generated with Claude Code