PoweringOpinionTables.lean`

116 declarations, 0 contain sorry, 0 declared as axioms

Bounded first-address tables for actual powering constraints

For a graph with numbered vertices and ports, each stored local-opinion index is the first address in allAddresses that reaches the requested vertex. The search traverses bounded port words, never the ambient vertex set.

The walk table stores one base dart and two address indices per traversed edge. Looking up the endpoint labels at those indices gives exactly the existing finitePortSelector decoders, including when addresses collide. The resulting finite table predicate equals the actual powering predicate.

theorem OAI.MaxCutGames.Foundations.PCP.PoweringOpinionTables.match_in_tail_inline_PoweringOpinionTables line 26
def OAI.MaxCutGames.Foundations.PCP.PoweringOpinionTables.firstIndex line 33
theorem OAI.MaxCutGames.Foundations.PCP.PoweringOpinionTables.get_firstIndex line 42
Source documentation
The stored index selects the very same first address as scanWitness, not just an address with the same endpoint.
```
theorem get_firstIndex (p : X → Prop) [DecidablePred p] :
    ∀ (xs : List X) (h : ∃ a ∈ xs, p a),
      xs.get (firstIndex p xs h) = (scanWitness p xs h).val := by
…
```
Mentions: OAI.MaxCutGames.Foundations.PCP.PoweringOpinionTables.firstIndex
theorem OAI.MaxCutGames.Foundations.PCP.PoweringOpinionTables.firstIndex_matches line 55
theorem OAI.MaxCutGames.Foundations.PCP.PoweringOpinionTables.firstIndex_is_first line 61
Source documentation
Every earlier stored address fails the matching predicate.
```
theorem firstIndex_is_first (p : X → Prop) [DecidablePred p] :
    ∀ (xs : List X) (h : ∃ a ∈ xs, p a) (j : Fin xs.length),
      j.val < (firstIndex p xs h).val → ¬p (xs.get j) := by
…
```
Mentions: OAI.MaxCutGames.Foundations.PCP.PoweringOpinionTables.firstIndex
abbrev OAI.MaxCutGames.Foundations.PCP.PoweringOpinionTables.AddressIndex line 78
Source documentation
A local label slot is an index into the explicit bounded address list.
```
abbrev AddressIndex (d t : Nat) := Fin (allAddresses d t).length
…
```
def OAI.MaxCutGames.Foundations.PCP.PoweringOpinionTables.addressIndex line 82
theorem OAI.MaxCutGames.Foundations.PCP.PoweringOpinionTables.addressIndex_get line 89
theorem OAI.MaxCutGames.Foundations.PCP.PoweringOpinionTables.addressIndex_matches line 98
theorem OAI.MaxCutGames.Foundations.PCP.PoweringOpinionTables.addressIndex_is_first line 104
theorem OAI.MaxCutGames.Foundations.PCP.PoweringOpinionTables.addressIndex_lt line 111
Source documentation
The address bound depends on degree and radius, not the vertex count.
```
theorem addressIndex_lt (G : PortGraph (Fin vertices) (Fin d)) (t : Nat)
    (center : Fin vertices) (u : Ball G t center) :
    (addressIndex G t center u).val < ∑ n : Fin (t + 1), d ^ n.val := by
…
```
Mentions: OAI.MaxCutGames.Foundations.PCP.PoweringOpinionTables.addressIndex
abbrev OAI.MaxCutGames.Foundations.PCP.PoweringOpinionTables.LabelTable line 117
def OAI.MaxCutGames.Foundations.PCP.PoweringOpinionTables.labelTable line 120
Source documentation
Materialize a padded label in the common address order.
```
def labelTable {t : Nat} (a : PaddedLabel (Fin d) t A) : LabelTable d t A :=
…
```
Mentions: OAI.MaxCutGames.Foundations.PCP.PoweringOpinionTables.LabelTable
theorem OAI.MaxCutGames.Foundations.PCP.PoweringOpinionTables.labelTable_get line 123
theorem OAI.MaxCutGames.Foundations.PCP.PoweringOpinionTables.labelTable_addressIndex line 130
Source documentation
Exact evaluation bridge for every local target, with no consistency assumption on labels at distinct addresses that reach the same vertex.
```
theorem labelTable_addressIndex (G : PortGraph (Fin vertices) (Fin d)) (t : Nat)
    (center : Fin vertices) (u : Ball G t center) (a : PaddedLabel (Fin d) t A) :
    (labelTable a)[addressIndex G t center u] =
      decode (finitePortSelector G t center) a u := by
