`DirectedEulerLedgerSystem`

definition

show as: view math explainer →

module: IndisputableMonolith.NumberTheory.DirectedEulerLedger
domain: NumberTheory
line: 64 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.NumberTheory.DirectedEulerLedger on GitHub at line 64.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  61  exact reciprocal_primeEulerEvent_mem_sensorEulerLedger sensor (hST hp)
  62
  63/-- A directed system of concrete Euler ledgers attached to a single sensor. -/
  64structure DirectedEulerLedgerSystem (sensor : DefectSensor) where
  65  /-- The finite-stage ledger at a given prime support. -/
  66  stage : PrimeSupport → LedgerForcing.Ledger
  67  /-- Every finite stage is balanced. -/
  68  stage_balanced : ∀ support, LedgerForcing.balanced (stage support)
  69  /-- Hence every finite stage has zero net flow. -/
  70  stage_net_flow_zero :
  71    ∀ support agent, LedgerForcing.net_flow (stage support) agent = 0
  72  /-- Every prime in the support contributes both the Euler event and its
  73  reciprocal. -/
  74  stage_prime_pair :
  75    ∀ {support : PrimeSupport} {p : Nat.Primes}, p ∈ support →
  76      primeEulerEvent sensor.realPart (sensor_realPart_pos sensor) p ∈
  77          (stage support).events ∧
  78        LedgerForcing.reciprocal
  79          (primeEulerEvent sensor.realPart (sensor_realPart_pos sensor) p) ∈
  80            (stage support).events
  81  /-- Coherence under support enlargement: any prime already present in a
  82  smaller support remains present in every larger support. -/
  83  stage_prime_pair_mono :
  84    ∀ {S T : PrimeSupport} {p : Nat.Primes}, S ⊆ T → p ∈ S →
  85      primeEulerEvent sensor.realPart (sensor_realPart_pos sensor) p ∈
  86          (stage T).events ∧
  87        LedgerForcing.reciprocal
  88          (primeEulerEvent sensor.realPart (sensor_realPart_pos sensor) p) ∈
  89            (stage T).events
  90  /-- Directedness of the support index set. -/
  91  directed_support :
  92    ∀ S T : PrimeSupport, ∃ U : PrimeSupport, S ⊆ U ∧ T ⊆ U
  93  /-- Explicit stage cost formula. -/
  94  stage_cost_formula :

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.