Representation.lean — FrcCore

1import FrcCore.Nat2import FrcCore.Shell3import FrcCore.Frame4import FrcCore.Sum5import FrcCore.Theme.Projective6import FrcCore.Keys.Projective78/-!9# 4-rep — universal latent representation: the ledger predicates with no axioms1011Rows of the predicate ledger of *Universal Latent Representation in Finite Ring Continuum* (Entropy 2026, 28, 40;12tree `4-deepfrc-20251217`).  The representation predicates are set theory over arbitrary types: a bijection is carried as13data (`Bij`: the map, its inverse, the two inverse laws), adequacy as a bijection through the observation map, and14every statement is pointwise, so neither function extensionality nor choice is used.  The Gödel row is decided on15two primes by induction, the hypersphere row in the shell's own arithmetic (the character chart has constant16conjugate norm).  Every declaration prints "does not depend on any axioms".17-/1819namespace FRC.Representation2021/-- A bijection as data: the map, an inverse, and the two inverse laws. -/22structure Bij (Z W : Type) where23  toFun : Z → W24  inv : W → Z25  left : ∀ z, inv (toFun z) = z26  right : ∀ w, toFun (inv w) = w2728/-- 4:B3 (Definition 2) — `E : X → W` is adequate for the observation map `g : Z → X` when `E ∘ g` is a29bijection `φ : Z → W` (carried as data), `E (g z) = φ z`. -/30structure Adequate {Z X W : Type} (g : Z → X) (E : X → W) where31  φ : Bij Z W32  eq : ∀ z, E (g z) = φ.toFun z3334variable {Z X W W₁ W₂ U : Type}3536/-- 4:B4 — adequacy makes the observation map injective on the latent domain: `g z₁ = g z₂ → z₁ = z₂`. -/37theorem adequate_inj {g : Z → X} {E : X → W} (A : Adequate g E) {z₁ z₂ : Z} (h : g z₁ = g z₂) : z₁ = z₂ := by38  have e : A.φ.toFun z₁ = A.φ.toFun z₂ := by rw [← A.eq, ← A.eq, h]39  rw [← A.φ.left z₁, ← A.φ.left z₂, e]4041/-- 4:B5 (Lemma 2) — the transition `ψ = φ₂ ∘ φ₁⁻¹` between two adequate representations of one observation map:42`E₂ (g z) = ψ (E₁ (g z))` for every latent state. -/43def transition {g : Z → X} {E₁ : X → W₁} {E₂ : X → W₂} (A₁ : Adequate g E₁) (A₂ : Adequate g E₂) : W₁ → W₂ :=44  fun w => A₂.φ.toFun (A₁.φ.inv w)4546/-- 4:B5 — `E₂ ∘ g = ψ ∘ E₁ ∘ g` pointwise. -/47theorem transition_spec {g : Z → X} {E₁ : X → W₁} {E₂ : X → W₂} (A₁ : Adequate g E₁) (A₂ : Adequate g E₂) (z : Z) :48    E₂ (g z) = transition A₁ A₂ (E₁ (g z)) := by49  unfold transition; rw [A₁.eq, A₁.φ.left, A₂.eq]5051/-- 4:B5 — the transition is a bijection `W₁ → W₂`: its inverse is `φ₁ ∘ φ₂⁻¹`. -/52def transitionBij {g : Z → X} {E₁ : X → W₁} {E₂ : X → W₂} (A₁ : Adequate g E₁) (A₂ : Adequate g E₂) : Bij W₁ W₂ where53  toFun := transition A₁ A₂54  inv := fun w => A₁.φ.toFun (A₂.φ.inv w)55  left := fun w => by show A₁.φ.toFun (A₂.φ.inv (A₂.φ.toFun (A₁.φ.inv w))) = w; rw [A₂.φ.left, A₁.φ.right]56  right := fun w => by show A₂.φ.toFun (A₁.φ.inv (A₁.φ.toFun (A₂.φ.inv w))) = w; rw [A₁.φ.left, A₂.φ.right]5758/-- 4:B5 (the uniqueness clause) — any `ψ'` with `E₂ (g z) = ψ' (E₁ (g z))` for every `z` agrees with the59transition on all of `W₁`, because `E₁ ∘ g` is onto `W₁`. -/60theorem transition_unique {g : Z → X} {E₁ : X → W₁} {E₂ : X → W₂} (A₁ : Adequate g E₁) (A₂ : Adequate g E₂)61    (ψ' : W₁ → W₂) (h : ∀ z, E₂ (g z) = ψ' (E₁ (g z))) (w : W₁) : ψ' w = transition A₁ A₂ w := by62  rw [← A₁.φ.right w, ← A₁.eq, ← h]; exact transition_spec A₁ A₂ _6364/-- 4:B6, 4:C2 (the canonical embedding into the shell) — with `incl : Z → U` the inclusion of the latent domain,65`ι := incl ∘ φ⁻¹ : W → U` is injective when `incl` is, and `ι (E (g z)) = incl z`: the chart `ψ = ι ∘ φ` is the66inclusion itself. -/67def iota {g : Z → X} {E : X → W} (A : Adequate g E) (incl : Z → U) : W → U := fun w => incl (A.φ.inv w)6869/-- 4:B6 — `ι` is injective when the inclusion is. -/70theorem iota_inj {g : Z → X} {E : X → W} (A : Adequate g E) {incl : Z → U}71    (hincl : ∀ z₁ z₂, incl z₁ = incl z₂ → z₁ = z₂) {w₁ w₂ : W} (h : iota A incl w₁ = iota A incl w₂) : w₁ = w₂ := by72  rw [← A.φ.right w₁, ← A.φ.right w₂, hincl _ _ h]7374/-- 4:C2 (Theorem 1 (iii)) — in the canonical parametrisation every chart is the inclusion: `ι (E (g z)) = incl z`. -/75theorem canonical_chart {g : Z → X} {E : X → W} (A : Adequate g E) (incl : Z → U) (z : Z) :76    iota A incl (E (g z)) = incl z := by77  unfold iota; rw [A.eq, A.φ.left]7879/-- 4:C1 (Theorem 1 (i)) — the chart `ψ = ι ∘ E ∘ g` is injective for any injective `ι`. -/80theorem chart_inj {g : Z → X} {E : X → W} (A : Adequate g E) {ι : W → U} (hι : ∀ w₁ w₂, ι w₁ = ι w₂ → w₁ = w₂)81    {z₁ z₂ : Z} (h : ι (E (g z₁)) = ι (E (g z₂))) : z₁ = z₂ := by82  have e : A.φ.toFun z₁ = A.φ.toFun z₂ := by rw [← A.eq, ← A.eq]; exact hι _ _ h83  rw [← A.φ.left z₁, ← A.φ.left z₂, e]8485/-- 4:C1 (Theorem 1 (ii)) — the transition `Ψ_{m→n} = ψ_n ∘ ψ_m⁻¹` is well defined and bijective between the images:86two latent states have the same `ψ_m`-image exactly when they have the same `ψ_n`-image, so the pairs87`(ψ_m z, ψ_n z)` are the graph of a bijection `ψ_m(Z) → ψ_n(Z)`. -/88theorem transition_graph {ψm ψn : Z → U} (hm : ∀ z₁ z₂, ψm z₁ = ψm z₂ → z₁ = z₂)89    (hn : ∀ z₁ z₂, ψn z₁ = ψn z₂ → z₁ = z₂) (z₁ z₂ : Z) : ψm z₁ = ψm z₂ ↔ ψn z₁ = ψn z₂ :=90  ⟨fun h => by rw [hm _ _ h], fun h => by rw [hn _ _ h]⟩9192/-- 4:C3 (Corollary 1) — the latent lift `L := φ⁻¹ ∘ E : X → Z`. -/93def lift {g : Z → X} {E : X → W} (A : Adequate g E) : X → Z := fun x => A.φ.inv (E x)9495/-- 4:C3 — the lift recovers the latent state, `L (g z) = z`. -/96theorem lift_g {g : Z → X} {E : X → W} (A : Adequate g E) (z : Z) : lift A (g z) = z := by97  unfold lift; rw [A.eq, A.φ.left]9899/-- 4:C3 — `L x` is the unique `z` with `E x = φ z`. -/100theorem lift_unique {g : Z → X} {E : X → W} (A : Adequate g E) (x : X) (z : Z) :101    E x = A.φ.toFun z ↔ lift A x = z := by102  constructor103  · intro h; unfold lift; rw [h, A.φ.left]104  · intro h; unfold lift at h; rw [← h, A.φ.right]105106/-- 4:C4 (Corollary 2) — cross-modal consistency: the lifts of two modalities' observations of one latent state107agree, `L_m (g_m z) = L_n (g_n z)`, hence so do their canonical charts `ψ ∘ L_m ∘ g_m = ψ = ψ ∘ L_n ∘ g_n`. -/108theorem consistency {Xm Xn Wm Wn : Type} {gm : Z → Xm} {gn : Z → Xn} {Em : Xm → Wm} {En : Xn → Wn}109    (Am : Adequate gm Em) (An : Adequate gn En) (incl : Z → U) (z : Z) :110    lift Am (gm z) = lift An (gn z) ∧ incl (lift Am (gm z)) = incl z := by111  rw [lift_g, lift_g]; exact ⟨rfl, rfl⟩112113/-! ### 4:E3 — Gödel collapse into one residue, the two-prime instance -/114115theorem three_pow_mod_two : ∀ b : Nat, 3 ^ b % 2 = 1116  | 0 => rfl117  | b + 1 => by118      rw [Nat.pow_succ, FRC.Nat.mul_mod _ _ 2 (Nat.zero_lt_succ 1), three_pow_mod_two b]119120theorem two_mul_mod_two (x : Nat) : 2 * x % 2 = 0 := by121  rw [FRC.Nat.mul_mod_left' 2 x 2 (Nat.zero_lt_succ 1)]122  show 0 * x % 2 = 0123  rw [Nat.zero_mul]124125theorem three_pow_inj : ∀ b d : Nat, 3 ^ b = 3 ^ d → b = d126  | 0, 0, _ => rfl127  | 0, d + 1, h => by128      have h1 : 1 * 3 ≤ 3 ^ d * 3 := Nat.mul_le_mul_right 3 (Nat.pow_pos (Nat.zero_lt_succ 2))129      have h' : 1 = 3 ^ d * 3 := h130      rw [← h'] at h1131      exact absurd h1 (by decide)132  | b + 1, 0, h => by133      have h1 : 1 * 3 ≤ 3 ^ b * 3 := Nat.mul_le_mul_right 3 (Nat.pow_pos (Nat.zero_lt_succ 2))134      have h' : 3 ^ b * 3 = 1 := h135      rw [h'] at h1136      exact absurd h1 (by decide)137  | b + 1, d + 1, h =>138      congrArg Nat.succ (three_pow_inj b d (Nat.eq_of_mul_eq_mul_right (Nat.zero_lt_succ 2) h))139140/-- 4:E3 (Gödel encoding, two primes) — `2^a 3^b = 2^c 3^d` forces `a = c` and `b = d`: the code is injective, by141parity and cancellation; the general case over `d` distinct primes is `FrcLedger.Representation.godel_injective`. -/142theorem godel2_inj : ∀ a c b d : Nat, 2 ^ a * 3 ^ b = 2 ^ c * 3 ^ d → a = c ∧ b = d143  | 0, 0, b, d, h => ⟨rfl, three_pow_inj b d (by rw [Nat.pow_zero, Nat.one_mul, Nat.one_mul] at h; exact h)⟩144  | 0, c + 1, b, d, h => by145      have hl : 2 ^ 0 * 3 ^ b % 2 = 1 := by rw [Nat.pow_zero, Nat.one_mul]; exact three_pow_mod_two b146      have hr : 2 ^ (c + 1) * 3 ^ d % 2 = 0 := by147        rw [Nat.pow_succ, FRC.Nat.mul_assoc, FRC.Nat.mul_left_comm]; exact two_mul_mod_two _148      rw [h] at hl; rw [hl] at hr; exact absurd hr (by decide)149  | a + 1, 0, b, d, h => by150      have hr : 2 ^ 0 * 3 ^ d % 2 = 1 := by rw [Nat.pow_zero, Nat.one_mul]; exact three_pow_mod_two d151      have hl : 2 ^ (a + 1) * 3 ^ b % 2 = 0 := by152        rw [Nat.pow_succ, FRC.Nat.mul_assoc, FRC.Nat.mul_left_comm]; exact two_mul_mod_two _153      rw [h] at hl; rw [hl] at hr; exact absurd hr (by decide)154  | a + 1, c + 1, b, d, h => by155      have h' : 2 * (2 ^ a * 3 ^ b) = 2 * (2 ^ c * 3 ^ d) := by156        rw [← FRC.Nat.mul_left_comm, ← FRC.Nat.mul_assoc, ← Nat.pow_succ, h, Nat.pow_succ, FRC.Nat.mul_assoc,157          FRC.Nat.mul_left_comm]158      have ih := godel2_inj a c b d (Nat.eq_of_mul_eq_mul_left (Nat.zero_lt_succ 1) h')159      exact ⟨congrArg Nat.succ ih.1, ih.2⟩160161/-- 4:E3 (the reduction into the shell) — an injective integer code with values below `q` stays injective162modulo `q`: `f a % q = f b % q` forces `f a = f b`. -/163theorem mod_injective {α : Type} (f : α → Nat) (q : Nat) (hq : ∀ a, f a < q) {a b : α}164    (h : f a % q = f b % q) : f a = f b := by165  rw [FRC.Nat.mod_eq_of_lt (hq a), FRC.Nat.mod_eq_of_lt (hq b)] at h; exact h166167/-! ### 4:E1 — the hypersphere in the shell's own arithmetic -/168169namespace Shell170171open FRC.Shell172173variable {p : Nat} [Pos p]174175/-- 4:E1 — the character chart of the shell, `z ↦ (g^{kz})_{k}`: the finite shadow of the Fourier embedding176`z ↦ (cos 2πkz/p, sin 2πkz/p)_k`. -/177def charChart (g : Shell p) (z k : Nat) : Shell p := g ^ (k * z)178179/-- 4:E1 (equivariance) — translation by `a` multiplies coordinate `k` by `g^{ka}`: the shell's translations act on180the chart coordinatewise, as the rotations act on the Fourier embedding. -/181theorem charChart_shift (g : Shell p) (z a k : Nat) : charChart g (z + a) k = g ^ (k * a) * charChart g z k := by182  unfold charChart; rw [Nat.mul_add, pow_add, mul_comm]183184/-- 4:E1 (constant norm) — the conjugate norm `Σ_{k<n} g^{kz} g^{k(n−z)}` of the chart equals `n = p − 1` for every185`z ≤ n`: every point of the chart lies on one sphere, exactly. -/186theorem charChart_norm {κ : Nat} {g : Shell p} (F : Frame p κ g) (z : Nat) (hz : z ≤ p - 1) :187    sumRange (fun k => charChart g z k * charChart g (p - 1 - z) k) (p - 1) = ofNat (p - 1) := by188  have e : ∀ k, k < p - 1 → charChart g z k * charChart g (p - 1 - z) k = (fun _ => (1 : Shell p)) k := by189    intro k _190    show g ^ (k * z) * g ^ (k * (p - 1 - z)) = 1191    rw [← pow_add, ← Nat.mul_add, FRC.Nat.add_sub_of_le hz, Nat.mul_comm, pow_mul, F.pow_n, one_pow]192  rw [sum_congr (p - 1) e, sum_const, mul_one]193194end Shell195196-- Ledger predicates of 4-representation (generated by make_predicates.py from docs/4-representation/4-representation-ledger.json; edit the ledger, not this section)197/-- 4:B4 (p04008) — Adequacy makes the observation map injective on the latent domain: $g_m(z)=g_m(z')$ forces $z=z'$; $\mathcal Z$ is the domain modality $m$ resolves completely. -/198theorem p04008 : ∀ {Z X W : Type} {g : Z → X} {E : X → W} (A : FRC.Representation.Adequate g E) {z₁ z₂ : Z}, g z₁ = g z₂ → z₁ = z₂ :=199  @FRC.Representation.adequate_inj200/-- 4:B5 (p04009) — Uniqueness up to bijection: for adequate $E_1$, $E_2$ of one $g$, $\psi=\varphi_2\circ\varphi_1^{-1}:W_1\to W_2$ is a bijection with $E_2\circ g=\psi\circ E_1\circ g$ --- $E_2=\psi\circ E_1$ on $g(\mathcal Z)$, on all of $\mathcal X$ when $\mathcal X=g(\mathcal Z)$; $\psi$ is the unique map with this property. Cited definitions (not proofs): FRC.Representation.transitionBij. -/201theorem p04009 : (∀ {Z X W₁ W₂ : Type} {g : Z → X} {E₁ : X → W₁} {E₂ : X → W₂} (A₁ : FRC.Representation.Adequate g E₁) (A₂ : FRC.Representation.Adequate g E₂) (z : Z), E₂ (g z) = FRC.Representation.transition A₁ A₂ (E₁ (g z))) ∧ ∀ {Z X W₁ W₂ : Type} {g : Z → X} {E₁ : X → W₁} {E₂ : X → W₂} (A₁ : FRC.Representation.Adequate g E₁) (A₂ : FRC.Representation.Adequate g E₂) (ψ' : W₁ → W₂), (∀ (z : Z), E₂ (g z) = ψ' (E₁ (g z))) → ∀ (w : W₁), ψ' w = FRC.Representation.transition A₁ A₂ w :=202  And.intro @FRC.Representation.transition_spec (@FRC.Representation.transition_unique)203/-- 4:B6 (p04010) — The embedding into the shell: $|W_m|=|\mathcal Z|\le\p$, so an injection $\iota_m:W_m\hookrightarrow\mathcal U_t$ exists --- the one place finiteness enters; canonically $\iota_m=\varphi_m^{-1}$ followed by the inclusion; $\psi_m:=\iota_m\circ\varphi_m:\mathcal Z\hookrightarrow\mathcal U_t$ is modality $m$'s chart of $\mathcal Z$. -/204theorem p04010 : ∀ {Z X W U : Type} {g : Z → X} {E : X → W} (A : FRC.Representation.Adequate g E) {incl : Z → U}, (∀ (z₁ z₂ : Z), incl z₁ = incl z₂ → z₁ = z₂) → ∀ {w₁ w₂ : W}, FRC.Representation.iota A incl w₁ = FRC.Representation.iota A incl w₂ → w₁ = w₂ :=205  @FRC.Representation.iota_inj206/-- 4:C1 (p04011) — Theorem~\ref{thm:UST} (i), (ii): every chart $\psi_m$ is injective, and $\Psi_{m\to n}:=\psi_n\circ\psi_m^{-1}:\psi_m(\mathcal Z)\to\psi_n(\mathcal Z)$ is a well-defined bijection, with $\Psi_{n\to k}\circ\Psi_{m\to n}=\Psi_{m\to k}$ and $\Psi_{m\to m}$ the identity. -/207theorem p04011 : (∀ {Z X W U : Type} {g : Z → X} {E : X → W} (A : FRC.Representation.Adequate g E) {ι : W → U}, (∀ (w₁ w₂ : W), ι w₁ = ι w₂ → w₁ = w₂) → ∀ {z₁ z₂ : Z}, ι (E (g z₁)) = ι (E (g z₂)) → z₁ = z₂) ∧ ∀ {Z U : Type} {ψm ψn : Z → U}, (∀ (z₁ z₂ : Z), ψm z₁ = ψm z₂ → z₁ = z₂) → (∀ (z₁ z₂ : Z), ψn z₁ = ψn z₂ → z₁ = z₂) → ∀ (z₁ z₂ : Z), ψm z₁ = ψm z₂ ↔ ψn z₁ = ψn z₂ :=208  And.intro @FRC.Representation.chart_inj (@FRC.Representation.transition_graph)209/-- 4:C2 (p04012) — Theorem~\ref{thm:UST} (iii): with $\iota_m=\varphi_m^{-1}$ every chart is the inclusion $\mathcal Z\hookrightarrow\mathcal U_t$ and $\psi(\mathcal Z)=\mathcal Z$; canonical structurally (unique once $\mathcal Z$ is fixed), not algorithmically; ``subspace'' means subset. -/210theorem p04012 : ∀ {Z X W U : Type} {g : Z → X} {E : X → W} (A : FRC.Representation.Adequate g E) (incl : Z → U) (z : Z), FRC.Representation.iota A incl (E (g z)) = incl z :=211  @FRC.Representation.canonical_chart212/-- 4:C3 (p04013) — The canonical lift $L_m:=\varphi_m^{-1}\circ E_m:\mathcal X_m\to\mathcal Z$ satisfies $L_m\circ g_m=\mathrm{id}_{\mathcal Z}$, and $L_m(x)$ is the unique $z$ with $E_m(x)=\varphi_m(z)$. -/213theorem p04013 : (∀ {Z X W : Type} {g : Z → X} {E : X → W} (A : FRC.Representation.Adequate g E) (z : Z), FRC.Representation.lift A (g z) = z) ∧ ∀ {Z X W : Type} {g : Z → X} {E : X → W} (A : FRC.Representation.Adequate g E) (x : X) (z : Z), E x = A.φ.toFun z ↔ FRC.Representation.lift A x = z :=214  And.intro @FRC.Representation.lift_g (@FRC.Representation.lift_unique)215/-- 4:C4 (p04014) — Cross-modal consistency: $\psi\circ L_m\circ g_m=\psi\circ L_n\circ g_n=\psi$ --- observations of one latent state lift to one point --- and $\iota_m(W_m)=\iota_n(W_n)=\psi(\mathcal Z)=\mathcal Z$. -/216theorem p04014 : ∀ {Z U Xm Xn Wm Wn : Type} {gm : Z → Xm} {gn : Z → Xn} {Em : Xm → Wm} {En : Xn → Wn} (Am : FRC.Representation.Adequate gm Em) (An : FRC.Representation.Adequate gn En) (incl : Z → U) (z : Z), FRC.Representation.lift Am (gm z) = FRC.Representation.lift An (gn z) ∧ incl (FRC.Representation.lift Am (gm z)) = incl z :=217  @FRC.Representation.consistency218set_option linter.defProp false in219/-- 4:C5 (p04015) — Charts of the shell itself: for $\mathcal Z=\Fp$ the charts respecting the arithmetic are the frames $x\mapsto a+bx$ (1:C2), $\p(\p-1)$ of them, and $\Psi_{m\to n}$ between two frames is the one affine map carrying the first to the second (simply transitive) --- the corpus's coordinate systems are the paper's charts. -/220def p04015 := @FRC.Ledger.p04015221/-- 4:E1 (p04018) — The hypersphere [chart]: a Euclidean chart $\mathrm{Emb}:\mathcal Z\to\R^{d}$ equivariant for a symmetry acting transitively on $\mathcal Z$ and orthogonally on $\R^{d}$ has constant norm --- $\mathrm{Emb}(\mathcal Z)\subset S^{d-1}$. The shell's character chart $z\mapsto(\cos2\pi kz/\p,\sin2\pi kz/\p)_{k}$ is such a chart under translation, $\|\mathrm{Emb}(z)\|^{2}=\p-1$; in the shell's arithmetic $\sum_{k}\g^{kz}\g^{k(n-z)}=n$ for every $z$. -/222theorem p04018 : (∀ {p : Nat} [FRC.Pos p] (g : FRC.Shell p) (z a k : Nat), FRC.Representation.Shell.charChart g (z + a) k = g ^ (k * a) * FRC.Representation.Shell.charChart g z k) ∧ ∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (z : Nat), z ≤ p - (1 : Nat) → FRC.Shell.sumRange (fun k => FRC.Representation.Shell.charChart g z k * FRC.Representation.Shell.charChart g (p - (1 : Nat) - z) k) (p - (1 : Nat)) = FRC.Shell.ofNat (p - (1 : Nat)) :=223  And.intro @FRC.Representation.Shell.charChart_shift (@FRC.Representation.Shell.charChart_norm)224/-- 4:E3 (p04020) — Gödel collapse: for distinct primes $p_1,\dots,p_d$ the code $G(x)=\prod p_i^{x_i}$ is injective on $\N^{d}$ (unique factorisation), and $G\bmod q$ stays injective on a finite set once $q$ exceeds its maximum; instance $d=3$, $x_i\le4$, primes $2,3,5$: $125$ codes, maximum $810\,000$, $q=810\,013$; signed coordinates are shifted first. -/225theorem p04020 : (∀ (a c b d : Nat), (2 : Nat) ^ a * (3 : Nat) ^ b = (2 : Nat) ^ c * (3 : Nat) ^ d → a = c ∧ b = d) ∧ ∀ {α : Type} (f : α → Nat) (q : Nat), (∀ (a : α), f a < q) → ∀ {a b : α}, f a % q = f b % q → f a = f b :=226  And.intro @FRC.Representation.godel2_inj (@FRC.Representation.mod_injective)227-- end ledger predicates228229end FRC.Representation230