…
```
Mentions: OAI.MaxCutGames.Foundations.PCP.PoweringOpinionTables.labelTable, OAI.MaxCutGames.Foundations.PCP.PoweringOpinionTables.addressIndex
structure OAI.MaxCutGames.Foundations.PCP.PoweringOpinionTables.WalkOpinionRow line 138
Source documentation
One finite row for each constraint checked along a recorded walk.
```
structure WalkOpinionRow (vertices d t : Nat) where
…
```
abbrev OAI.MaxCutGames.Foundations.PCP.PoweringOpinionTables.WalkRows line 143
def OAI.MaxCutGames.Foundations.PCP.PoweringOpinionTables.walkRows line 146
Source documentation
The only target vertices inspected are the actual edge endpoints.
```
def walkRows (G : PortGraph (Fin vertices) (Fin d)) (n : Nat)
    (w : Walk (Fin vertices) (Fin d) (n + 1)) : WalkRows vertices d n :=
…
```
Mentions: OAI.MaxCutGames.Foundations.PCP.PoweringOpinionTables.WalkRows
theorem OAI.MaxCutGames.Foundations.PCP.PoweringOpinionTables.walkRows_edge line 153
theorem OAI.MaxCutGames.Foundations.PCP.PoweringOpinionTables.walkRows_tail_value line 158
theorem OAI.MaxCutGames.Foundations.PCP.PoweringOpinionTables.walkRows_head_value line 166
theorem OAI.MaxCutGames.Foundations.PCP.PoweringOpinionTables.walkRows_length line 174
def OAI.MaxCutGames.Foundations.PCP.PoweringOpinionTables.rowsAccepts line 181
Source documentation
Evaluate an already stored row vector by finite label lookups. The only quantified type is the bounded set of walk positions.
```
def rowsAccepts {n : Nat} (accepts : Edge (Fin vertices) (Fin d) → A → A → Bool)
    (rows : WalkRows vertices d n) (a b : LabelTable d (n + 1) A) : Bool :=
…
```
Mentions: OAI.MaxCutGames.Foundations.PCP.accepts, OAI.MaxCutGames.Foundations.PCP.PoweringOpinionTables.WalkRows, OAI.MaxCutGames.Foundations.PCP.PoweringOpinionTables.LabelTable
theorem OAI.MaxCutGames.Foundations.PCP.PoweringOpinionTables.rowsAccepts_walkRows line 187
Source documentation
The stored finite lookup predicate implements the actual powering test.
```
theorem rowsAccepts_walkRows (G : PortGraph (Fin vertices) (Fin d))
    (accepts : Edge (Fin vertices) (Fin d) → A → A → Bool) (n : Nat)
    (w : Walk (Fin vertices) (Fin d) (n + 1))
    (a b : PaddedLabel (Fin d) (n + 1) A) :
    rowsAccepts accepts (walkRows G n w) (labelTable a) (labelTable b) =
      PoweringTest.pathAccepts G accepts n (finitePortSelector G (n + 1)) w a b := by
