RealFlow.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Real-valued causal conditional rows, mirroring the exact finite-flow proof. Uniform-computation Section 02, Proposition finite-table. This verifies the finite flow -> finite policy step, including every zero-marginal row. It is support, not an existence input.

structure OAI.UniformKServer.RealFlow.Data line 15
structure OAI.UniformKServer.RealFlow.Valid line 19
def OAI.UniformKServer.RealFlow.row line 31
Source documentation
All rows are explicitly defined, even outside the construction horizon.
```
def row (F : Data R C J) (fallback : C → R → J) (H : ℕ)
    (w : List R) (r : R) (c : C) (j : J) : ℝ :=
…
```
Mentions: OAI.UniformKServer.RealFlow.Data
def OAI.UniformKServer.RealFlow.cost line 36
def OAI.UniformKServer.RealFlow.flowCost line 41
theorem OAI.UniformKServer.RealFlow.zero_flow line 55
theorem OAI.UniformKServer.RealFlow.mass_row line 62
theorem OAI.UniformKServer.RealFlow.row_nonneg line 69
theorem OAI.UniformKServer.RealFlow.row_sum line 76
theorem OAI.UniformKServer.RealFlow.row_support line 83
theorem OAI.UniformKServer.RealFlow.inflow_average line 93
theorem OAI.UniformKServer.RealFlow.cost_average line 106

theorem OAI.UniformKServer.RealFlow.realization line 123

Source documentation

The precise finite flow realization obligation.

theorem realization (F : Data R C J) (T : C → R → J → C)
    (allowed : C → R → J → Prop) (initial : C) (H : ℕ)
    (fallback : C → R → J) (hfallback : ∀ c r, allowed c r (fallback c r))
    (hF : Valid F T allowed initial H) :
    (∀ w r c j, 0 ≤ row F fallback H w r c j) ∧
    (∀ w r c, ∑ j, row F fallback H w r c j = 1) ∧
    (∀ w r c j, ¬allowed c r j → row F fallback H w r c j = 0) ∧
    (∀ d rs, rs.length ≤ H → cost (row F fallback H) T d [] initial rs = flowCost F d [] rs) := by
…

Mentions: OAI.UniformKServer.RealFlow.Data, OAI.UniformKServer.initial, OAI.UniformKServer.RealFlow.Valid, OAI.UniformKServer.RealFlow.row, OAI.UniformKServer.RealFlow.cost, OAI.UniformKServer.RealFlow.flowCost