PROOF_BOUNDARY.md
Resolution Semantics
PROOF_BOUNDARY.md
1 # Proof boundary
2
3 ## Mathematical proofs supplied in the PDF
4
5 The common presentation theorem assumes a set-indexed family of nonempty models
6 and choice in the metatheory. It does not construct an economical master universe.
7
8 The defect calculus assumes Boolean-homomorphic evaluations and functorial
9 transport. The invariant core is a Boolean subalgebra. Its residual quotient is
10 an F_2-vector-space quotient, not a Boolean quotient. Definable coherent
11 observables may be a proper part of the categorical limit.
12
13 The finite integration, selector classification, canonical envelope, ambiguity
14 support, and stability theorems have ordinary complete proofs in the note.
15 Their finite tests do not claim to realize the corresponding graphs by forcing.
16
17 The weighted multiresolution result assumes a finite set, positive fixed weights,
18 and nested partitions. Its outputs are real summaries, not binary truth values.
19
20 ## Exact computation
21
22 The script checks 12 stated polynomial identities by free Boolean-ring normal
23 forms. It also checks all monomial multiplication evaluations in four variables.
24 A reduction to the zero polynomial is an algebraic certificate under the stated
25 Boolean-ring reduction laws. The program is not a proof-assistant kernel.
26
27 Exhaustive finite checks cover graphs and partitions through 5 points, with the
28 smaller independent homomorphism and directed-system ranges stated in the JSON.
29 They corroborate the accompanying proofs, not replace them.
30
31 ## External theorems used conditionally
32
33 Forcing truth semantics, CH-changing forcing, S4.2 forcing validity, and
34 nonamalgamation are cited results. They are not newly proved or Lean-formalized
35 in this release. The forcing application assumes an externally supplied countable
36 transitive model and an appropriate generic filter.
37
38 ## Not established
39
40 - Existence of a model of ZFC, a countable transitive model, or all-worlds universe.
41 - A new independence, consistency, or large-cardinal result.
42 - Universal gluing or amalgamation of forcing worlds.
43 - A canonical Boolean projector for arbitrary resolution data.
44 - A sheaf or topos arising automatically from a diagram limit.
45 - Novelty of the complete proposed framework.
46 - Lean verification of any newly supplied declaration.
47
48 ## Formal source status
49
50 `formal/KRS_Core.lean` is UNCOMPILED. Its declarations are not counted as
51 machine-checked results. There are no intended `sorry` or custom `axiom`
52 commands in that source, but a source inspection is not a compiler audit.
53
54 The current note is an independent first version, not a merger with unseen earlier
55 Komorebi archives. Earlier reported theorem counts do not certify this note.