…
```
Mentions: OAI.MaxCutGames.Foundations.PCP.accepts, OAI.MaxCutGames.Foundations.PCP.PoweringOpinionTables.rowsAccepts, OAI.MaxCutGames.Foundations.PCP.PoweringOpinionTables.walkRows, OAI.MaxCutGames.Foundations.PCP.PoweringOpinionTables.labelTable, OAI.MaxCutGames.Foundations.PCP.PoweringTest.pathAccepts
abbrev OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.Label line 214
abbrev OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.RelationTable line 215
def OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.relationIndex line 220
Source documentation
The fixed row-major ordering of the complete predicate table.
```
def relationIndex (q : Nat) : (Label q) × (Label q) ≃ Fin (q * q) := finProdFinEquiv
```
Mentions: OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.Label
theorem OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.relationIndex_val line 222
def OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.relationAt line 225
def OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.relationOf line 228
theorem OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.relationAt_relationOf line 231
structure OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.DartRow line 236
Source documentation
The row itself is finite data; index bounds are checked while parsing.
```
structure DartRow (q vertices darts : Nat) where
…
```
abbrev OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.Rows line 241
def OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.reverseAt line 243
def OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.acceptsAt line 246
def OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.Valid line 250
Source documentation
The two graph laws are decidable finite checks on the stored rows.
```
def Valid {n m : Nat} (rows : Rows q n m) : Prop :=
…
```
Mentions: OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.Rows
instance OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.(instance at line 254) line 254
structure OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.Table line 258
def OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.rowList line 265
Source documentation
The ordered list serialized by the codec. Equal rows remain separate.
```
def rowList (table : (Table q)) : List (DartRow q table.vertices table.darts) := table.rows.toList
```
Mentions: OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.Table, OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.DartRow
theorem OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.rowList_length line 267
def OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.semantics line 271
Source documentation
Decode validated finite data into the actual constraint-graph semantics.
```
def semantics (table : (Table q)) : ConstraintGraph (Fin table.vertices) (Fin table.darts) (Label q) where
…
```
Mentions: OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.Table, OAI.MaxCutGames.Foundations.PCP.ConstraintGraph, OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.Label
theorem OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.semantics_reverse line 282
theorem OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.semantics_tail line 285
theorem OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.semantics_accepts line 288
def OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.graphRows line 291
theorem OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.reverseAt_graphRows line 294
theorem OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.acceptsAt_graphRows line 299
theorem OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.graphRows_valid line 304
def OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.ofGraph line 312
theorem OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.semantics_ofGraph_reverse line 315
theorem OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.semantics_ofGraph_tail line 320
theorem OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.semantics_ofGraph_accepts line 326
theorem OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.semantics_ofGraph_edgeSatisfied line 331
theorem OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.constraintGraph_ext_inline_GenericGraphTables line 336
theorem OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.semantics_ofGraph line 351
Source documentation
Complete semantic graph roundtrip, including its actual reversal map.
```
@[simp] theorem semantics_ofGraph {n m : Nat}
    (G : ConstraintGraph (Fin n) (Fin m) (Label q)) : semantics (ofGraph G) = G := by
…
```
Mentions: OAI.MaxCutGames.Foundations.PCP.ConstraintGraph, OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.Label, OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.semantics, OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.ofGraph
theorem OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.semantics_ofGraph_rejectionCount line 360
def OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.enumeratedGraph line 368
Source documentation
Explicit enumerations determine every vertex name, dart position, and predicate label. No hidden choice of a graph representation is made.
```
def enumeratedGraph {V E A : Type*} {n m : Nat} (G : ConstraintGraph V E A)
    (vertexOrder : V ≃ Fin n) (dartOrder : E ≃ Fin m) (labelOrder : A ≃ (Label q)) :
    ConstraintGraph (Fin n) (Fin m) (Label q) where
