Paper IX · Lean source

NegativeAffineJointLift.lean

Selected results recorded Coverage and evidence

Compiler/replay evidence is reported for a subset or bounded block. No whole-work coverage is implied.

This viewer reads the retained source; it does not run Lean or assign new claim mappings.

shared_correction/controls/NegativeAffineJointLift.lean8 lines

Original source path

preserved/PRSC_IX_Consolidated_Manuscript/shared_correction/controls/NegativeAffineJointLift.lean

1 module
2 public import AffinePairControls
3 
4 @[expose] public section
5 open Komorebi.AffinePair Komorebi.AffinePairControls
6 
7 example : HasJointLift 2 1 oneId oneId (fun _ => 0) (fun _ => 2) (fun _ => 0) := by
8   exact two_individual_lifts

Back to source controls

Original file and source record

This copy matches the recorded source file. Its publication here does not change the work’s review status.

SHA-256: c4de3f527e6ab307fa259aefc10b0099df1014d7765e929ca4a92a339e2cd008

Original source on GitHub

Back to Paper IX: Arithmetic Packets, Dyadic Towers, and Local Polynomial Deformation