Seq Compose succ
ChallengeTreeShape.seqCompose_succ
Plain-language statement
Successor unfolding of the sequentially-composed shape. ChallengeTreeShape.seqCompose of a family over m + 1 factors is the binary append of the head shape with the sequential composition of the tail. This is the shape-level analogue of ProtocolSpec.seqCompose_succ_eq_append, and is what lets the n-ary tree-soundness induction reduce its ste...
Exact Lean statement
theorem seqCompose_succ (S : ∀ i, ChallengeTreeShape (pSpec i)) :
ChallengeTreeShape.seqCompose S =
(S 0).append (ChallengeTreeShape.seqCompose (fun i => S (Fin.succ i)))Formal artifact
Lean source
theorem seqCompose_succ (S : ∀ i, ChallengeTreeShape (pSpec i)) : ChallengeTreeShape.seqCompose S = (S 0).append (ChallengeTreeShape.seqCompose (fun i => S (Fin.succ i))) := by have harity : (ChallengeTreeShape.seqCompose S).arity = ((S 0).append (ChallengeTreeShape.seqCompose (fun i => S (Fin.succ i)))).arity := by funext i change (S (seqComposeChallengeIdxToSigma i).1).arity (seqComposeChallengeIdxToSigma i).2 = ChallengeTree.appendArity (S 0).arity (ChallengeTreeShape.seqCompose (fun i => S (Fin.succ i))).arity i rcases hsplit : (ChallengeIdx.sumEquiv (pSpec₁ := pSpec 0) (pSpec₂ := ProtocolSpec.seqCompose (fun i => pSpec (Fin.succ i)))).symm i with i₁ | i₂ · obtain rfl : i = (ChallengeIdx.inl (pSpec₂ := ProtocolSpec.seqCompose (fun i => pSpec (Fin.succ i))) i₁ : (ProtocolSpec.seqCompose pSpec).ChallengeIdx) := by have := (Equiv.symm_apply_eq ChallengeIdx.sumEquiv).mp hsplit simp only [ChallengeIdx.sumEquiv_apply, Sum.elim_inl] at this exact this rw [toSigma_inl] simp only [ChallengeTree.appendArity, Function.comp_apply, ChallengeIdx.sumEquiv_symm_inl, Sum.elim_inl] · obtain rfl : i = (ChallengeIdx.inr (pSpec₁ := pSpec 0) i₂ : (ProtocolSpec.seqCompose pSpec).ChallengeIdx) := by have := (Equiv.symm_apply_eq ChallengeIdx.sumEquiv).mp hsplit simp only [ChallengeIdx.sumEquiv_apply, Sum.elim_inr] at this exact this rw [toSigma_inr] simp only [ChallengeTree.appendArity, Function.comp_apply, ChallengeIdx.sumEquiv_symm_inr, Sum.elim_inr] rfl refine ChallengeTreeShape.ext harity ?_ refine Function.hfunext rfl (fun i i' hi => ?_) obtain rfl : i = i' := eq_of_heq hi refine Function.hfunext (by rw [harity]) (fun challenges challenges' hch => ?_) rcases hsplit : (ChallengeIdx.sumEquiv (pSpec₁ := pSpec 0) (pSpec₂ := ProtocolSpec.seqCompose (fun i => pSpec (Fin.succ i)))).symm i with i₁ | i₂ · obtain rfl : i = (ChallengeIdx.inl (pSpec₂ := ProtocolSpec.seqCompose (fun i => pSpec (Fin.succ i))) i₁ : (ProtocolSpec.seqCompose pSpec).ChallengeIdx) := by have := (Equiv.symm_apply_eq ChallengeIdx.sumEquiv).mp hsplit simp only [ChallengeIdx.sumEquiv_apply, Sum.elim_inl] at this exact this apply heq_of_eq rw [seqCompose_nodeOk_eq, append_nodeOk_inl] have hsig := toSigma_inl (pSpec := pSpec) i₁ have hfst := congrArg Sigma.fst hsig have hsnd := (Sigma.ext_iff.mp hsig).2 refine eq_of_heq (heq_nodeOk (congrArg len hfst) ?_ ?_ hsnd ?_) · rw [hfst] · rw [hfst] · refine Function.hfunext (congrArg Fin ?hdom) (fun j j' hj => ?_) case hdom => change (ChallengeTreeShape.seqCompose S).arity _ = (S 0).arity i₁ rw [harity] change ChallengeTree.appendArity (S 0).arity (ChallengeTreeShape.seqCompose (fun i => S (Fin.succ i))).arity (ChallengeIdx.inl i₁) = (S 0).arity i₁ simp only [ChallengeTree.appendArity, Function.comp_apply, ChallengeIdx.sumEquiv_symm_inl, Sum.elim_inl] refine HEq.trans (cast_heq _ _) (HEq.trans ?_ (cast_heq _ _).symm) refine heq_app (by rw [harity]) ?_ hch ?_ · rw [harity] · refine HEq.trans hj ?_ exact (Fin.heq_ext_iff (by change (S 0).arity i₁ = ChallengeTree.appendArity (S 0).arity (ChallengeTreeShape.seqCompose (fun i => S (Fin.succ i))).arity (ChallengeIdx.inl i₁) simp only [ChallengeTree.appendArity, Function.comp_apply, ChallengeIdx.sumEquiv_symm_inl, Sum.elim_inl])).mpr rfl · obtain rfl : i = (ChallengeIdx.inr (pSpec₁ := pSpec 0) i₂ : (ProtocolSpec.seqCompose pSpec).ChallengeIdx) := by have := (Equiv.symm_apply_eq ChallengeIdx.sumEquiv).mp hsplit simp only [ChallengeIdx.sumEquiv_apply, Sum.elim_inr] at this exact this apply heq_of_eq rw [seqCompose_nodeOk_eq, append_nodeOk_inr, seqCompose_nodeOk_eq] have hsig := toSigma_inr (pSpec := pSpec) i₂ have hfst := congrArg Sigma.fst hsig have hsnd := (Sigma.ext_iff.mp hsig).2 refine eq_of_heq (heq_nodeOk (congrArg len hfst) ?_ ?_ hsnd ?_) · rw [hfst] · rw [hfst] · refine Function.hfunext (congrArg Fin ?hdomr) (fun j j' hj => ?_) case hdomr => change (ChallengeTreeShape.seqCompose S).arity _ = (ChallengeTreeShape.seqCompose (fun i => S (Fin.succ i))).arity i₂ rw [harity] change ChallengeTree.appendArity (S 0).arity (ChallengeTreeShape.seqCompose (fun i => S (Fin.succ i))).arity (ChallengeIdx.inr i₂) = (ChallengeTreeShape.seqCompose (fun i => S (Fin.succ i))).arity i₂ simp only [ChallengeTree.appendArity, Function.comp_apply, ChallengeIdx.sumEquiv_symm_inr, Sum.elim_inr] refine HEq.trans (cast_heq _ _) ?_ refine HEq.trans ?_ (HEq.trans (cast_heq _ _) (cast_heq _ _)).symm refine heq_app (by rw [harity]) ?_ hch ?_ · rw [harity] · refine HEq.trans hj ?_ exact (Fin.heq_ext_iff (by change (ChallengeTreeShape.seqCompose (fun i => S (Fin.succ i))).arity i₂ = ChallengeTree.appendArity (S 0).arity (ChallengeTreeShape.seqCompose (fun i => S (Fin.succ i))).arity (ChallengeIdx.inr i₂) simp only [ChallengeTree.appendArity, Function.comp_apply, ChallengeIdx.sumEquiv_symm_inr, Sum.elim_inr])).mpr rfl- Project
- ArkLib
- License
- Apache-2.0
- Commit
- fad5cbf80877
- Source
- ArkLib/OracleReduction/Security/CoordinateWiseSpecialSoundness/SeqCompose.lean:249-349
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
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...
Source project: ArkLib
Person-level attribution pending.
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.
Source project: ArkLib
Person-level attribution pending.
Gadget Decompose lawful
ArkLib.Lattices.Ajtai.gadgetDecompose_lawful
Plain-language statement
The base-b gadget decomposition is a lawful gadget decomposition.
Source project: ArkLib
Person-level attribution pending.