…
```
Mentions: OAI.MaxCutGames.Foundations.PCP.ConstraintGraph, OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.Label
theorem OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.enumeratedGraph_edgeSatisfied line 384

theorem OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.enumeratedGraph_rejectionCount line 393

Source documentation

Every directed occurrence contributes once before and after enumeration.

theorem enumeratedGraph_rejectionCount {V E A : Type*} [Fintype E] {n m : Nat}
    (G : ConstraintGraph V E A) (vertexOrder : V ≃ Fin n) (dartOrder : E ≃ Fin m)
    (labelOrder : A ≃ (Label q)) (labeling : V → A) :
    (enumeratedGraph G vertexOrder dartOrder labelOrder).rejectionCount
      (fun v => labelOrder (labeling (vertexOrder.symm v))) = G.rejectionCount labeling := by
…

Mentions: OAI.MaxCutGames.Foundations.PCP.ConstraintGraph, OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.Label, OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.enumeratedGraph

def OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.ofEnumeratedGraph line 405
def OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.bitWord line 409
def OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.parseBit line 411
theorem OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.parseBit_bitWord line 416
theorem OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.parseBits_bitWords line 419
def OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.relationWords line 425
theorem OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.relationWords_length line 427
def OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.parseRelation line 430
theorem OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.parseRelation_encoded line 436
def OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.rowWords line 443
def OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.parseRow line 446
theorem OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.parseRow_encoded line 454
def OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.parseRows line 462
theorem OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.parseRows_encoded line 470
def OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.tableWords line 476
def OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.tableBits line 479
def OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.decodeTableWords line 481
theorem OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.decodeTableWords_encoded line 492
def OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.decodeTableBits line 500
theorem OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.decodeTableBits_encoded line 503
def OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.encoding line 508
Source documentation
A concrete encoding for the fixed alphabet, suitable for the existing TM2 computation interface.
```
def encoding (q : Nat) : Computability.Encoding (Table q) Bool where
…
```
Mentions: OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.Table
theorem OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.tableBits_injective line 513
theorem OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.rowWords_length line 515
theorem OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.rowsWords_length line 521
theorem OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.tableWords_length line 527
theorem OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.tableWords_length_le_bits line 534
Source documentation
At least one unary delimiter is stored for every field, including all (q * q) entries of every predicate table.
```
theorem tableWords_length_le_bits (table : (Table q)) :
    2 + (q * q + 2) * table.darts ≤ (tableBits table).length := by
…
```
Mentions: OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.Table, OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.tableBits
theorem OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.relationBits_length_le line 539
theorem OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.rowBits_length_le line 547
theorem OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.rowsBits_length_le line 556
theorem OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.tableBits_length_le line 568
Source documentation
Full unary size bound: headers, both bounded indices in every row, and every Boolean predicate entry are counted. This is not a runtime assertion.
```
theorem tableBits_length_le (table : (Table q)) :
    (tableBits table).length ≤ table.vertices + table.darts + 2 +
      table.darts * (table.vertices + table.darts + (2 * (q * q))) := by
…
```
Mentions: OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.Table, OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.tableBits
theorem OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.vertices_le_tableBits_length line 577
theorem OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.darts_le_tableBits_length line 583
def OAI.MaxCutGames.Foundations.PCP.PoweringTables.labelCount line 606
Source documentation
Program-constant output alphabet size for degree d and walk length n+1.
```
def labelCount (d n : Nat) : Nat := 64 ^ addressCount d (n + 1)
```
def OAI.MaxCutGames.Foundations.PCP.PoweringTables.dartCount line 609
Source documentation
Number of directed recorded-walk occurrences, including orientation.
```
def dartCount (vertices d n : Nat) : Nat := 2 * vertices * d ^ (n + 1)
```
def OAI.MaxCutGames.Foundations.PCP.PoweringTables.mathematicalGraph line 611
def OAI.MaxCutGames.Foundations.PCP.PoweringTables.rowAccepts line 618
Source documentation
The finite first-address predicate evaluator used for each stored row.
```
def rowAccepts {vertices d : Nat} (input : PortTables.Table vertices d) (n : Nat)
    (e : PoweringTest.Dart (Fin vertices) (Fin d) n)
    (a b : Fin (labelCount d n)) : Bool :=
…
```
Mentions: OAI.MaxCutGames.Foundations.PCP.PortTables.Table, OAI.MaxCutGames.Foundations.PCP.PoweringTest.Dart, OAI.MaxCutGames.Foundations.PCP.PoweringTables.labelCount
theorem OAI.MaxCutGames.Foundations.PCP.PoweringTables.rowAccepts_eq line 627
def OAI.MaxCutGames.Foundations.PCP.PoweringTables.table line 637
theorem OAI.MaxCutGames.Foundations.PCP.PoweringTables.table_vertices line 642
theorem OAI.MaxCutGames.Foundations.PCP.PoweringTables.table_darts line 645
theorem OAI.MaxCutGames.Foundations.PCP.PoweringTables.semantics_table line 649
Source documentation
Complete decoded semantics, with executable vertex, dart and label orders.
```
theorem semantics_table {vertices d : Nat} (input : PortTables.Table vertices d) (n : Nat) :
    GenericGraphTables.semantics (table input n) =
      GenericGraphTables.enumeratedGraph (mathematicalGraph input n) (Equiv.refl _)
        (dartEquiv vertices d n) (paddedLabelEquiv d (n + 1) 64) :=
