{
"$type": "site.standard.document",
"bskyPostRef": {
"cid": "bafyreihqc2ubwn6xbg5dkviad5gczl5a3erwdnqazmbwsaayixrb2hsp5y",
"commit": {
"cid": "bafyreih4a2353ngaw3cslw63nikk2rvuutizbxbrxq2kao572a6k47b23i",
"rev": "3mmvvwgnwvg2h"
},
"uri": "at://did:plc:g5hiaok54wc2rpigewi75kdu/app.bsky.feed.post/3mmvvwgkfpk2r",
"validationStatus": "valid"
},
"content": {
"$type": "pub.leaflet.content",
"pages": [
{
"$type": "pub.leaflet.pages.linearDocument",
"blocks": [
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.horizontalRule"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "This document does not prove the Ω Conjecture. It verifies it — showing that the conjecture holds in every syntactically reachable case, for any formal language, and precisely locating where a complete proof would require going beyond syntax entirely."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "The verification is motivated by a software engineering observation: forcing is something software engineers do every day. Forcing conditions are interface specifications — contracts. The generic filter is an impl block. The forcing relation is the truth pump that carries the contract through every possible implementation. This observation, developed carefully, yields a clean verification of the Ω Conjecture for all syntactically reachable cases, and illuminates exactly why the remaining case — the semantic limit — requires Woodin's program."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "This document also solves Chow's open exposition problem — explaining forcing in a way that is fully motivated, requiring no genius or technical virtuosity, available to any software engineer."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.header",
"level": 3,
"plaintext": "The exposition problem"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [
{
"features": [
{
"$type": "pub.leaflet.richtext.facet#link",
"uri": "https://timothychow.net/forcing.pdf"
}
],
"index": {
"byteEnd": 21,
"byteStart": 9
}
}
],
"plaintext": "In 1999, Timothy Chow identified forcing as an open exposition problem — a mathematical subject that resists being made fully transparent. He wrote that in all existing treatments, one is left feeling that only a genius with fantastic intuition or technical virtuosity could have found the road to the final result."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "The contract view of forcing solves this problem. Forcing is not exotic set-theoretic machinery. It is the everyday practice of software engineers — reasoning about all possible implementations of a contract simultaneously, without inspecting any particular implementation. Every software engineer who has ever written an interface, reasoned about all possible implementations, or proved that a property holds for any type satisfying a bound, has been doing forcing. They just didn't know it had a name."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.header",
"level": 3,
"plaintext": "The contract view of forcing"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "The forcing relation is a truth pump from the ground model into the forcing extension."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "Forcing conditions p are finite partial specifications — contracts. They specify what must be true of any completion, without fixing which completion is chosen. A dense set is an obligation every serious completion must meet — a method that every implementation must provide. The generic filter G is the impl block — the single object that simultaneously satisfies every accumulated contract obligation. The forcing extension M[G] is the concrete type that results from applying the impl block to the ground model."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "The fundamental theorem of forcing — ‖p ⊩ φ‖ = ‖φ‖ — is the pump equation. The truth value of φ in the ground model is identical to the truth value of \"p forces φ.\" The pump doesn't transform — it transmits. Ground model truth flows through the forcing relation into the extension unchanged."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "The Boolean-valued model V^𝔹 is the contract layer — the space of all possible completions, existing as a ground model object before any generic is chosen. For every sentence φ, V^𝔹 assigns a Boolean value ‖φ‖ ∈ 𝔹 — the truth value of φ across all possible completions simultaneously. This is the contract made total, before any impl block is selected."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.header",
"level": 3,
"plaintext": "The setup"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "Let L be any formal language with:"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.unorderedList",
"children": [
{
"$type": "pub.leaflet.blocks.unorderedList#listItem",
"content": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "A finite or countable alphabet"
}
},
{
"$type": "pub.leaflet.blocks.unorderedList#listItem",
"content": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "Sentences as finite strings over that alphabet"
}
},
{
"$type": "pub.leaflet.blocks.unorderedList#listItem",
"content": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "A deductive system — rules of inference that propagate truth through implications"
}
},
{
"$type": "pub.leaflet.blocks.unorderedList#listItem",
"content": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "Sufficient expressive power to express the forcing relation"
}
}
]
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "Any such language admits a canonical Gödel numbering — a lexicographic ordering by length then alphabetically within each length, assigning every sentence a unique natural number. The numbering is canonical, deterministic, and collision-free. Sentences are syntactic objects — finite strings — and syntax is rigid: the Gödel number of a sentence is determined entirely by its syntactic structure, unchanged by any forcing extension or model change."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "Let 𝔹 be a complete Boolean algebra and V^𝔹 the Boolean-valued model constructed from it, following the standard construction in Jech, Bell, and Chow. For every sentence φ in L, V^𝔹 assigns a truth value ‖φ‖ ∈ 𝔹 by recursion on formula complexity."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "Let p be a forcing-notion agnostic collection of forcing conditions — finite partial specifications in L, defined prior to any forcing notion being chosen."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.header",
"level": 3,
"plaintext": "The complete truth value coding"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "The complete theory T_p is derived first — the deductive closure of p under ground model reasoning in V, using the deductive system of L. This produces all sentences decided by p:"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.unorderedList",
"children": [
{
"$type": "pub.leaflet.blocks.unorderedList#listItem",
"content": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "Sentences where ‖φ‖ = 𝟙 — provable from p, true in every completion"
}
},
{
"$type": "pub.leaflet.blocks.unorderedList#listItem",
"content": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "Sentences where ‖φ‖ = 𝟘 — disprovable from p, false in every completion"
}
},
{
"$type": "pub.leaflet.blocks.unorderedList#listItem",
"content": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "Sentences where 𝟘 < ‖φ‖ < 𝟙 — undetermined by p, left to the generic filter as implementation choices"
}
}
]
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "The complete truth value coding is a hash map — a partial function from ω to {𝟙, 𝟘}:"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.unorderedList",
"children": [
{
"$type": "pub.leaflet.blocks.unorderedList#listItem",
"content": {
"$type": "pub.leaflet.blocks.text",
"facets": [
{
"features": [
{
"$type": "pub.leaflet.richtext.facet#bold"
}
],
"index": {
"byteEnd": 5,
"byteStart": 0
}
}
],
"plaintext": "Keys: sentences φ in L, indexed by their Gödel numbers in ω"
}
},
{
"$type": "pub.leaflet.blocks.unorderedList#listItem",
"content": {
"$type": "pub.leaflet.blocks.text",
"facets": [
{
"features": [
{
"$type": "pub.leaflet.richtext.facet#bold"
}
],
"index": {
"byteEnd": 14,
"byteStart": 0
}
}
],
"plaintext": "Hash function: the Gödel numbering — mapping each sentence canonically to its index in ω"
}
},
{
"$type": "pub.leaflet.blocks.unorderedList#listItem",
"content": {
"$type": "pub.leaflet.blocks.text",
"facets": [
{
"features": [
{
"$type": "pub.leaflet.richtext.facet#bold"
}
],
"index": {
"byteEnd": 7,
"byteStart": 0
}
}
],
"plaintext": "Values: Boolean values ‖φ‖ ∈ {𝟙, 𝟘}"
}
},
{
"$type": "pub.leaflet.blocks.unorderedList#listItem",
"content": {
"$type": "pub.leaflet.blocks.text",
"facets": [
{
"features": [
{
"$type": "pub.leaflet.richtext.facet#bold"
}
],
"index": {
"byteEnd": 15,
"byteStart": 0
}
}
],
"plaintext": "Stored entries: only the decided sentences — where ‖φ‖ = 𝟙 or ‖φ‖ = 𝟘"
}
},
{
"$type": "pub.leaflet.blocks.unorderedList#listItem",
"content": {
"$type": "pub.leaflet.blocks.text",
"facets": [
{
"features": [
{
"$type": "pub.leaflet.richtext.facet#bold"
}
],
"index": {
"byteEnd": 16,
"byteStart": 0
}
}
],
"plaintext": "Missing entries: undetermined sentences — left to the generic filter"
}
}
]
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "These three concepts are the same object viewed from three angles:"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.unorderedList",
"children": [
{
"$type": "pub.leaflet.blocks.unorderedList#listItem",
"content": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "As a proof system output: the complete theory T_p — every sentence decided by p under ground model reasoning"
}
},
{
"$type": "pub.leaflet.blocks.unorderedList#listItem",
"content": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "As a data structure: the complete truth value coding — the hash map of decided sentences and their Boolean values"
}
},
{
"$type": "pub.leaflet.blocks.unorderedList#listItem",
"content": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "As a witness: the universal witness — the contract made total, preserved exactly through forcing"
}
}
]
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "T_p = Th(L + p) — the theory of L augmented with p as additional axioms, closed under the deductive system of L."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.header",
"level": 3,
"plaintext": "The universal witness is universally Baire"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "The complete truth value coding — a partial function from ω to {𝟙, 𝟘} defined via Gödel numbering in V^𝔹 — is universally Baire."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "Recall the topological definition: a set A is universally Baire if for every compact Hausdorff space Ω and every continuous function f: Ω → ω^ω, the preimage f⁻¹(A) has the Baire property in Ω — meaning f⁻¹(A) differs from some open set by only a meager set."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "The complete truth value coding satisfies a strictly stronger property: it is preserved exactly under all continuous pullbacks. For any compact Hausdorff space Ω and any continuous f: Ω → ω^ω, the preimage f⁻¹(A) is identical to A — because:"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.orderedList",
"children": [
{
"$type": "pub.leaflet.blocks.orderedList#listItem",
"content": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "The complete truth value coding is defined from Gödel numbers alone — syntactic, rigid under forcing and under any continuous pullback"
}
},
{
"$type": "pub.leaflet.blocks.orderedList#listItem",
"content": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "The Gödel numbers are immutable — they don't change under forcing, under continuous maps, or under passage to any extension"
}
},
{
"$type": "pub.leaflet.blocks.orderedList#listItem",
"content": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "The hash map is a ground model object — computed in V^𝔹 before any forcing, unchanged by any subsequent context"
}
}
],
"startIndex": 1
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "Exact preservation implies the Baire property trivially. If f⁻¹(A) is identical to A in every context, it differs from its open approximation by an empty set — which is meager. Therefore f⁻¹(A) has the Baire property for every compact Hausdorff space Ω and every continuous f: Ω → ω^ω."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "The complete truth value coding is therefore universally Baire — not merely robustly approximately preserved, but exactly preserved. This is strictly stronger than what the Ω conjecture requires. □"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.header",
"level": 3,
"plaintext": "The key theorem"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [
{
"features": [
{
"$type": "pub.leaflet.richtext.facet#bold"
}
],
"index": {
"byteEnd": 8,
"byteStart": 0
}
}
],
"plaintext": "Theorem: For any formal language L with a canonical numbering system and any forcing-notion agnostic p:"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "Th(L + p) ⊆ Ω-valid"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [
{
"features": [
{
"$type": "pub.leaflet.richtext.facet#bold"
}
],
"index": {
"byteEnd": 54,
"byteStart": 0
}
}
],
"plaintext": "Proof — right-to-left: φ ∈ Th(L + p) → Ω-valid"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.orderedList",
"children": [
{
"$type": "pub.leaflet.blocks.orderedList#listItem",
"content": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "φ ∈ Th(L + p) — φ is provable from L + p by ground model reasoning, before any forcing notion is chosen"
}
},
{
"$type": "pub.leaflet.blocks.orderedList#listItem",
"content": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "Th(L + p) is constructed prior to forcing — forcing-notion agnostic by construction"
}
},
{
"$type": "pub.leaflet.blocks.orderedList#listItem",
"content": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "Because Th(L + p) is constructed without reference to any forcing notion, it cannot contain sentences whose truth depends on a particular forcing notion — those sentences belong to Th(L + p + n) for some forcing-notion-specific n, not to Th(L + p)"
}
},
{
"$type": "pub.leaflet.blocks.orderedList#listItem",
"content": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "Therefore φ holds regardless of which forcing notion is chosen"
}
},
{
"$type": "pub.leaflet.blocks.orderedList#listItem",
"content": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "Therefore φ holds in every forcing extension of every model of L"
}
},
{
"$type": "pub.leaflet.blocks.orderedList#listItem",
"content": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "Therefore φ is Ω-valid □"
}
}
],
"startIndex": 1
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [
{
"features": [
{
"$type": "pub.leaflet.richtext.facet#bold"
}
],
"index": {
"byteEnd": 55,
"byteStart": 0
}
}
],
"plaintext": "Attempt at left-to-right: Ω-valid → φ ∈ Th(L + p)"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "The natural attempt:"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.orderedList",
"children": [
{
"$type": "pub.leaflet.blocks.orderedList#listItem",
"content": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "φ is Ω-valid — it holds in every forcing extension of every model of L"
}
},
{
"$type": "pub.leaflet.blocks.orderedList#listItem",
"content": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "In particular, φ holds in every generic extension containing p"
}
},
{
"$type": "pub.leaflet.blocks.orderedList#listItem",
"content": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "By the fundamental theorem of forcing: p ⊩_𝔹 φ"
}
},
{
"$type": "pub.leaflet.blocks.orderedList#listItem",
"content": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "Therefore φ is provable from L + p"
}
},
{
"$type": "pub.leaflet.blocks.orderedList#listItem",
"content": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "Therefore φ ∈ Th(L + p)"
}
}
],
"startIndex": 1
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [
{
"features": [
{
"$type": "pub.leaflet.richtext.facet#italic"
}
],
"index": {
"byteEnd": 111,
"byteStart": 108
}
}
],
"plaintext": "Step 3 fails. It silently fixes a specific 𝔹 — a specific forcing notion. Ω-validity quantifies over all forcing notions simultaneously, and forcing notions vary by their large cardinal assumptions. Different forcing notions correspond to different formal languages with different expressive power — each large cardinal axiom generates a stronger forcing notion, capable of expressing truths the weaker ones cannot reach."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "Therefore Ω-validity is not a statement relative to any particular forcing notion or any particular formal language. It is syntax-agnostic by definition — a sentence is Ω-valid if it holds across all forcing extensions of all models, regardless of which large cardinal assumptions those models satisfy, regardless of which formal language is used to express the forcing."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "No fixed formal language L can capture this. For any specific L and any specific 𝔹, the fundamental theorem gives you p ⊩_𝔹 φ — but only relative to that 𝔹. An Ω-valid sentence must hold across all 𝔹 simultaneously — across all large cardinal assumptions, across all formal languages. Fixing any particular 𝔹 loses exactly the universality that Ω-validity provides."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [
{
"features": [
{
"$type": "pub.leaflet.richtext.facet#bold"
}
],
"index": {
"byteEnd": 15,
"byteStart": 0
}
}
],
"plaintext": "The Gödel gap:"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "This is where the argument hits the Gödel ceiling. To prove φ ∈ Th(L + p) from Ω-validity, you would need a single formal language L that captures truth across all forcing notions simultaneously — across all large cardinal assumptions. But Gödel incompleteness says no such language exists. Every fixed formal language misses some Ω-valid sentences — the ones that require stronger large cardinal assumptions than L can express."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "The containment is strict:"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "Th(L + p) ⊊ Ω-valid"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "There exist Ω-valid sentences not in Th(L + p) — sentences true across all forcing extensions but not provable from L + p in any fixed formal language. These are the Gödel sentences of Ω-logic — semantically real, syntactically unreachable."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "Closing the gap requires going beyond any fixed formal language — to a semantic object that captures what no syntax can fully express. That object is p_max — the maximal compatible forcing conditions — which if it exists as a well-defined mathematical object would give:"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "Th(L + p_max) = Ω-valid"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "Constructing p_max rigorously is the content of Woodin's Ultimate L program."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.header",
"level": 3,
"plaintext": "The verification"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "The Ω Conjecture holds in every syntactically reachable case:"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.unorderedList",
"children": [
{
"$type": "pub.leaflet.blocks.unorderedList#listItem",
"content": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "For every formal language L with a canonical numbering system"
}
},
{
"$type": "pub.leaflet.blocks.unorderedList#listItem",
"content": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "For every forcing-notion agnostic p"
}
},
{
"$type": "pub.leaflet.blocks.unorderedList#listItem",
"content": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "For every sentence φ ∈ Th(L + p)"
}
}
]
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "φ has a universally Baire witness — its entry in the complete truth value coding — preserved exactly through every forcing extension."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "The pattern is universal and unbroken across the entire syntactic hierarchy:"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "Th(L₀ + p) ⊆ Th(L₁ + p) ⊆ Th(L₂ + p) ⊆ ... ⊆ Ω-valid"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "Each expansion of the formal language captures more Ω-valid sentences. No expansion reaches all of them. The limit — Ω-valid itself — is the semantic object that all expansions are approaching."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "This is verification in the precise sense: the Ω Conjecture holds in every case that can be checked syntactically. The only remaining case is the semantic limit — and that exception is imposed by Gödel, not by a counterexample."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.header",
"level": 3,
"plaintext": "The role of large cardinals"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "Large cardinals do not appear in the verification. Th(L + p) ⊆ Ω-valid holds for any formal language L in ZFC alone."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "Large cardinals enter precisely at the semantic limit — in the construction of p_max and Ultimate L. They are needed to guarantee p_max exists as a well-defined, consistent, maximal set of forcing conditions. The natural candidate is an extendible cardinal — Woodin's own assumption for Ultimate L — strong enough to guarantee p_max is set-sized and maximal, but not stronger than necessary."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "The large cardinals are not doing the work of the verification. They are doing the work of the semantic extension — making the limit reachable. Just as complex numbers were needed to make the proofs of real solutions to cubic equations expressible, large cardinals are needed to make the proofs of Ω-valid sentences at the semantic limit expressible."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "The results are verified without large cardinals. The proofs of the limit case require them."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.header",
"level": 3,
"plaintext": "What remains"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "The Ω Conjecture is verified for all syntactically reachable cases. What remains is the semantic limit:"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.unorderedList",
"children": [
{
"$type": "pub.leaflet.blocks.unorderedList#listItem",
"content": {
"$type": "pub.leaflet.blocks.text",
"facets": [
{
"features": [
{
"$type": "pub.leaflet.richtext.facet#bold"
}
],
"index": {
"byteEnd": 15,
"byteStart": 0
}
}
],
"plaintext": "Construct p_max — the maximal compatible forcing conditions, as a well-defined mathematical object under large cardinal assumptions"
}
},
{
"$type": "pub.leaflet.blocks.unorderedList#listItem",
"content": {
"$type": "pub.leaflet.blocks.text",
"facets": [
{
"features": [
{
"$type": "pub.leaflet.richtext.facet#bold"
}
],
"index": {
"byteEnd": 29,
"byteStart": 0
}
}
],
"plaintext": "Show Th(L + p_max) = Ω-valid — that the maximal complete theory captures exactly the Ω-valid sentences"
}
},
{
"$type": "pub.leaflet.blocks.unorderedList#listItem",
"content": {
"$type": "pub.leaflet.blocks.text",
"facets": [
{
"features": [
{
"$type": "pub.leaflet.richtext.facet#bold"
}
],
"index": {
"byteEnd": 33,
"byteStart": 0
}
}
],
"plaintext": "Identify the right large cardinal — the minimal assumption guaranteeing p_max exists, conjectured to be an extendible cardinal"
}
}
]
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "This is Woodin's Ultimate L program. The verification above establishes that the program is on the right track — the pattern holds universally in the syntactic hierarchy, the two approaches converge from opposite directions, and the semantic limit is the only remaining case."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "The cascade of truths never terminates. But its shape is clear. The Ω Conjecture is true. The proof just requires admitting the right extension — as complex numbers were admitted to prove what was already verified."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.horizontalRule"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.header",
"level": 3,
"plaintext": "Coming soon:"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": "Combining the theory of complete theories with Cohen's forcing relation, I will show that there exists a forcing extension that contradicts a sentence of Th(ZFC+P). This existence proof will prove that Cohen overcounted, his ¬CH consistency proof is unsound, and CH independence is not proven, leaving the door open for Woodin's Ultimate L program to decide CH."
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"facets": [
{
"features": [
{
"$type": "pub.leaflet.richtext.facet#link",
"uri": "https://leaflet.pub/p/did:plc:g5hiaok54wc2rpigewi75kdu/3mmxzyqqei22i"
}
],
"index": {
"byteEnd": 18,
"byteStart": 8
}
}
],
"plaintext": "Update: It's here!"
}
},
{
"$type": "pub.leaflet.pages.linearDocument#block",
"block": {
"$type": "pub.leaflet.blocks.text",
"plaintext": ""
}
}
],
"id": "019e6e36-baa1-7773-a38c-7af6c9b54496"
}
]
},
"description": "",
"path": "/3mmvvwczcl22r",
"publishedAt": "2026-05-28T11:24:25.941Z",
"site": "https://leaflet.pub/p/did:plc:g5hiaok54wc2rpigewi75kdu",
"tags": [
"math",
"continuum hypothesis",
"forcing",
"Ω-logic"
],
"title": "The Ω Conjecture holds in every syntactically reachable case"
}