OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanCoupledSourceImage.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Joint source-bundle images for the actual coupled recurrence

The interval laws and all recurrence denominators are constructed here. Only the good-profile mass and the full normalized source-map submersion remain to be supplied by the profile selection.

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.coupled_source_bundle_haar_image_sequence line 35