…
```
Mentions: OAI.MaxCutGames.Foundations.PCP.PortTables.Table, OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.semantics, OAI.MaxCutGames.Foundations.PCP.PoweringTables.table, OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.enumeratedGraph, OAI.MaxCutGames.Foundations.PCP.PoweringTables.mathematicalGraph
theorem OAI.MaxCutGames.Foundations.PCP.PoweringTables.table_accepts line 656
Source documentation
Each actual output relation entry is the bounded stored-opinion evaluator.
```
theorem table_accepts {vertices d : Nat} (input : PortTables.Table vertices d) (n : Nat)
    (i : Fin (dartCount vertices d n)) (a b : Fin (labelCount d n)) :
    GenericGraphTables.acceptsAt (table input n).rows i a b =
      rowAccepts input n (decodeDart vertices d n i) a b := by
…
```
Mentions: OAI.MaxCutGames.Foundations.PCP.PortTables.Table, OAI.MaxCutGames.Foundations.PCP.PoweringTables.dartCount, OAI.MaxCutGames.Foundations.PCP.PoweringTables.labelCount, OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.acceptsAt, OAI.MaxCutGames.Foundations.PCP.PoweringTables.table, OAI.MaxCutGames.Foundations.PCP.PoweringTables.rowAccepts
theorem OAI.MaxCutGames.Foundations.PCP.PoweringTables.table_reverse line 665
Source documentation
The reverse row flips just the orientation in the recorded-walk encoding.
```
theorem table_reverse {vertices d : Nat} (input : PortTables.Table vertices d) (n : Nat)
    (direction : Bool) (w : Walk (Fin vertices) (Fin d) (n + 1)) :
    GenericGraphTables.reverseAt (table input n).rows (encodeDart vertices d n (direction, w)) =
      encodeDart vertices d n (!direction, w) := by
…
```
Mentions: OAI.MaxCutGames.Foundations.PCP.PortTables.Table, OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.reverseAt, OAI.MaxCutGames.Foundations.PCP.PoweringTables.table
def OAI.MaxCutGames.Foundations.PCP.PoweringTables.outputBits line 678
Source documentation
Serialized output in the shared generic graph codec.
```
def outputBits {vertices d : Nat} (input : PortTables.Table vertices d) (n : Nat) : List Bool :=
…
```
Mentions: OAI.MaxCutGames.Foundations.PCP.PortTables.Table
def OAI.MaxCutGames.Foundations.PCP.PoweringTables.transform line 682
Source documentation
The actual function on variable-size regular input tables.
```
def transform (d n : Nat) (input : PortTables.Input d) : GenericGraphTables.Table (labelCount d n) :=
…
```
Mentions: OAI.MaxCutGames.Foundations.PCP.PortTables.Input, OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.Table, OAI.MaxCutGames.Foundations.PCP.PoweringTables.labelCount
theorem OAI.MaxCutGames.Foundations.PCP.PoweringCounting.constraint_rejection_mean_eq_count line 706
Source documentation
An arbitrary constraint graph's rejection probability is its actual rejected-dart cardinal ratio, including the empty-dart case.
```
theorem constraint_rejection_mean_eq_count [Fintype E]
    (H : ConstraintGraph V E A) (labels : V → A) :
    SpectralReturn.mean (fun e : E => PoweringMoment.bit
      (H.edgeSatisfied labels e = false)) =
      (H.rejectionCount labels : ℝ) / (Fintype.card E : ℝ) := by
