Project-declaredLean 4.31.0 · mathlib@fabf563a7c95

Append node Ok inr

ChallengeTreeShape.append_nodeOk_inr

cryptography proof systems coding theory seq compose

Plain-language statement

The append node predicate at a right-embedded index reduces to the right shape's predicate.

Exact Lean statement

theorem append_nodeOk_inr (S₁ : ChallengeTreeShape p₁) (S₂ : ChallengeTreeShape p₂)
    (i₂ : p₂.ChallengeIdx)
    (challenges : Fin ((S₁.append S₂).arity (ChallengeIdx.inr i₂)) →
        (p₁ ++ₚ p₂).Challenge (ChallengeIdx.inr i₂)) :
    (S₁.append S₂).nodeOk (ChallengeIdx.inr i₂) challenges
      = S₂.nodeOk i₂ (fun j => cast (by simp [ProtocolSpec.append, ChallengeIdx.inr])
          (challenges (Fin.cast (by
            change S₂.arity i₂ = ChallengeTree.appendArity S₁.arity S₂.arity (ChallengeIdx.inr i₂)
            simp only [ChallengeTree.appendArity, Function.comp_apply,
              ChallengeIdx.sumEquiv_symm_inr, Sum.elim_inr]) j)))

Formal artifact

Lean source

Canonical source

Full Lean sourceLean 4

theorem append_nodeOk_inr (S₁ : ChallengeTreeShape p₁) (S₂ : ChallengeTreeShape p₂)    (i₂ : p₂.ChallengeIdx)    (challenges : Fin ((S₁.append S₂).arity (ChallengeIdx.inr i₂)) →        (p₁ ++ₚ p₂).Challenge (ChallengeIdx.inr i₂)) :    (S₁.append S₂).nodeOk (ChallengeIdx.inr i₂) challenges      = S₂.nodeOk i₂ (fun j => cast (by simp [ProtocolSpec.append, ChallengeIdx.inr])          (challenges (Fin.cast (by            change S₂.arity i₂ = ChallengeTree.appendArity S₁.arity S₂.arity (ChallengeIdx.inr i₂)            simp only [ChallengeTree.appendArity, Function.comp_apply,              ChallengeIdx.sumEquiv_symm_inr, Sum.elim_inr]) j))) := by  simp only [ChallengeTreeShape.append]  split  · rename_i i₁' heq    rw [ChallengeIdx.sumEquiv_symm_inr] at heq    simp at heq  · rename_i i₂' heq    rw [ChallengeIdx.sumEquiv_symm_inr] at heq    obtain rfl : i₂' = i₂ := by simpa using heq.symm    rfl

Project: ArkLib
License: Apache-2.0
Commit: fad5cbf80877
Source: ArkLib/OracleReduction/Security/CoordinateWiseSpecialSoundness/SeqCompose.lean:184-202

Reuse this declaration

Bring the exact result into your workflow

The import identifies the source module. Your project still needs the pinned package dependency shown on this page.

What this badge means

This completion status comes from the project or community source. It has not yet been represented here as an independent rebuild and axiom audit.

Continue in this project

Related declarations

Project-declaredLean 4.31.0

Affine gaps lifted to interleaved codes

affine_gaps_lifted_to_interleaved_codes

Project documentation

This lemma proves the final algebraic step in the DG25 Theorem 3.1 proof. It shows that if R > e + 1, then e * (R / (R - 1)) < e + 1. The intuition is that the fraction R / (R - 1) is always greater than 1, but as R gets larger, it gets closer to 1. The hypothesis R > e + 1 provides a strong enough bound to ensure the product e * (fraction) do...

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record

Project-declaredLean 4.31.0

Gadget Decompose coeff

ArkLib.Lattices.Ajtai.gadgetDecompose_coeff

Plain-language statement

The k-th coefficient (k < deg φ) of a gadget-decomposition block is exactly the corresponding digit of the corresponding input coefficient.

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record

Project-declaredLean 4.31.0

Gadget Decompose lawful

ArkLib.Lattices.Ajtai.gadgetDecompose_lawful

Plain-language statement

The base-b gadget decomposition is a lawful gadget decomposition.

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record