feat(spine/bridges): scalar Lindblad ↔ QM τ_ent bridge (port from main)#173
Merged
jagg-ix merged 1 commit intoMay 26, 2026
Merged
Conversation
Brings the one substantive non-vacuous file from main that was missing from feat/publication. All 7 headline theorems audit [propext, Classical.choice, Quot.sound] only — no new axioms, no sorry, no abstract Prop-witness pattern. CATEPTMain/Spine/Bridges/LindbladBridge.lean (191 lines) Imports already present on feat/publication (UnifiedTheory pin identical to main): - CATEPTMain.Spine.QuantumMechanics - UnifiedTheory.LayerB.LindbladDecoherence Distinct from GKLSDissipatorBridge.lean (matrix-level GKLS, on publication via PR #172). This bridge operates at the scalar spine-level: tauEnt_lindblad rate t := -log(γ(t)) (where γ(t) = exp(-Γt)) = Γ · t Seven new theorems: 1. tauEnt_lindblad_eq_Gamma_t — closed form τ_ent = Γ·t 2. tauEnt_lindblad_nonneg — second law 3. tauEnt_lindblad_monotone — monotone in t 4. catept_lindblad_preserves_populations (UnifiedTheory re-export) 5. catept_lindblad_contracts_coherence 6. catept_observable_approaches_classical 7. catept_qm_tauEnt_from_lindblad — headline identity Provides the scalar reading complementing GKLSDissipatorBridge's matrix algebra, both wiring into the same QM τ_ent on the spine. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
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
Ports
CATEPTMain/Spine/Bridges/LindbladBridge.leanfrommaintofeat/publication— the single substantive non-vacuous file present on main but not on publication after PR #172 merged.What this adds
CATEPTMain/Spine/Bridges/LindbladBridge.lean— 191 lines, 0 sorry, 0 axiomWires
UnifiedTheory.LayerB.LindbladDecoherence(already on publication via the existing UnifiedTheory pin) into the spine's QMτ_entidentity at the scalar level. Distinct fromGKLSDissipatorBridge.lean(matrix-level GKLS, landed via PR #172).The bridge defines:
7 substantive theorems, all kernel-clean
[propext, Classical.choice, Quot.sound]:tauEnt_lindblad_eq_Gamma_t— closed formτ_ent = Γ·ttauEnt_lindblad_nonneg— second lawtauEnt_lindblad_monotone— monotone intcatept_lindblad_preserves_populations(UnifiedTheory re-export)catept_lindblad_contracts_coherencecatept_observable_approaches_classicalcatept_qm_tauEnt_from_lindblad— headline identityCompatibility
mainandfeat/publicationUnifiedTheory.LayerB.LindbladDecoherenceexposesDephasingRate,gamma_pos,gamma_antitone, etc. — all kernel-cleanlake buildclean (2173 jobs), audit cleanTest plan
lake build CATEPTMain.Spine.Bridges.LindbladBridgepasses[propext, Classical.choice, Quot.sound]feat/publicationby current workflow config)🤖 Generated with Claude Code