Foundation Topological Conservation Charge To Axis Bijective

The charge-axis correspondence

In physics, a conservation law says some quantity stays the same as a system evolves. Electric charge, baryon number, and lepton number are familiar examples. In the Recognition Science framework, these conserved quantities are modeled as linking numbers: integers that count how many times one structure winds around another. The framework's library proves that such charges are exactly conserved along any allowed trajectory, and that they take integer values only.

The declaration charge_to_axis_bijective establishes a precise correspondence in three dimensions. It proves that the map from the three standard charges (electric, baryon, lepton) to the three axes of three-dimensional space is bijective: each charge corresponds to exactly one axis, and every axis has exactly one charge. This is a formal theorem in the machine-checked library of formal theorems, not a physical measurement or a heuristic argument.

The framework derives this from topology rather than symmetry. In the standard Noether approach, conservation laws come from continuous symmetries of a system. The framework instead models conservation as a topological invariant: linking numbers cannot change under continuous deformation, so they are automatically conserved. The theorem three_charges_at_D3 shows that in exactly three dimensions, the framework supports exactly three independent charges, and no_charges_at_other_D shows that other dimensions support none.

What the declaration does not claim is equally important. It does not claim that electric charge, baryon number, or lepton number in the real world are actually linking numbers; that identification is a modeling choice, not a theorem. It does not claim that Noether's theorem is wrong. The framework proves that Noether charges need not be integers, but it does not prove that topological conservation replaces symmetry-based conservation in all cases. The bijection itself is a formal result about the framework's definitions, not an empirical fact about particle physics.

Within the framework, this correspondence is what makes three dimensions special. The framework proves that conservation laws arise from linking, and linking requires three dimensions. The bijection between charges and axes is the structural consequence: in this account, the three conserved quantities are not arbitrary, they are the three axes of space themselves.

theorem charge_to_axis_bijective : Function.Bijective charge_to_axis :=
  ⟨charge_to_axis_injective, charge_to_axis_surjective⟩

/-- **THEOREM (Exact Conservation Along Trajectories)** -/
theorem topological_charge_trajectory_conserved {N : ℕ} (Q : TopologicalCharge N)
    (traj : Trajectory N) (h : IsVariationalTrajectory traj) :
    ∀ t, Q.value (traj t) = Q.value (traj 0) := by
  intro t
  induction t with
  | zero => rfl
  | succ n ih => rw [← ih]; exact Q.conserved (traj n) (traj (n + 1)) (h n)

/-- **THEOREM (Quantization Is Automatic)**:
    Every topological charge takes integer values. -/
theorem topological_charge_quantized {N : ℕ} (Q : TopologicalCharge N)
    (c : Configuration N) : ∃ n : ℤ, Q.value c = n :=
  ⟨Q.value c, rfl⟩

theorem three_charges_at_D3 : independent_charge_count 3 = 3 := by
  simp [independent_charge_count]

/-- **THEOREM (Noether Charges Need Not Be Quantized)**:
    There exist Noether charges that take non-integer values.

    Proof: log(2) satisfies 0 < log(2) < 1, so it is not an integer. -/
theorem noether_not_necessarily_quantized :
    ∃ (N : ℕ) (Q : NoetherCharge N) (c : Configuration N),
      ¬∃ n : ℤ, Q.value c = (n : ℝ) := by
  use 1, logChargeAsNoether 1
  let c : Configuration 1 := {
    entries := fun _ => 2
    entries_pos := fun _ => by norm_num
  }
  use c
  intro ⟨n, hn⟩
  simp only [logChargeAsNoether, log_charge, Fin.sum_univ_one] at hn
  have h_pos : 0 < Real.log 2 := Real.log_pos (by norm_num : (1 : ℝ) < 2)
  have h_lt : Real.log 2 < 1 := by
    have h2_lt_e : (2 : ℝ) < Real.exp 1 := by
      exact lt_trans (by norm_num) Real.exp_one_gt_d9
    calc Real.log 2 < Real.log (Real.exp 1) :=
          Real.log_lt_log (by norm_num) h2_lt_e
      _ = 1 := Real.log_exp 1
  have h1 : (0 : ℝ) < n := by linarith
  have h2 : (n : ℝ) < 1 := by linarith
  have h3 : (0 : ℤ) < n := Int.cast_pos.mp h1
  have h4 : n < (1 : ℤ) := by exact_mod_cast h2
  omega

What this page does not claim

The identification of real-world electric charge, baryon number, or lepton number as linking numbers is a modeling choice, not a theorem. The framework does not prove that topological conservation replaces Noether's theorem in all physical contexts. The bijection is a formal result about the framework's definitions, not an empirical measurement of particle physics.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/TopologicalConservation.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: