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