Paper IX · Lean source

InvalidUnconditionalSolvability.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/InvalidUnconditionalSolvability.lean7 lines

Original source path

preserved/PRSC_IX_Consolidated_Manuscript/shared_correction/controls/InvalidUnconditionalSolvability.lean

1 import SharedCorrectionControls
2 
3 open Komorebi.SharedCorrectionControls
4 
5 -- EXPECTED FAILURE: one correction cannot realize two arbitrary identity targets.
6 example (a b : Two) : ∃ w : Two, identity w = a ∧ identity w = b := by
7   exact ⟨a, rfl, rfl⟩

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: 6cbbfe69a30a273276237affe23d63b6767d4ea6560d5513790fa8f72487d315

Original source on GitHub

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