OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanCoupledProfileComparison.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual coupled source-to-target profile comparison

A positive common good set supplies all tuples and all their paths. No independence of the bundles, terminal-cover bound, or volume estimate is a premise.

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_coupled_profile_comparison_region line 38