HIBS — Hidden-space Bridge System
Lean 4 formalisation of
Liu & Xu, "The Hidden-space Bridge System: A Three-axiom Foundation Connecting the Real and Imaginary Domains"
Complex numbers ℂ admit three standard axiomatisations:
| Style | Definition | What it takes as primitive |
|---|---|---|
| Polynomial-ring quotient | ℝ[x]/(x²+1) | The ring ℝ[x] and the ideal (x²+1) |
| Matrix representation | {{a,-b},{b,a}} | Matrix multiplication and SO(2) |
| Formal symbol | i² = −1 | An extraneous symbol i with a stipulated rule |
All three accept ℂ as an already-split object (real part + imaginary part). They explain how ℂ works, but leave three questions unanswered:
- Why does an imaginary direction exist at all?
- Could i have other generative origins?
- Does ℂ emerge from a more elementary structure?
HIBS addresses these questions by reversing the direction of explanation: instead of building ℂ from ℝ by adjoining i, it postulates a hidden generative layer S whose observable projection is ℂ.
S (hidden generative layer)
/ \
f / \ g (non-injective projections)
v v
ℝ iℝ
\ /
\ / π
v
ℂ (observable slice)
Three axioms govern S:
| Axiom | Statement | Intuition |
|---|---|---|
| (A1) | ∃ f : S↠ℝ, g : S↠iℝ, both non-injective | Projection loses information — you cannot go back |
| (A2a) | ⟨₁+⟨₂ ∈ S, ⟨₁−⟨₂ ∈ S (Flow = S) | Addition and subtraction stay inside the hidden layer |
| (A2b) | Flow(⟨₁×⟨₂) = ℝ, Flow(⟨₁÷⟨₂) = ℝ | Multiplication and division force a projection to ℝ |
| (A3) | Flow(√⟨) = iℝ for all ⟨ ∈ S | Square root forces a projection to iℝ |
The asymmetry is the point: ± stay in S, ×÷ jump to ℝ, √ jumps to iℝ.
Define ι : ℂ → S by ι(a+bi) = ι_ℝ(a) ⊕_S (˙b)i. Then ι is an additive monomorphism.
ι(z₁ + z₂) = ι(z₁) ⊕_S ι(z₂) (additive homomorphism)
ι(z₁) = ι(z₂) ⇒ z₁ = z₂ (injective)
There exist z₁, z₂ ∈ ℂ such that
ι(z₁ · z₂) ≠ ι(z₁) ⊗ ι(z₂)
The two sides live in different signal branches of S. Explicit counterexample in the labelled-pair model: z₁ = 1 + i, z₂ = i.
π ∘ ι = id_ℂ
Every complex number is uniquely recovered from its hidden image; ℂ is strictly the observable slice of S.
S contains the additive structure of ℂ but multiplication cannot be embedded. This is a direct algebraic consequence of axiom (A2b): every internal multiplication forces a projection to ℝ.
No two axioms imply the third:
| Model | Violates | Satisfies | Construction |
|---|---|---|---|
| M₁ | (A1) | (A2), (A3) | Σ collapsed to {∗}; f,g become injective |
| M₂ | (A2b) | (A1), (A3) | Product tag stays S instead of R |
| M₃ | (A3) | (A1), (A2) | Square-root tag stays S instead of iR |
All proofs are carried out on the labelled-pair model
S = ℤ × Σ where Σ = {S, R, iR}
The value type is ℤ (all paper examples use integers). A hidden number ⟨x, σ⟩ carries a value and a signal tag σ that records whether it came from S, projects to ℝ, or projects to iℝ.
| Operation | Definition | Tag |
|---|---|---|
| ⟨x,σ⟩ + ⟨y,τ⟩ | ⟨x+y, S⟩ | S |
| ⟨x,σ⟩ − ⟨y,τ⟩ | ⟨x−y, S⟩ | S |
| ⟨x,σ⟩ × ⟨y,τ⟩ | ⟨xy, R⟩ | R |
| √⟨x,σ⟩ | ⟨x, iR⟩ | iR |
The tag is the formal realisation of the Flow operator.
HIBS/
├── HIBS.pdf # Original paper
├── Main.lean # Executable entry point
├── HIBS.lean # Library root
├── HIBS/
│ ├── Definitions.lean # Core types: Tag, S, ℂ, operations, ι, π
│ ├── Axioms.lean # Type-polymorphic Axiom1, Axiom2, Axiom3
│ ├── Model.lean # Consistency (Thm 4.2) + Independence (Cor 4.8)
│ ├── Embedding.lean # Main theorems (6.1–6.10)
│ ├── Derivation.lean # Reverse direction: S derived from the imaginary unit i
│ ├── Conjugation.lean # Conjecture (ii): conj z̄ ↔ signal reversal ⟨+↔⟨−
│ └── Sqrt.lean # Full (A3): ⟨+ ↦ iR⁻, ⟨− ↦ iR⁺ (hSqrtFull, half-axes)
Design decisions:
| Decision | Rationale |
|---|---|
| Zero dependencies | Pure core Lean 4 — no mathlib imports. All types (ℂ, Imag, Hidden) are self-defined. Makes the project trivially portable across Lean versions and CI-fast. |
| Signature-polymorphic axioms | Axiom1/Axiom2/Axiom3 are defined as structures over a generic carrier type S. The three counter-models M₁, M₂, M₃ each instantiate different S and operation definitions while sharing the same axiom predicates — a model-theoretic independence proof inside the type system. |
| ℤ as base ring | All paper examples are integer arithmetic. Using ℤ (available in core Lean) avoids the ℝ/ℚ dependency (which would require mathlib). |
Tags as inductive Tag |
The three-element inductive `Tag.S |
| native_decide for ground terms | Specific counterexamples (Thm 6.2, Cor 6.10) are decided by native_decide after case-splitting the free variables. |
What is verified:
- ✅ Consistency: the labelled-pair model satisfies (A1)∧(A2)∧(A3)
- ✅ Independence: three counter-models show no pair implies the third
- ✅ Additive embedding: ι preserves + and is injective
- ✅ Multiplicative obstruction: explicit counterexample where ι(z₁·z₂) ≠ ι(z₁)⊗ι(z₂)
- ✅ Projection factorisation: π∘ι = id_ℂ (using the two-component embedding ι')
- ✅ Reversibility: add/sub are value-inverses; mul and sqrt irreversibly change tags
- ✅ Factorisation asymmetry: ⟨6,R⟩ = ⟨1,S⟩×⟨6,S⟩ = ⟨2,S⟩×⟨3,S⟩
- ✅ Derivation from i (reverse direction, §7): tags = i-powers (i⁰=S, i¹=iR, i²=R); hEval(hMulAdj a b) = hEval a · hEval b; imul closes S under ×i; (iR)² = R-ray; z = a·i⁰ ⊕ b·i¹ embeds ℂ
- ✅ Axiom diagnostics of the derived structure: A1, A3 hold; A2b fails for hMulAdj (× stays in S instead of collapsing to ℝ)
- ✅ Conjecture (ii) (§2): conj z̄ ↔ signal reversal — hEval(conjS h) = conj(hEval h); ι'(z̄) = conjC(ι' z); π'(conjC(ι' z)) = z̄; signalRev swaps the ⟨+/⟨− partition; conjS is an automorphism of hMulAdj and anti-linear w.r.t. ×i
- ✅ Full (A3) (§5): hSqrtFull (sign-aware √) — tag always iR; ⟨+ ↦ iR⁻, ⟨− ↦ iR⁺ (geometric: √ = ×(−i) on the real rays); √0 = 0; (√⟨)² ∈ ℝ (R-ray); iℝ∖{0} = iR⁻ ⊔ iR⁺; 0 ∈ ℝ∩iℝ
lake build
.lake/build/bin/hibsRequires Lean 4.28.0 (or compatible). No external dependencies.
7. Deriving the hidden space from the imaginary unit (reverse direction)
The paper postulates S = ℤ×{S,R,iR} and shows ℂ is its observable slice ("S flows down to ℂ").
The reverse direction derives S from the imaginary unit i (with i² = −1), formalized in
HIBS/Derivation.lean:
| Tag | Power of i | Complex value | Ray |
|---|---|---|---|
S |
i⁰ | 1 | positive real ray |
R |
i² | −1 | reflected real ray |
iR |
i¹ | i | imaginary ray |
i³ = −i is absorbed by the ℤ coefficient (x·(−i) = (−x)·i), so the tag set is exactly {i⁰, i¹, i²}. Every hidden number ⟨x, σ⟩ evaluates (hEval) to the complex number x·σ — a point on the real or imaginary axis (S ⊂ ℤ ∪ iℤ ⊂ ℂ), and every axis point is a hidden number.
The operation rules are adjusted to be i-consistent:
| Operation | Rule | Meaning |
|---|---|---|
hAdd/hSub |
⟨x,σ⟩ ± ⟨y,τ⟩ = ⟨x±y, S⟩ | collapse to the i⁰ ray (unchanged, A2a) |
hMulAdj |
exact ray product σ·τ | hEval(a×b) = hEval a · hEval b (complex-consistent) |
hSqrt |
↦ iR ray (unchanged, A3) | (iR)² = R because i² = −1 |
imul |
S → S (multiply by i) | hEval(imul h) = i·hEval h; closure under ×i |
Results formalized:
- Generation. The imaginary unit acts on S, and the whole hidden space is generated from the real ray by powers of i: ⟨x,iR⟩ = i¹·⟨x,S⟩, ⟨x,R⟩ = i²·⟨x,S⟩.
- Geometric origin of (A2b)/(A3). (xi)(yi) = −xy: the square of the imaginary ray is the
reflected real ray. The paper's flow-to-R collapse is exact exactly at i·i = −1
(
mul_agrees_on_iR_iR) — the single case where the exact ray product is real with tag R. - Embedding. z = a+bi ↦ (⟨a,S⟩, ⟨b,iR⟩): ℂ embeds into S by the i-power decomposition z = a·i⁰ ⊕ b·i¹.
- Axiom diagnostics (decided, 2026-08-13). A1 and A3 survive unchanged; A2b fails for
hMulAdj— the exact product stays in S instead of collapsing to ℝ. Decision (honest mathematics): in the derived structure,hMulAdjis the exact multiplication (identical to complex multiplication on the rays), and the paper's flow-to-R rule is its collapse — exact only at i·i = −1 (mul_agrees_on_iR_iR). The two multiplications coexist with distinct semantics:hMul(paper axiom A2b, collapses to ℝ) andhMulAdj(derived, exact). The reverse derivation trades the ×-asymmetry of the paper for ×-exactness: the irreversible operation moves to addition (1 + i collapses to ⟨2, S⟩, losing the imaginary part — the mirror image of the paper's one-way flow).
Liu & Xu, The Hidden-space Bridge System: A Three-axiom Foundation Connecting the Real and Imaginary Domains, 2025. HIBS.pdf
Hibs-Physics — the physics program built on these axioms: algebraic emergent physics (Representation Completeness, Kernel Null Theorem, the five bridges), formalized in Lean 4. Projection, kernel and observable-factorization theorems there generalize HIBS's π ∘ ι = id (Thm 6.5) into a research program: every observable is a function of the Image quadratic form and the Kernel scalar invariant.