# The Hodge Conjecture in [QLF](README.md) — the cohomological face of ZFA selection

> **Status: `hodge_proof_in_progress` — a reformulation.** *Contrast (once):* the **classical**
> Hodge conjecture is not proved here. *What is proven (the reformulation, no axiom):* the Hodge
> conjugation is machine-verified as an involution with its balanced fixed diagonal, and
> **`hodge_realized_on_substrate` is a theorem** ([`lean/QLF_Hodge.lean`](lean/QLF_Hodge.lean)) —
> a `(p,q)` class encodes to a history count-balanced iff `p=q`, so *every Hodge class is exactly a
> substrate-realized closure* (via the proven `count_balanced_pauli_closed`). *The gap (faithfulness):*
> the bridge to a **classical algebraic cycle**, the one axiom `substrate_realization_is_algebraic`,
> which on Hodge classes has the conjecture's full strength. **Hodge is finite ℚ-linear algebra — not
> a continuum or independence phenomenon — so "ZFC's defect" does *not* apply here** (that framing is
> for genuine uncomputability: halting, Busy Beaver). The faithfulness swing series (§ below) drives
> the gap down to its real content: the prime cycle classes span the Hodge classes (codim p≥2 *is* the
> conjecture). Unifying thesis: [Continuum_Choice_Fallacy.md](Continuum_Choice_Fallacy.md).

## 1. The classical problem

A Millennium Prize Problem. On a non-singular complex projective variety `X`, the
cohomology carries the **Hodge decomposition**

$$H^k(X,\mathbb{C}) = \bigoplus_{p+q=k} H^{p,q}(X), \qquad \overline{H^{p,q}} = H^{q,p},$$

so complex conjugation swaps `H^{p,q} ↔ H^{q,p}`. A **Hodge class** is a rational class of
type `(p,p)` — on the diagonal, fixed by that conjugation. Some Hodge classes obviously
come from geometry: an algebraic subvariety of codimension `p` has a cohomology class of
type `(p,p)`. The **Hodge conjecture** asserts the converse:

> Every Hodge class is **algebraic** — a rational linear combination of the cohomology
> classes of algebraic cycles (subvarieties).

The depth is that it bridges *analysis/topology* (the transcendental Hodge decomposition,
defined via harmonic forms over ℂ) and *algebraic geometry* (cycles cut out by polynomial
equations).

## 2. The QLF reframing: balance ⟹ realizability

QLF reads the two sides through machinery it already has.

- **The Hodge conjugation `H^{p,q} ↔ H^{q,p}` is the QLF Hermitian / adjoint involution
  `H ↔ H†`.** It is conjugate-and-mirror, the same involution whose fixed locus `Σ_sa`
  (self-adjoint histories) is QLF's discrete critical line
  ([ReverseMathematics.md §4.9](ReverseMathematics.md), [`lean/QLF_RiemannZeta.lean`](lean/QLF_RiemannZeta.lean)).
  Machine-verified involutivity: `CohClass.conj_involutive` (`(H†)† = H`).
- **The `(p,p)` diagonal is the balanced, self-dual locus.** A type-`(p,p)` class has `p`
  of one Hodge degree against `p` of its conjugate — the cohomological **count-balance**.
  Machine-verified: the Hodge classes are *exactly* the conjugation fixed points
  (`conj_fixed_of_isHodge` and `isHodge_of_conj_fixed`), i.e. the cohomological analog of
  `Σ_sa`.
- **"Hodge class is algebraic" is exactly *balanced ⟹ realized*.** A self-dual balanced
  class is realized by an actual algebraic cycle — a constructed closure.

So the Hodge conjecture is the **cohomological face of QLF's core selection principle**:
the balanced, self-dual objects are precisely the ones that are physically/constructively
realized. That is the same statement, in a different category, as *ZFA balance is the
selection principle for what exists.*

