|
|
87e361b6d8
|
feat(lean): Chentsov->Finsler->QUBO->QAOA routing bridge
Chentsov's theorem forces the Fisher metric; Finsler-Randers generalizes
with asymmetric drift beta; QUBO discretizes the geodesic; QAOA solves it.
- TransportQUBOBridge.lean (new, 0 sorries, 2 axioms with TODO(lean-port)):
randersMetricToQUBO, geodesicAssignment, isAnisotropic bridging
TransportTheory.RandersMetric -> EntropyMeasures.QUBOFormulation.
Two Q16_16 lemma boundaries: add_self_eq_zero_iff, cost_nonneg.
- computeAlphaCost_neg / computeBetaCost_neg lemmas added to TransportTheory.lean
(alpha symmetric, beta antisymmetric under direction negation).
- qaoa_adapter.py section III-D: FinslerMetric dataclass + finsler_metric_to_qubo()
conversion + finsler_demo CLI (verified: anisotropic pair Q_01=0.927, Q_10=0.0).
- docs/chentsov_finsler_qubo_routing.md: full 4-layer pipeline formalization.
- AGENTS.md updated: TransportQUBOBridge in blessed surface + pending proof work.
Build: lake build Semantics.TransportQUBOBridge -> 0 errors, 0 sorries
|
2026-06-21 00:32:23 -05:00 |
|
