source.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 
6 import Mathlib.Data.Finset.Basic
7 import Mathlib.Logic.Function.Basic
8 
9 /-!
10 # Nonlinear operation trees and obstruction packets
11 
12 This file establishes a deliberately modest nonlinear foundation.  An
13 operation tree is syntax with arbitrary unary and binary semantics; no
14 linearity, differentiability, convergence, or closure theorem is assumed.
15 Lean proves that evaluation depends only on the inputs that occur in the tree.
16 
17 The obstruction API is likewise local and fail-closed.  A nonzero residual at
18 one packet rules out one proposed global solution.  It does not, without added
19 hypotheses, prove that every candidate is obstructed or classify all solutions.
20 -/
21 
22 set_option autoImplicit false
23 
24 namespace Komorebi.PaperIII.NonlinearObstructions
25 
26 universe u v w x y
27 
28 /-! ## Nonlinear operation trees -/
29 
30 /--
31 Finite syntax for constants, inputs, unary operations, and binary operations.
32 The operation labels carry no unadvertised algebraic laws.
33 -/
34 inductive OperationTree
35     (Input : Type u) (Constant : Type v) (Unary : Type w) (Binary : Type x)
36     where
37   | input : Input → OperationTree Input Constant Unary Binary
38   | constant : Constant → OperationTree Input Constant Unary Binary
39   | unary : Unary → OperationTree Input Constant Unary Binary →
40       OperationTree Input Constant Unary Binary
41   | binary : Binary → OperationTree Input Constant Unary Binary →
42       OperationTree Input Constant Unary Binary →
43       OperationTree Input Constant Unary Binary
44 
45 namespace OperationTree
46 
47 variable {Input : Type u} {Constant : Type v} {Unary : Type w} {Binary : Type x}
48 variable {Value : Type y}
49 
50 /-- Evaluate an operation tree under completely explicit operation semantics. -/
51 def eval
52     (inputValue : Input → Value)
53     (constantValue : Constant → Value)
54     (unaryValue : Unary → Value → Value)
55     (binaryValue : Binary → Value → Value → Value) :
56     OperationTree Input Constant Unary Binary → Value
57   | .input i => inputValue i
58   | .constant c => constantValue c
59   | .unary op child => unaryValue op (eval inputValue constantValue unaryValue binaryValue child)
60   | .binary op left right =>
61       binaryValue op
62         (eval inputValue constantValue unaryValue binaryValue left)
63         (eval inputValue constantValue unaryValue binaryValue right)
64 
65 /-- The finite set of input packets actually read by a tree. -/
66 def inputs [DecidableEq Input] :
67     OperationTree Input Constant Unary Binary → Finset Input
68   | .input i => {i}
69   | .constant _ => ∅
70   | .unary _ child => inputs child
71   | .binary _ left right => inputs left ∪ inputs right
72 
73 /--
74 Locality theorem for arbitrary nonlinear semantics: agreement on all input
75 packets named by the syntax forces equal evaluation.
76 -/
77 theorem eval_congr_on_inputs [DecidableEq Input]
78     (tree : OperationTree Input Constant Unary Binary)
79     (first second : Input → Value)
80     (constantValue : Constant → Value)
81     (unaryValue : Unary → Value → Value)
82     (binaryValue : Binary → Value → Value → Value)
83     (hagree : ∀ i ∈ tree.inputs, first i = second i) :
84     tree.eval first constantValue unaryValue binaryValue =
85       tree.eval second constantValue unaryValue binaryValue := by
86   induction tree with
87   | input i =>
88       exact hagree i (by simp [inputs])
89   | constant c =>
90       rfl
91   | unary op child ih =>
92       simp only [eval]
93       congr 1
94       exact ih fun i hi ↦ hagree i (by simpa [inputs] using hi)
95   | binary op left right ihLeft ihRight =>
96       simp only [eval]
97       congr 1
98       · exact ihLeft fun i hi ↦ hagree i (by simp [inputs, hi])
99       · exact ihRight fun i hi ↦ hagree i (by simp [inputs, hi])
100 
101 /-- A tree with no named input packets has environment-independent value. -/
102 theorem eval_eq_of_inputs_eq_empty [DecidableEq Input]
103     (tree : OperationTree Input Constant Unary Binary)
104     (first second : Input → Value)
105     (constantValue : Constant → Value)
106     (unaryValue : Unary → Value → Value)
107     (binaryValue : Binary → Value → Value → Value)
108     (hempty : tree.inputs = ∅) :
109     tree.eval first constantValue unaryValue binaryValue =
110       tree.eval second constantValue unaryValue binaryValue := by
111   apply tree.eval_congr_on_inputs first second constantValue unaryValue binaryValue
112   intro i hi
113   rw [hempty] at hi
114   simp at hi
115 
116 end OperationTree
117 
118 /-! ## Candidate-specific obstruction packets -/
119 
120 section Obstructions
121 
122 variable {Packet : Type u} {Candidate : Type v} {Residual : Type w}
123 variable [Zero Residual]
124 
125 /-- A global solution is a candidate whose residual vanishes at every packet. -/
126 def IsSolution (residual : Candidate → Packet → Residual) (candidate : Candidate) : Prop :=
127   ∀ packet, residual candidate packet = 0
128 
129 /-- A local certificate naming one packet with a nonzero residual. -/
130 structure ObstructionPacket
131     (residual : Candidate → Packet → Residual) (candidate : Candidate) where
132   packet : Packet
133   nonzero : residual candidate packet ≠ 0
134 
135 /-- A certified obstruction packet rules out its specific candidate. -/
136 theorem ObstructionPacket.not_isSolution
137     {residual : Candidate → Packet → Residual} {candidate : Candidate}
138     (certificate : ObstructionPacket residual candidate) :
139     ¬ IsSolution residual candidate := by
140   intro hsolution
141   exact certificate.nonzero (hsolution certificate.packet)
142 
143 /-- A non-solution exposes an obstruction packet, classically and without finiteness. -/
144 theorem obstructionPacket_of_not_isSolution
145     {residual : Candidate → Packet → Residual} {candidate : Candidate}
146     (h : ¬ IsSolution residual candidate) :
147     Nonempty (ObstructionPacket residual candidate) := by
148   classical
149   by_contra hnone
150   apply h
151   intro packet
152   by_contra hnonzero
153   exact hnone ⟨⟨packet, hnonzero⟩⟩
154 
155 /-- Candidate failure is equivalent to the existence of a local obstruction packet. -/
156 theorem not_isSolution_iff_nonempty_obstructionPacket
157     {residual : Candidate → Packet → Residual} {candidate : Candidate} :
158     ¬ IsSolution residual candidate ↔
159       Nonempty (ObstructionPacket residual candidate) := by
160   constructor
161   · exact obstructionPacket_of_not_isSolution
162   · rintro ⟨certificate⟩
163     exact certificate.not_isSolution
164 
165 end Obstructions
166 
167 end Komorebi.PaperIII.NonlinearObstructions

Back to source controls