…
```
Mentions: OAI.MaxCutGames.Foundations.PCP.ConstraintGraph, OAI.MaxCutGames.Foundations.PCP.SpectralReturn.mean, OAI.MaxCutGames.Foundations.PCP.PoweringMoment.bit
theorem OAI.MaxCutGames.Foundations.PCP.PoweringCounting.constraint_rejection_lower_iff line 722
Source documentation
Multiplying a normalized lower bound by the actual positive dart count.
```
theorem constraint_rejection_lower_iff [Fintype E]
    (H : ConstraintGraph V E A) (labels : V → A)
    (hcard : 0 < Fintype.card E) (ε : ℝ) :
    ε ≤ SpectralReturn.mean (fun e : E => PoweringMoment.bit
      (H.edgeSatisfied labels e = false)) ↔
      ε * (Fintype.card E : ℝ) ≤ (H.rejectionCount labels : ℝ) := by
…
```
Mentions: OAI.MaxCutGames.Foundations.PCP.ConstraintGraph, OAI.MaxCutGames.Foundations.PCP.SpectralReturn.mean, OAI.MaxCutGames.Foundations.PCP.PoweringMoment.bit
theorem OAI.MaxCutGames.Foundations.PCP.PoweringCounting.edgeDensity_eq_bit_mean line 733
Source documentation
The edge-profile definition equals its actual directed-edge indicator mean without any nonemptiness assumption on vertices or ports.
```
theorem edgeDensity_eq_bit_mean [Fintype V] [Fintype D]
    (bad : Edge V D → Bool) :
    SpectralReturn.edgeDensity bad =
      SpectralReturn.mean (fun e : Edge V D => PoweringMoment.bit (bad e = true)) := by
