OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanCellProfileComparison.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A supported pair supplies the coupled profile comparison

The common good set, positive mass, and error rate are all selected from the actual joint weak law. The scale and both polynomial limits stay fixed.

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.coupled_comparison_of_supported_cell_profiles line 37