A machine-checked solution to the Jacobians challenge

15. form trace tower🔗

The fibrewise trace tower for pair forms h·ω₀ along a branched cover f : X → ℙ¹: fibre traces, branch handling, coherent selections, globalization and rationality of the traced form (the Gate-A reduction machinery).

1 modules, 123 lines, under Jacobians/FormTrace/.

  1. 15.1. Keystones
  2. 15.2. Builds on
  3. 15.3. FormTraceSheetCovector