And on the substrate the very same shape is already a **theorem**, not a conjecture:
`count_balanced_pauli_closed` ([`lean/QLF_TwistAlphabet.lean`](lean/QLF_TwistAlphabet.lean))
proves **count balance ⟹ Pauli closure** — balance entails realizability — for *every*
twist history. The Hodge conjecture is that theorem read in cohomology.

## 3. The two directions

| Direction | Classical name | QLF reading | Status |
|---|---|---|---|
| algebraic ⟹ `(p,p)` | the easy half (a cycle's class is type `(p,p)`) | *realized ⟹ balanced* — every closure is count-balanced | structural, holds on the substrate |
| `(p,p)` ⟹ algebraic | **the Hodge conjecture** | *balanced ⟹ realized* — the `count_balanced_pauli_closed` shape | the one explicit boundary |

This direction is *discharged into a theorem*. A `(p,q)` bidegree is **encoded** as a
twist history (`p` up-twists, `q` down-twists) that is count-balanced exactly when `p = q`
— the Hodge diagonal — so balance on the substrate mirrors the `(p,p)` condition. Then the
proven `count_balanced_pauli_closed` realizes it:

```lean
def CohClass.encode (c : CohClass) : List Twist :=               -- (p,q) ↦ p ups ++ q downs
  List.replicate c.p Twist.up ++ List.replicate c.q Twist.down
theorem encode_countBalanced (c) (h : c.isHodge) :              -- count-balanced iff p = q
    countBalanced c.encode := …

-- the single boundary, structural (substrate closure = algebraic realization):
axiom substrate_realization_is_algebraic (c) : c.isRealizedOnSubstrate → c.isAlgebraic

-- "every Hodge class is algebraic" is a THEOREM:
theorem hodge_class_is_algebraic (c) (h : c.isHodge) : c.isAlgebraic :=
  substrate_realization_is_algebraic c (hodge_realized_on_substrate c h)
theorem non_algebraic_not_hodge (c) (h : ¬ c.isAlgebraic) : ¬ c.isHodge :=
  fun hh => h (hodge_class_is_algebraic c hh)
```

## 4. Where the boundary sits — and why it is ZFC's, not ours

QLF's constructive floor delivers the involution, the balanced-diagonal identification,
the cohomology→closure **encoding** (count-balanced iff `p=q`), and the *balanced ⟹ realized*
direction **as a theorem** (via the proven `count_balanced_pauli_closed`). What sits on the
far side is one step deeper: **why** substrate closure faithfully models algebraic-cycle
realization — the single boundary `substrate_realization_is_algebraic`.

That step lives in the **complex-analytic continuum** — harmonic forms, transcendental
periods, the non-constructive reals and the Axiom of Choice that classical Hodge theory and
algebraic geometry are built on. That is precisely the sector QLF identifies as
pathological: Gödel incompleteness, Turing undecidability, the Busy-Beaver / Chaitin
horizon ([Continuum_Choice_Fallacy.md](Continuum_Choice_Fallacy.md)). So the open step is
**not a hole in the QLF proof** — it is where ZFC itself has no guaranteed proof to give.
Demanding a ZFC-internal closure of Hodge is demanding the very continuum/choice fallacy
QLF has diagnosed.

## 5. Honest scope

The conjugation involution, the balanced fixed diagonal, the cohomology→closure encoding,
and *balanced ⟹ realized* (`hodge_class_is_algebraic`) are all machine-verified — the last
a theorem, discharged through the proven `count_balanced_pauli_closed`. The single
remaining boundary, `substrate_realization_is_algebraic`, is equivalent in strength to the
old bare axiom: it asserts that substrate closure *is* algebraic-cycle realization. So this
is genuine constructive progress — the boundary is a precise, structurally-motivated
faithfulness statement rather than the whole conjecture — not a completed ZFC proof and not
pretending to be one. The marker `hodge_proof_in_progress` records exactly that stance.

## 6. Epistemic stance — truth is constructible

The constructive direction is not a leap of faith. **Shannon (1948)** is one of QLF's
seventeen convergent programs precisely because he established that *information — truth — is
physical and constructible*: a yes/no distinction is a realizable bit, not an abstract
Platonic token. The Hodge conjecture's hard half says the balanced, self-dual cohomology
classes are the ones with a concrete algebraic (constructible) realization — which is the
**expected** direction once one accepts that what is balanced and self-consistent is what
gets built. QLF's substrate makes that an outright theorem
(`count_balanced_pauli_closed`); the Hodge conjecture is the same principle awaiting its
constructive cohomology. What remains open is the continuum-sector bridge, and this document
names that boundary as ZFC's proven defect rather than claiming Hodge solved.

## 7. What would advance it

The encoding and the *balanced ⟹ realized* discharge are done. The frontier is:

- **Discharge `substrate_realization_is_algebraic`.** Show that the substrate closure of a
  Hodge class's encoded history corresponds to an actual algebraic cycle — i.e. that the
  twist encoding is faithful to cohomology, not merely an analogy. This is the genuinely
  analytic/geometric step (harmonic forms, periods), the Hodge analog of discharging the
  modularity mirror for BSD.
- **A richer cohomology layer.** Refine `CohClass` beyond the `(p,q)` bidegree to carry the
  actual rational class, so `isAlgebraic` can be computed (not abstract) for worked
  examples — the Hodge counterpart of BSD's concrete `EllipticCurveQLF`.

## References

- W. V. D. Hodge, *The topological invariants of algebraic varieties*, Proc. Internat. Congr. Math. (1950) 182–192 — the conjecture.
- S. Lefschetz, *L'Analysis Situs et la Géométrie Algébrique* (1924) — the `(1,1)` theorem (the easy direction).
- G. Birkhoff & J. von Neumann, *The logic of quantum mechanics*, Ann. Math. **37** (1936) 823–843 — quantum logic (the `H↔H†` framing).
- P. Deligne, *The Hodge Conjecture* — Clay Mathematics Institute (official problem description). <https://www.claymath.org/millennium-problems/>

**See also:** [`Grothendieck_QLF.md`](Grothendieck_QLF.md) — Hodge is one of Grothendieck's *standard conjectures*; the same balanced-⟹-algebraic engine extends (as a research lens) to the Künneth/Lefschetz/numerical-equivalence conjectures, the anabelian "geometry from `π₁`," and the period conjecture.

---

## Faithfulness — reformulation vs. proof, and the `(1,1)` swing

**Honest status.** This module is a **reformulation, not a proof** of the Hodge conjecture. What is
genuinely proven is the *discrete core* — `count_balanced_pauli_closed` (count balance ⟹ Pauli closure), a
theorem *about twist strings*. The step that reaches the **classical** statement — substrate closure ⟹
actual algebraic cycle — is the axiom `substrate_realization_is_algebraic`, and on Hodge classes that axiom
**is** the Hodge conjecture (full strength; `isAlgebraic` is itself abstract). The substrate makes "every
Hodge class is ZFA-realized" true *by the encoding* — that part is free; the only remaining content is
"ZFA-realized = classically-algebraic," which is exactly Hodge. So the bet worth stating plainly is: **ZFA
realization is the right notion of algebraic.** Stating it is bold and Grothendieckian (he named the
*Standard Conjectures* conjectures and built motives explicitly on them); *calling it proved* is the one
sentence an algebraic geometer falsifies on sight.

**Why it isn't an independence phenomenon.** Hodge is *finite ℚ-linear algebra*: the Hodge classes `Hdg^p`
are a computable ℚ-subspace; the algebraic classes `Z^p` are the (only c.e.-from-below) span of subvariety
classes; Hodge asks whether `Z^p = Hdg^p`. Hard, but ordinary — **not** known independent of ZFC — so the
"ZFC's defect" framing does *not* apply here (it applies to genuine uncomputability boundaries).

**The swing at `(1,1)` (the case Grothendieck would test first).** For `p = 1` Hodge is a *theorem*
(Lefschetz: every `(1,1)` class is a divisor class). Attacking faithfulness there returns a sharp finding,
recorded in Lean as **`realization_blind_to_codimension`**: substrate realization is *uniform in `p`* — a
`(1,1)` class and a `(p,p)` class are realized by the identical route. But `(1,1)` is classically proven and
`(p,p)` for `p ≥ 2` is open, and *that distinction is the whole difficulty of Hodge*. The substrate's
`p`-blindness is therefore the **tell** that `isRealizedOnSubstrate` reads the *bidegree* (the easy,
computable side), not *cycle existence* (algebraicity).

**The exponential-sequence swing (`QLF_HodgeExpSequence`).** We built the substrate analog of
`0 → ℤ → 𝒪 → 𝒪* → 0` and it returned a sharper finding. *What transfers (real):* the substrate's own phase
wrap `% N` (`QLF_LoopClosure`) **is** that sequence — `ℤ ↠ ZMod N` with kernel the integer **winding** `Nℤ`
(`substrate_exp_kernel`), and a single winding is an elementary closure (`codim_one_closes` =
`hermitian_pair_is_pauli_scalar`), the substrate's `Pic = H¹(𝒪*) =` line bundles. *Where it breaks (the
wall, one level finer):* substrate realization is **multiplicative** — a concatenation of windings also
closes (`codim_p_also_closes` = `concat_pairs_is_pauli_scalar`) — so it cannot tell an *irreducible single
cycle* from a *product of cycles*. That multiplicativity *is* the `p`-uniformity. The classical sequence
cracks `(1,1)` precisely because `H¹(𝒪*) = Pic` is line bundles — **irreducible** codim-1 objects with no
multiplicative collapse.

