OAI/NumberTheory/DukePrimeDegree/Entropy/ShiftedRootConditionalProduct.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The remaining-root product law on physical time windows

The canonical one-root chart uses a time origin depending on all transverse coordinates. Removing that origin before restricting gives the product step in the ordered-root induction of EK2003, Proposition 8.3.

  1. theorem OAI.DukePrimeDegree.initialRootChart_shifted_conditional_product line 24