Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Native RAM execution of the weight-to-multiplicity reduction

Lax263307.NativeWeightReduction · concepts/Lax263307/NativeWeightReduction.lean · lax-263307

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Theorem

    One fixed finite RAM program reads the exact unprefixed weighted-graph input, clips negative weights, finds the maximum, and emits the rounded copy counts in vertex order. Its running time and sufficient word width are at most c(n+h+1)^2 when all rational numerators and denominators are at most 2^h. The guarantee holds at every larger word width.

    Concept map
    6 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Lax263307.WeightRounding
    2import Lax808846.Ram
    3
    4/-!
    5---
    6title: Native RAM execution of the weight-to-multiplicity reduction
    7type: theorem
    8---
    9One fixed finite RAM program reads the exact unprefixed weighted-graph input,
    10clips negative weights, finds the maximum, and emits the rounded copy counts
    11in vertex order. Its running time and sufficient word width are at most
    12c(n+h+1)^2 when all rational numerators and denominators are at most 2^h.
    13The guarantee holds at every larger word width.
    14
    15# Formalization notes
    16
    17The proof compiles the checked input, maximum, accuracy, multiplicity, and
    18output loops through the registered RAM simulation theorem. Empty graphs
    19and instances with no positive weight are included. This implements the
    20multiplicity calculation; constructing the blow-up and executing the
    21recursive independent-set algorithm remain separate native obligations.
    22-/
    23
    24namespace Lax263307.NativeWeightReduction
    25
    26open WeightedIndependentSet WeightRounding
    27
    28axiom exists_program : ∃ p : Lax808846.Ram.Program, ∃ c : ℕ, 0<c ∧
    29 ∀ (n h : ℕ), 1≤h → ∀ (G : SimpleGraph (Fin n)) [DecidableRel G.Adj]
    30 (w : Fin n → ℚ) (ε : ℚ), 0<ε →
    31 (∀ i,(w i).num.natAbs≤2^h ∧ (w i).den≤2^h) →
    32 ε.num.natAbs≤2^h → ε.den≤2^h →
    33 ∀ width : ℕ,c*(n+h+1)^2≤width →
    34 ∃ t≤c*(n+h+1)^2,Lax808846.Ram.RunsTo width p (encodeInput G w ε)
    35 (List.ofFn (copies (fun i => max (w i) 0) ε)) t
    36
    37end Lax263307.NativeWeightReduction
    38
    Show Proof
    Formalization notes

    The proof compiles the checked input, maximum, accuracy, multiplicity, and output loops through the registered RAM simulation theorem. Empty graphs and instances with no positive weight are included. This implements the multiplicity calculation; constructing the blow-up and executing the recursive independent-set algorithm remain separate native obligations.

    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…