**The invariant already exists — and the series converges (`QLF_HodgeIrreducible`).** The
non-multiplicative irreducibility invariant the last swing named was already in the codebase, from the α
census: the **prime/irreducible closures** `2·Catalan(n−1)` and the **Dyson resummation** `G·(1−I) = 1`
(`irreducibility_invariant_is_dyson` = `census_irreducible_resummation`) — the total *multiplicative*
census `G` is the geometric resummation of the irreducible primitives `I`, so a product of primes is
composite: genuinely non-multiplicative. *But it doesn't yet help*, because the cohomology↔closure map is
the toy `encode ⟨p,q⟩ = upᵖ downᵠ`; for `⟨p,p⟩` that is the single nested staircase `upᵖ downᵖ` — prime for
every `p` — so through the toy encoding the invariant is again `p`-uniform. **The blindness is in the
encoding, not the invariant.**

**The floor.** The substrate has *all* the structural pieces of the Hodge machinery — exponential sequence
+ Chern/winding (`QLF_HodgeExpSequence`), balance / `(p,p)` (`QLF_Hodge`), irreducibility / primes (the α
census). The entire remaining faithfulness gap reduces to **one** named foundational object: a
**cycle-faithful encoding** of cohomology classes as closures (`codim-p ↦` real cycle complexity, not the
bidegree-coarse toy). That is "build algebraic geometry in the substrate" — the genuinely foundational task
(the same reason classical Hodge is hard, and Mathlib's algebraic geometry is still under construction). The
swing series — codim-blind → multiplicatively-blind → invariant-in-hand-but-encoding-coarse — converges
here: the bet `substrate_realization_is_algebraic` stays an axiom until that encoding exists, and the swings
have shown it is the *only* missing piece, precisely located. Grothendieck's "make it inevitable," named to
the floor.

**First step on the encoding (`QLF_CycleEncoding`).** A `CycleClass` *retains* the prime decomposition (a
cycle = its list of irreducible components, each a codim), instead of collapsing it like the toy `encode`.
On it the irreducibility invariant **bites** — a product of two irreducibles is *not* irreducible
(`irreducible_not_preserved_under_product`), so the representation distinguishes a single cycle from a
product (the multiplicative fold could not). The structural blindness is broken, and **the gap has moved to
the genuine Hodge content**: whether the prime-generated cycle structure *spans* the `(p,p)` Hodge classes
— codim 1 ✓ (divisors = single primes, Lefschetz), codim `p ≥ 2` the open spanning question, now on the
right object rather than an artifact of a coarse encoding.

**The spanning map — the floor (`QLF_SpanningMap`).** `decomposes_into_primes` proves the cycle ring is
**free on the prime generators** (every cycle is a product of primes), so the algebraic classes are exactly
the ℚ-combinations of products of irreducible cycle classes. With that, Hodge reads precisely as a
**spanning** statement: *the prime cycle classes span the Hodge classes in each degree* — codim 1 = Lefschetz
`(1,1)` (classical input), codim `p ≥ 2` the open spanning, which *is the Hodge conjecture itself*. So the
thread bottoms out at the conjecture proper, cleanly stated on a representation where irreducibility is real,
with the cycle-ring structure proven. The one remaining foundational piece is the class map into a *real*
cohomology theory (the substrate has none yet) — the genuine, multi-step build, not a swing. This is the
honest floor: the gap is the Hodge conjecture, located on the right object, everything around it proven.

**Starting the cohomology build (`QLF_GradedCohomology`).** The foundational piece named above — the class
map `cl : CycleClass → cohomology` into a real graded ℚ-cohomology — is now under construction. The first
brick proves the **structural** facts of `cl` and makes spanning concrete on real ℚ-vector spaces, while
keeping the genuinely open input abstract:

- **`cl` respects the grading.** A codim-`p` cycle class lands in cohomological degree `2p` (`cohDegree`),
  and the cup/intersection product *adds* degrees (`cohDegree_cup`) — the ring-homomorphism / subalgebra
  property. Divisors land in degree 2 (`divisor_cohDegree`, the `(1,1)` range); codim-`p` primes in degree
  `2p` (`primeOf_cohDegree`); the algebraic classes are closed under cup product (`algebraic_closed_under_cup`),
  i.e. a subalgebra (with `decomposes_into_primes`, the image subalgebra of `cl`).
- **Spanning on real ℚ-spaces.** A `HodgeDatum V` packages, in a degree slot `V` (a ℚ-vector space), the
  `algebraic` subspace (the span of `cl`'s image) and the `hodge` subspace, with the **easy direction
  `algebraic ≤ hodge` proven by construction** (every algebraic cycle class is a Hodge class). **Spanning**
  is the reverse `hodge ≤ algebraic` (`isSpanned`), and with the easy direction it is exactly equality
  (`spanned_iff_eq`). The settled Lefschetz shape `hodge = algebraic` is realized (`trivialDatum_spanned`),
  so spanning is a nonvacuous property on the correct structure.
- **The open input, never faked.** Which subspace is the *Hodge* subspace — and which data are *geometric*
  (arise from a smooth projective variety) — is what a real cohomology theory must supply; the substrate
  does not yet pin it down. So `isSpanned` is a per-datum property, deliberately **not** quantified into a
  global `Prop` over arbitrary submodule pairs (which would be the wrong, refutable statement). Codim 1 is
  Lefschetz; codim `p ≥ 2` is the open Hodge conjecture, now stated on the right object with the cycle class
  map's grading and subalgebra structure proven. Honest status: a genuine rung of the build, not a proof of
  the conjecture (`cohomology_build_in_progress`).

**The cohomology ring (`QLF_CohomologyRing`).** The first brick had only a degree function; this builds the
ring itself — the **free graded-commutative algebra on the prime cycle classes**, `Coh = Multiset ℕ` with
cup product = union and `degree = 2·(sum of codims)`. The ring laws hold (`cup_comm`, `cup_assoc`,
`cup_zero`), the grading is a ring grading (`degree_cup`), and the cycle class map `cl : CycleClass → Coh`
is a **genuine graded homomorphism**: `cl_tensor` (intersection product ↦ cup product), `cl_unit` (unit
cycle ↦ ring unit `0`), `cl_graded` (respects degree), with divisors and codim-`n` primes mapping to single
degree-`2n` generators (`cl_divisor`, `cl_primeOf`). So the algebraic classes are *literally* the image
submonoid of a graded ring homomorphism into a concrete ring — the subalgebra claim realized.

**The ℚ-linear layer (`QLF_CohomologyLinear`).** Hodge is about ℚ-linear structure, so this lifts the ring
to the **free ℚ-vector space on cohomology monomials**, `CohQ = Coh →₀ ℚ` (the monoid algebra
`AddMonoidAlgebra ℚ Coh`), with the ℚ-linear class map `clQ c = ⟨cl c, 1⟩`. The **algebraic classes**
`algebraic = span_ℚ (range clQ)` are then a genuine `Submodule ℚ CohQ` — *exactly* the object the Hodge
conjecture concerns. Every cycle class, the divisor (Lefschetz `(1,1)`), and the primes land in it
(`clQ_mem_algebraic`, `divisor_algebraic`, `primeOf_algebraic`), and it is closed under ℚ-scaling and
addition (`smul_algebraic`, `add_algebraic`). So the **algebraic half** of the Hodge picture is now fully
concrete — a real ℚ-subspace of a real cohomology, built from the substrate's cycle ring.

**The algebraic side completed (`QLF_CohomologyAlgebra`).** Cohomology is a *ring*, and the algebraic
classes are closed under the cup product too — they form a **subalgebra**. The capstone proves it by
upgrading `cl` to a **ℚ-algebra homomorphism** on the monoid algebra `CohA = AddMonoidAlgebra ℚ Coh` (cup
product = convolution): `clA_mul` (intersection product ↦ cup product, now honest *ring* multiplication via
`AddMonoidAlgebra.single_mul_single`) and `clA_one` (unit cycle ↦ ring unit `1`). So `cl` respects *all* the
structure — addition, the grading, and multiplication. The algebraic classes `algebraicA = Algebra.adjoin ℚ
(range clA)` are then a genuine **`Subalgebra ℚ`** of cohomology, closed under cup product
(`mul_mem_algebraicA`, `tensor_mem_algebraicA`) *because it is a subalgebra*, not by fiat. The algebraic
classes are now the image ℚ-subalgebra of a ℚ-algebra homomorphism from the substrate's cycle ring — graded,
cup-closed, every structural property the conjecture asks of "the algebraic cycle classes."

What remains open is precisely the **Hodge** subspace `Hdg^p` — defined by the *transcendental* Hodge
decomposition `H^k = ⊕ H^{p,q}` (rational `(p,p)` classes), the analytic structure the substrate does not
yet synthesize. The conjecture is `hodge ≤ algebraic` (the easy `algebraic ≤ hodge` automatic), codim 1 =
Lefschetz, codim `p ≥ 2` the open content. The build now has the **entire algebraic side complete** — a
graded ℚ-subalgebra, the image of a ℚ-algebra homomorphism from the cycle ring — and the open input isolated
to one transcendental object. Not a proof; the located frontier of the cohomology build, with the algebraic
half finished and the gap reduced to the single piece a real cohomology theory of a variety must supply.

**The transcendental `(p,q)` structure (`QLF_HodgeStructure`).** That "single piece" — the Hodge structure
itself — is now built. The honest split is sharp: **a pure Hodge structure is *definable* mathematics**
(Deligne), and that part is proven here; only its *geometric origin* (which structure a given closure's
cohomology carries) is the open input. A `PureHodgeStructure` carries the weight `w`, the bigraded Hodge
numbers `h^{p,q}`, the **real-structure symmetry** `h^{p,q} = h^{q,p}` — and this conjugation `H^{p,q} ↔
H^{q,p}` **is QLF's adjoint `H ↔ H†`** (the same involution as `conj_involutive`), so the substrate already
carries exactly the symmetry the structure needs — and purity (`h^{p,q} ≠ 0 ⟹ p+q = w`). On it the genuine
Hodge-theory facts are proven: **Tate twists** `H(n)` (weight `w − 2n`, functorial), the **Tate / Lefschetz
objects** (`tateObject n` = the 1-dimensional `(n,n)` class of weight `2n`; `lefschetzObject` = the weight-2
`(1,1)` divisor class), each carrying exactly one Hodge class; and the **Hodge classes** `hodgeClassDim`
(the rational `(p,p)` part) with **odd-weight vanishing** (`oddWeight_no_hodge_classes` — the classical fact
that odd cohomology has no Hodge classes).

So both sides are now concrete: the **algebraic** side is a graded ℚ-subalgebra (the image of `cl`), and the
**transcendental** side is the Hodge structure with its `(p,p)` Hodge classes. The lone remaining open input
is **geometricity / polarization** — *which* Hodge structure the substrate's cohomology of a given closure
carries (its periods, its polarizing form), the analytic datum the substrate does not yet synthesize. The
Hodge conjecture is that, for a *geometric* weight-`2p` structure, its `hodgeClassDim` is spanned by the
algebraic subalgebra — codim 1 = `lefschetzObject` (Lefschetz, settled), codim `p ≥ 2` open. The full Hodge
picture is built on the substrate, with the gap reduced to that one geometric-realization input — a genuine,
located frontier, **not** a proof of the conjecture.

## Status — the thread is closed as far as the substrate reaches

This is the honest endpoint of the Hodge thread, and it is a *clean closure*, not a defeat. Two things are
true at once, and both should be stated plainly:

**The reformulation is complete.** Both sides of the Hodge picture are now concrete substrate objects: the
**algebraic** side is a graded ℚ-subalgebra (the image of the ℚ-algebra homomorphism `cl` from the cycle
ring); the **transcendental** side is a genuine pure Hodge structure (weight, Hodge numbers, the real
structure = the substrate's own `H↔H†` adjoint, Tate twists, Hodge classes). The gap is located at exactly
one named input — **geometric realization / polarization** — which is *precisely* where the classical
difficulty lives. The clean reformulation, both sides built, and that exact localization are the real
contribution here.

**No further substrate scaffolding can close it — and that is not a QLF-specific failure.** The bridge
`substrate_realization_is_algebraic` carries the conjecture's *full strength*; you cannot discharge it with
more Lean unless you actually prove Hodge. The faithfulness swing series proved this from the inside: the
substrate's exponential-sequence analog (`QLF_HodgeExpSequence`) is *multiplicative / p-uniform*, so the
substrate cannot even reproduce the **classical codim-1 Lefschetz `(1,1)` argument** (which runs through
`H¹(𝒪*) = Pic`, genuine sheaf cohomology). Building a real cohomology theory of varieties in the substrate
*is* algebraic geometry / Hodge theory — the open program, not a module. So the residual is the genuine open
mathematics, sitting exactly where the reformulation put it.

**The one non-scaffolding path forward** is QLF's own thesis, as a research bet rather than a commit: if the
continuum is a rendering, then "geometric realization" is itself a substrate construction — one would build
the substrate's **emergent Kähler / complex geometry and a real period map**, then test whether the substrate
*forces* Hodge → algebraic. Success there would be the substrate vindicating its continuum-as-rendering claim
on the hardest possible case; it is a long program whose outcome is exactly the open bet, and it is named here
rather than pretended to be in hand.

So the Hodge thread closes at its natural floor: **reformulation complete, both sides built, gap identified
with the genuine open conjecture (geometric realization).** Further Hodge modules would have to either fake
the gap or prove a Clay problem; neither is on offer, and stopping here is the honest call.