A selected actual look-ahead refresh #
The honest refresh reads the original right source and uses either the first or second honest look-ahead output. Its law retains both original right inputs, all four look-ahead outputs, and the complete left state. The Boolean selector is true for the second output. This is the actual deterministic image of the source law, without a repaired coordinate.
noncomputable def
Algebraic.Cutwidth.Extractor.lookAheadSelectedRefreshWeight
{Z : Type u_1}
{A : Type u_2}
{B : Type u_3}
{X : Type u_4}
{Q : Type u_5}
{Seed : Type u_6}
{Mid : Type u_7}
{Y : Type u_8}
{Out : Type u_9}
[Fintype Z]
[Fintype A]
[Fintype B]
(w : Z → ℝ)
(l : Z → A → ℝ)
(r : Z → B → ℝ)
(x x' : Z → A → X)
(q q' : Z → B → Q)
(initialSeed : Q → Seed)
(W : X → Seed → Mid)
(QExt : Q → Mid → Seed)
(y : Z → B → Y)
(R : Y → Mid → Out)
(second : Bool)
:
(LookAheadBaseTranscript Z Q Mid × A) × Out → ℝ
Refresh from the selected honest output, retaining the full common history and left state.
Equations
- One or more equations did not get rendered due to their size.