…
```
Mentions: OAI.MaxCutGames.Foundations.PCP.SpectralReturn.edgeDensity, OAI.MaxCutGames.Foundations.PCP.SpectralReturn.mean, OAI.MaxCutGames.Foundations.PCP.PoweringMoment.bit

theorem OAI.MaxCutGames.Foundations.PCP.PoweringCounting.base_edgeDensity_eq_rejection_count line 748

Source documentation

Decoded badness is exactly rejection in the actual base constraint graph.

theorem base_edgeDensity_eq_rejection_count [Fintype V] [Fintype D]
    (G : PortGraph V D) (accepts : Edge V D → A → A → Bool)
    (reverse_accepts : ∀ e a b, accepts (G.rot e) b a = accepts e a b)
    (assignment : V → A) :
    SpectralReturn.edgeDensity (decodedBad G accepts assignment) =
      ((baseGraph G accepts reverse_accepts).rejectionCount assignment : ℝ) /
        (Fintype.card (Edge V D) : ℝ) := by
…

Mentions: OAI.MaxCutGames.Foundations.PCP.accepts, OAI.MaxCutGames.Foundations.PCP.SpectralReturn.edgeDensity

theorem OAI.MaxCutGames.Foundations.PCP.PoweringCounting.base_count_lower_to_density line 766

theorem OAI.MaxCutGames.Foundations.PCP.PoweringCounting.powered_rejection_mean_eq_count line 778

Source documentation

The actual powered graph's directed-dart average is its rejected-dart fraction. No nonemptiness premise is needed for this identity.

theorem powered_rejection_mean_eq_count [Fintype V] [Fintype D]
    (G : PortGraph V D) (accepts : Edge V D → A → A → Bool) (n : Nat)
    (selectors : ∀ v, AddressSelector G (n + 1) v)
    (labels : V → PaddedLabel D (n + 1) A) :
    SpectralReturn.mean (fun d : Dart V D n => PoweringMoment.bit
      ((poweredGraph G accepts n selectors).edgeSatisfied labels d = false)) =
      ((poweredGraph G accepts n selectors).rejectionCount labels : ℝ) /
        (Fintype.card (Dart V D n) : ℝ) :=
…

Mentions: OAI.MaxCutGames.Foundations.PCP.accepts, OAI.MaxCutGames.Foundations.PCP.SpectralReturn.mean, OAI.MaxCutGames.Foundations.PCP.PoweringMoment.bit

theorem OAI.MaxCutGames.Foundations.PCP.PoweringCounting.path_rejection_mean_eq_count line 790

Source documentation

The recorded-walk rejection average used in soundness is the actual powered graph's rejected-dart fraction.

theorem path_rejection_mean_eq_count [Fintype V] [Fintype D]
    (G : PortGraph V D) (accepts : Edge V D → A → A → Bool) (n : Nat)
    (selectors : ∀ v, AddressSelector G (n + 1) v)
    (labels : V → PaddedLabel D (n + 1) A) :
    SpectralReturn.mean (fun w : Walk V D (n + 1) => PoweringMoment.bit
      (pathAccepts G accepts n selectors w (labels w.1) (labels (endpoint G w)) = false)) =
      ((poweredGraph G accepts n selectors).rejectionCount labels : ℝ) /
        (Fintype.card (Dart V D n) : ℝ) := by
…

Mentions: OAI.MaxCutGames.Foundations.PCP.accepts, OAI.MaxCutGames.Foundations.PCP.SpectralReturn.mean, OAI.MaxCutGames.Foundations.PCP.PoweringMoment.bit

theorem OAI.MaxCutGames.Foundations.PCP.PoweringCounting.powered_density_lower_to_count line 803

Source documentation

Convert a proved path-test rejection lower bound into the actual powered constraint graph's rejected-dart count inequality.

theorem powered_density_lower_to_count [Fintype V] [Fintype D]
    (G : PortGraph V D) (accepts : Edge V D → A → A → Bool) (n : Nat)
    (selectors : ∀ v, AddressSelector G (n + 1) v)
    (labels : V → PaddedLabel D (n + 1) A)
    (hcard : 0 < Fintype.card (Dart V D n)) (ε : ℝ)
    (hlower : ε ≤ SpectralReturn.mean (fun w : Walk V D (n + 1) => PoweringMoment.bit
      (pathAccepts G accepts n selectors w (labels w.1) (labels (endpoint G w)) = false))) :
    ε * (Fintype.card (Dart V D n) : ℝ) ≤
      ((poweredGraph G accepts n selectors).rejectionCount labels : ℝ) := by
…

Mentions: OAI.MaxCutGames.Foundations.PCP.accepts, OAI.MaxCutGames.Foundations.PCP.SpectralReturn.mean, OAI.MaxCutGames.Foundations.PCP.PoweringMoment.bit

theorem OAI.MaxCutGames.Foundations.PCP.PoweringCounting.natCard_dart line 817
Source documentation
Exact size of the powered dart type, retaining both direction flags and all recorded port words, including repeated vertices and edges.
```
theorem natCard_dart [Finite V] [Finite D] (n : Nat) :
    Nat.card (Dart V D n) = 2 * Nat.card V * Nat.card D ^ (n + 1) := by
…
```
theorem OAI.MaxCutGames.Foundations.PCP.PoweringCounting.fintypeCard_dart line 821
theorem OAI.MaxCutGames.Foundations.PCP.PoweringCounting.natCard_poweredAlphabet line 828
Source documentation
The common powered alphabet size depends only on degree, radius, and the base alphabet. The ambient vertex cardinality does not occur.
```
theorem natCard_poweredAlphabet [Finite D] [Finite A] (n : Nat) :
    Nat.card (PaddedLabel D (n + 1) A) =
      Nat.card A ^ (∑ j : Fin (n + 2), Nat.card D ^ j.val) :=
…
```
theorem OAI.MaxCutGames.Foundations.PCP.PoweringCounting.natCard_finitePortAlphabet line 835
Source documentation
With finite numbered ports, the same exponent is the length of the already constructed executable address enumeration.
```
theorem natCard_finitePortAlphabet [Finite A] (d n : Nat) :
    Nat.card (PaddedLabel (Fin d) (n + 1) A) =
      Nat.card A ^ (PoweringAddresses.allAddresses d (n + 1)).length := by
…
```
Mentions: OAI.MaxCutGames.Foundations.PCP.PoweringAddresses.allAddresses